Unique Solutions of Guarded Recursive Equations

TL;DR

This paper proves that guarded recursive equations in process algebra have unique solutions up to various behavioral equivalences, ensuring these are congruences and enabling a complete axiomatisation.

Contribution

It establishes the uniqueness of solutions for guarded recursive equations across multiple behavioral equivalences in process algebra, and derives a complete axiomatisation.

Findings

Guarded recursive equations have unique solutions up to strong bisimilarity.

Equivalences and preorders are full congruences for guarded recursion.

Provides a sound and ground-complete axiomatisation for strong bisimilarity.

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.