Several deterministically/stochastically timed process calculi have been proposed in the literature that, apart from their synchronization mechanism, mainly differ for the way in which actions and delays are represented. In particular, a distinction is made between integrated-time calculi, in which actions are durational, and orthogonal-time calculi, in which actions are instantaneous and delays are expressed separately. In a previous work on deterministic time, the two approaches have been shown to be reconcilable through an encoding from the integrated-time calculus CIPA to the orthogonal-time calculus TCCS, which preserves strong timed bisimilarity under certain conditions. In this paper, the picture is completed by first defining a reverse encoding from TCCS to CIPA, which requires slight modifications to both calculi and is shown to preserve only weak timed bisimilarity under conditions tighter than those for the direct encoding. Stochastic time is then addressed, by exhibiting an encoding from the integrated-time calculus MTIPP to the orthogonal-time calculus IML, together with a reverse encoding requiring slight modifications only to the former calculus, with both encodings being shown to preserve strong Markovian bisimilarity under suitable conditions. All the four encodings rely on the assumption that action execution is urgent. Variants are finally discussed in which action execution is delayable, in the sense that an enabled action can let time advance before starting its execution, or only the execution of internal actions is urgent, which is known as maximal progress.

Timed process calculi with deterministic or stochastic delays: Commuting between durational and durationless actions

CORRADINI, Flavio;TESEI, Luca
2016-01-01

Abstract

Several deterministically/stochastically timed process calculi have been proposed in the literature that, apart from their synchronization mechanism, mainly differ for the way in which actions and delays are represented. In particular, a distinction is made between integrated-time calculi, in which actions are durational, and orthogonal-time calculi, in which actions are instantaneous and delays are expressed separately. In a previous work on deterministic time, the two approaches have been shown to be reconcilable through an encoding from the integrated-time calculus CIPA to the orthogonal-time calculus TCCS, which preserves strong timed bisimilarity under certain conditions. In this paper, the picture is completed by first defining a reverse encoding from TCCS to CIPA, which requires slight modifications to both calculi and is shown to preserve only weak timed bisimilarity under conditions tighter than those for the direct encoding. Stochastic time is then addressed, by exhibiting an encoding from the integrated-time calculus MTIPP to the orthogonal-time calculus IML, together with a reverse encoding requiring slight modifications only to the former calculus, with both encodings being shown to preserve strong Markovian bisimilarity under suitable conditions. All the four encodings rely on the assumption that action execution is urgent. Variants are finally discussed in which action execution is delayable, in the sense that an enabled action can let time advance before starting its execution, or only the execution of internal actions is urgent, which is known as maximal progress.
2016
File in questo prodotto:
File Dimensione Formato  
BCT16-postprint.pdf

solo gestori di archivio

Descrizione: Full text post-print
Tipologia: Documento in Post-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 490.25 kB
Formato Adobe PDF
490.25 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11581/392585
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact