In: Desel, J.: Structures in Concurrency Theory, Proceedings of the International Workshop on Structures in Concurrency Theory (STRICT), Berlin, 11-13 May 1995, pages 326-340. 1995.
Abstract: It has been known at least time 1983 that the checking of failure equivalence of two labelled transition systems is a PSPACE-complete problem. While the same problem for observation equivalence can be solved in roughly cubic time. Correspondingly, a widespread belief has arisen that failure-based equivalences are slower for the verification of concurrent systems than observation equivalence. In this article it is shown that this belief is based on a misinterpretation of the theoretical complexity result. Both theoretical and experimental evidence is given to the claim that failure-based equivalences are often faster in practice than observation equivalence. It is argued that the weakest congruence preserving given properties is in a certain sense optimal for the verification of those properties. Results giving weakest congruences for several verification tasks are surveyed.