Several timed process calculi have been proposed in the literature, which mainly differ for the way in which 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. To reconcile the two approaches, in a previous work an encoding from the integrated-time calculus CIPA to the orthogonal-time calculus TCCS was defined, which preserves timed bisimilarity. To complete the picture, in this paper we consider the reverse translation, by examining the modifications to the two calculi that are needed to make an encoding feasible, as well as the behavioral equivalence that is appropriate to preserve. We then introduce an encoding from modified TCCS to modified CIPA, and show that it can only preserve the weak variant of timed bisimilarity.
Timed Process Calculi: From Durationless Actions to Durational Ones
Bernardo, Marco;
2014
Abstract
Several timed process calculi have been proposed in the literature, which mainly differ for the way in which 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. To reconcile the two approaches, in a previous work an encoding from the integrated-time calculus CIPA to the orthogonal-time calculus TCCS was defined, which preserves timed bisimilarity. To complete the picture, in this paper we consider the reverse translation, by examining the modifications to the two calculi that are needed to make an encoding feasible, as well as the behavioral equivalence that is appropriate to preserve. We then introduce an encoding from modified TCCS to modified CIPA, and show that it can only preserve the weak variant of timed bisimilarity.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
