On Bisimilarities Induced by Partial Orders

Relatore
S. Arun-Kumar - Indian Institute of Technology

Data e ora
martedì 29 giugno 2004 alle ore 17.30

Luogo
Ca' Vignal 3 - Piramide, Piano 0, Sala Verde

Referente
Massimo Merro

Referente esterno

Data pubblicazione
17 giugno 2004

Dipartimento
 

Riassunto

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.
ornamento
Inizio pagina