Minimal transition systems with respect to divergence preserving behavioural equivalences

Jaana Eloranta: Minimal transition systems with respect to divergence preserving behavioural equivalences. PhD Thesis, Report A-1994-1, Department of Computer Science, University of Helsinki, January 1994. 162 pages. <http://www.cs.helsinki.fi/TR/A-1994/1>

Full paper:
Metadata: XML file

Abstract

Three divergence preserving behavioural equivalences for labelled transition systems (lts), namely D-bisimilarity, branching D-bisimilarity and CFFD-equivalence, are analyzed and compared. For an image-finite lts, which does not contain an infinite sequence of distinct t-connected states, it is possible to find the unique lts which is state- and transition-minimal with respect to D-bisimilarity or branching D-bisimilarity. It is well known how to find an equivalent state-minimal lts. We show how the state and transition-minimal lts can be found, and moreover give a transition minimization algorithm in a finite case. In the case of CFFD-equivalence, which is a modification of failures-equivalence, a unique state- and transition-minimal lts cannot always be found.

For rooted versions of D-bisimilarity and branching D-bisimilarity the uniqueness result holds only for root-unwound lts's. Related equivalences, D-congruence and branching D-congruence, handle the first transitions from a root, rather than a root itself, in a special way. The relation between rooted equivalences and corresponding congruences is fully analyzed. For D-congruence and branching D-congruence a unique root-unwound minimal lts is found, for an image-finite (without an infinite sequence of distinct t-connected states). Moreover, D-congruence and branching D-congruence are compositional with respect to Basic LOTOS operations. Since the same result holds for CFFD-equivalence, D-congruence, branching D-congruence and CFFD-equivalence are compatible with compositional reduction.

In order to apply and demonstrate the theoretical results, we specify and verify several concurrent systems. The specifications are reduced with respect to several equivalences, including D-congruence, branching D-congruence and CFFD-equivalence. The analysis shows that it is possible to find errors, as well as reasons for divergences by studying reduced lts's. Moreover, these case studies are used to test the effect of the transition-minimization algorithm, to compare divergence preserving and divergence ignoring equivalences, and to compare branching and weak versions of equivalences. In some studies compositional reduction is used and the results are analyzed. Furthermore, based on the results of these applications, we propose some modifications to the reduction algorithm with respect to CFFD-equivalence.

Index Terms

Categories and Subject Descriptors:
F.3.1, D.2.4, F.1.1, F.1.2

General Terms: Specification, Verification, Concurrency, Laballed transition system

Additional Key Words and Phrases: interleaving semantics for concurrency, behavirioural equivalences, divergence, minimization