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. © 2008 Springer Science+Business Media, LLC.
CITATION STYLE
de Frutos Escrig, D., & Rodríguez, C. G. (2008). Universal coinductive characterisations of process semantics. In IFIP International Federation for Information Processing (Vol. 273, pp. 397–412). https://doi.org/10.1007/978-0-387-09680-3_27
Mendeley helps you to discover research relevant for your work.