Simple Bisimilarity Minimization in O(m log n) Time

Issue title: Applications and Theory of Petri Nets and Other Models of Concurrency, 2009

Article type: Research Article

Authors: Valmari, Antti

Affiliations: Tampere University of Technology, Department of Software Systems, PO Box 553, FI-33101 Tampere, Finland. Antti.Valmari@tut.fi

Note: [] Address for correspondence: Tampere University of Technology, Department of Software Systems, PO Box 553, FI-33101 Tampere, Finland

Abstract: A new algorithm for bisimilarity minimization of labelled directed graphs is presented. Its time consumption is O(m log n), where n is the number of states and m is the number of transitions. Unlike earlier algorithms, it meets this bound even if the number of different labels of transitions is not fixed. It is based on refining a partition of states with respect to the labelled transitions. A splitter is a pair consisting of a label and a set in the partition. A transition belongs to a splitter, if and only if it has the same label and its end state is in the set. Earlier algorithms consume lots of time in scanning splitters that have no transitions. The new algorithm avoids this by maintaining also a partition of transitions. To facilitate this, a refinable partition data structure with amortized constant time operations is used. Detailed pseudocode of all nontrivial details is presented. Novel simplifications are applied that both reduce the practical memory consumption and shorten the program code.

DOI: 10.3233/FI-2010-369

Journal: Fundamenta Informaticae, vol. 105, no. 3, pp. 319-339, 2010