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.
翻译:本文证明,对于任何具有就绪模拟格式结构操作语义的过程代数,守卫递归方程组在强互模拟意义下具有唯一解。类似结果对于模拟等价、就绪模拟等价以及(就绪)模拟预序同样成立。因此,这些等价关系与预序关系构成守卫递归的完全(预)同余关系。此外,唯一解结果为任意有限GSOS语言中强互模拟的可靠且地面完备的公理化提供了理论依据。