CCS, Locations and Asynchronous Transition Systems
DOI:
https://doi.org/10.7146/dpb.v21i395.6630Abstract
Our aim is to provide a simple non-interleaved operational semantics for CCS in terms of a model that is easy to understand - asynchronous transition systems. Our approach is guided by the requirement that the semantics should identify the concurrency present in the system in a natural way, in terms of events occurring at independent locations in the system.
We extend the standard interleaving transition system for CCS by introducing labels on the transitions with information about the locations of events. We then show that the resulting transition system is an asynchronous transition system which has the additional property of being elementary, which means that it can also be represented by a 1-safe net. We establish a close correspondence between our semantics and other approaches in terms of foldings.
We also introduce a notion of bisimulation on asynchronous transition systems which preserves independence. We conjecture that the induced equivalence on CCS processes coincides with the notion of location equiualence proposed by Boudol et al.
Downloads
Published
How to Cite
Issue
Section
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.