Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes
- 31 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 386-396
- https://doi.org/10.1109/lics.1993.287569
Abstract
The authors prove the decidability of two subclasses of recursive processes involving a parallel composition operator with respect to bisimulation equivalence, namely, the so-called normed and live processes. To accomplish this, the authors first prove a unique decomposition result for (a generalization of) normed processes, in order to deduce a necessary cancellation law. The decidability proof leads to a complete axiomatization for these process classes.<>Keywords
This publication has 9 references indexed in Scilit:
- Distributed bisimularity is decidable for a class of infinite state-space systemsPublished by Springer Nature ,2006
- Bisimulation equivalence is decidable for all context-free processesPublished by Springer Nature ,2006
- Actions speak louder than words: proving bisimilarity for context-free processesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A completeness theorem for Kleene algebras and the algebra of regular eventsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The Linear Time - Branching Time Spectrum I. The Semantics of Concrete, Sequential ProcessesPublished by Elsevier ,2001
- Unique decomposition of processesTheoretical Computer Science, 1993
- Graphes canoniques de graphes algébriquesRAIRO - Theoretical Informatics and Applications, 1990
- A complete inference system for a class of regular behavioursJournal of Computer and System Sciences, 1984
- Two Complete Axiom Systems for the Algebra of Regular EventsJournal of the ACM, 1966