Universal Coinductive Characterisations of Process Semantics

Abstract

We present a theoretical framework which allows to define in a uniform way coinductive characterisations of nearly any semantic preorder or equivalence between processes, by means of simulations up-to and bisimulations up-to. In particular, all the semantics in the linear time-branching time spectrum are covered. Constrained simulations, that generalise plain simulations by including a constraint that all the pairs of related processes must satisfy, are the key to obtain such a general framework. We provide a simple axiomatisation of any constrained simulation preorder and also for the corresponding equivalence. These axiomatizations allow us to prove in a uniform way that each constrained simulation preorder (equivalence) defines a class of process preorders (equivalences) which share commons properties, like the possibility of giving coinductive characterisations for all of them, or the existence of a canonical preorder inducing each of these equivalences.