Weakest Congruence Results Concerning “Any-Lock”

In process algebras the weakest congruences that preserve interesting properties of systems are of theoretical and practical importance. A system can stop executing visible actions in two ways: by deadlocking or livelocking. The weakest deadlock-preserving congruence was published in [20]. The weakest livelock-preserving congruence and the weakest congruence that preserves all traces of visible actions leading to a livelock were published in [17]. In this paper we will equate deadlock and livelock. We introduce the weakest congruence that preserves the predicate “any-lock” which distinguishes those systems that can stop executing visible actions from those that cannot. We also present the weakest congruence that preserves all traces after which the system can stop executing visible actions. Finally, we give two simple weakest-congruence characterisations for the CSP failures-divergences equivalence, one of which is a minimal characterisation in a well-defined sense. However, we also show that there is no minimum (least) characterisation.