Unique Solutions of Guarded Recursive Equations

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 groundcomplete axiomatisation of strong bisimilarity for any finitary GSOS language.