CCS, locations and asynchronous transition systems

Abstract

We provide a simple non-interleaved operational semantics for GGS in terms of asynchronous transition systems. We 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 CGS 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 also introduce a notion of bisimulation on asynchronous transition systems which preserves independence. We conjecture that the induced equivalence on CGS processes coincides with the notion of location equivalence proposed by Boudol et al.