Simple Bisimilarity Minimization in O(m log n) Time

• Autorzy: Valmari A.
• Języki publikacji: EN

Abstrakty

EN

A new algorithm for bisimilarity minimization of labelled directed graphs is presented. Its time consumption is O(mlog 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.

Słowa kluczowe

EN

bisimilarity; refinable partition data structure

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 105, nr 3
• Strony: 319--339
• Opis fizyczny: Bibliogr. 14 poz., tab.

Twórcy

autor

Valmari A.

• Tampere University of Technology, Department of Software Systems, PO Box 553, FI-33101 Tampere, Finland,

Bibliografia

• [1] Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, MA (1974)
• [2] Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science 59, 115-131 (1988)
• [3] Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal State-space Lumping in Markov Chains. Information Processing Letters 87(6), 309-315 (2003)
• [4] Dovier, A., Piazza, C., Policriti, A.: An Efficient Algorithm for Computing Bisimulation Equivalence. Theoretical Computer Science 311, 221-256 (2004)
• [5] Fernandez, J.-C.: An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming 13, 219-236 (1989/90)
• [6] Gries, D.: Describing an Algorithm by Hopcroft. Acta Informatica 2, 97-109 (1973)
• [7] Hopcroft, J.: An n log n Algorithm for Minimizing States in a Finite Automaton. Technical Report STAN-CS-71-190, Stanford University (1971)
• [8] Kanellakis, P., Smolka, S.: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. In: 2nd ACM Symposium on Principles of Distributed Computing, 228-240 (1983)
• [9] Knuutila, T.: Re-describing an Algorithm by Hopcroft. Theoretical Computer Science 250, 333-363 (2001)
• [10] Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs, NJ (1989)
• [11] Paige, R., Tarjan, R.: Three Partition Refinement Algorithms. SIAM Journal of Computing 16(6), 973-989 (1987)
• [12] Valmari, A.: Bisimilarity Minimization in O(mlog n) time. In: Franceschinis, G.,Wolf, K. (eds.): Petri Nets 2009, Lecture Notes in Computer Science 5606, 123-142, Springer, Heidelberg (2009)
• [13] Valmari, A., Franceschinis, G.: Simple O(mlog n) TimeMarkov Chain Lumping. In: Esparza, J.,Majumdar, R. (eds.) TACAS 2010, Lecture Notes in Computer Science 6015, 38-52, Springer, Heidelberg (2010)
• [14] Valmari, A., Lehtinen, P.: Efficient Minimization of DFAs with Partial Transition Functions. In: Albers, S., Weil, P. (eds.) STACS 2008, Symposium on Theoretical Aspects of Computer Science, Bordeaux, France, 645-656. http://drops.dagstuhl.de/volltexte/2008/1328/ (2008)