Unique Solutions of Guarded Recursive Equations
Rob van Glabbeek
TL;DR
The paper proves that guarded systems of recursive equations have a unique solution up to strong bisimilarity $\sim_B$ for any process algebra whose operational semantics fit the ready simulation format with recursion. It develops a maximal guardedness concept, demonstrates that ready simulation and related preorders are full (pre)congruences for guarded recursion, and shows that strong bisimilarity admits a sound and ground-complete axiomatisation for finitary GSOS languages. Central to the results are the recursive specification principle (RSP) and the guardedness-based proof techniques, including a robust treatment of 3-valued transition semantics and well-founded derivations. The work unifies and extends existing RSP/RDP results across bisimulation, simulation, and ready simulation, yielding practical axiomatisations for GSOS languages and clarifying the role of guarded recursion in congruence proofs. It sets the stage for extending these congruence and axiomatisation results to additional equivalences in future work.
Abstract
This paper shows that guarded systems of recursive equations have unique solutions up to strong bisimilarity for any process algebra with a structural operation semantics in the ready simulation format. A similar result holds for simulation equivalence, for ready simulation equivalence and for the (ready) simulation preorder. As a consequence, these equivalences and preorders are full (pre)congruences for guarded recursion. Moreover, the unique-solutions result yields a sound and ground-complete axiomatisation of strong bisimilarity for any finitary GSOS language.