On Bisimilarities Induced by Partial Orders

The question of when two systems are behaviourally equal has occupied a large part of the literature on semantics and has yielded various equivalences (and congruences). These equivalence relations are most useful in comparing systems whose executions are not necessarily finite. Much of this effort (especially under interleaving models of concurrency) has been devoted to the study of the nature of nondeterminism and how it influences extensional behaviour and therefore the correctness of systems. In this talk, we generalize the notion of bisimulations to "bisimulations induced by a pair of partial orders" on the underlying action set. We establish that many of the nice properties of bisimulations and bisimilarities may be thought of as actually having been induced by properties of the orderings on actions. We then apply these generalized notions to both synchronous and asynchronous concurrent systems to analyze some features encompassing correctness and efficiency considerations. We develop these notions in the setting of labelled transition systems with a parallel composition operation. We restrict our attention to parallel composition operators and bisimulation notions which respect an expansion law (e.g. interleaving parallelism as in CCS and lock-step parallelism as in SCCS). This implies that processes represented as rooted labelled transition systems are closed under a product operation that represents their parallel composition. These cases provide instances of how one may define cost-based bisimulation relations by basing them on a ``temporal'' ordering or a ``spatial'' ordering on the underlying action sets respectively.