Behaviour Equivalences in Timed Distributed π-Calculus
The complexity of the software-intensive systems requires working with notions as explicit locations in a distributed system, interaction among the mobile processes restricted by interaction timeouts, time scheduling, and restricted resource access. In order to work these notions, we use a timed and distributed variant of the π-calculus having explicit locations, types for restricting the resource access, and time constraints for interaction in distributed systems. Using observation predicates, several behavioural notions are defined and related: (global) barbed bisimulations, (global) typed barbed bisimulation, timed (global) barbed bisimulations, timed (global) typed barbed bisimulation and full timed global typed barbed bisimulation. These bisimulations form a lattice according to their distinguishing power.
KeywordsBehaviour Equivalence Locate Process Output Channel Channel Type Resource Access
Unable to display preview. Download preview PDF.
- 4.Ciobanu, G., Prisacariu, C.: Barbed Bisimulations for Timed Distributed π-Calculus. In: 2nd Int’l Conference on Intelligent Computer Communication and Processing, Cluj-Napoca, pages 6 (2006)Google Scholar
- 9.Milner, R., Sangiorgi, D.: Barbed Bisimulation. LNCS, vol. 623, pp. 685–695. Springer, Heidelberg (1992)Google Scholar
- 10.Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms, PhD Thesis, University of Edinburgh (1992)Google Scholar
- 11.van Glabbeek, R.J.: The Linear Time - Branching Time Spectrum. Handbook of Process Algebra, pp. 3–99 (2001)Google Scholar