Weakest-congruence results for livelock-preserving equivalences

摘要

A behavioural equivalence is a congruence, if a system is guaranteed to remain equivalent when nay one of its component processes is replaced by an equivalent component processes. An equivalence is weaker than another equivalence if the latter makes at least the same distinctions between systems as the former. An equivalence preserues a property, if no equivalence class contains one system that has that property and another system that lacks the property. Congruences that preserve such properties as deadlocks or livelocks are important in automatic verification of systems, and knowledge of the weakest such congruences is useful for designing verification algorithms. A simple denotational characterisation of the weakest deadlock-preserving congruence has been published in 1995. In this article simple characterisations are given to the weakest livelock-preserving congruence, and to the weakest congruence that preserves all livelocking traces. The results are compared to Hoare's failures-divergences equivalence in the CSP theory.