Abstract
There has been several attempts over the years to solve the bisimulation minimization problem for finite automata. One of the most famous algorithms is the one suggested by Paige and Tarjan. The algorithm has a complexity of \(\mathcal O\)(m log n) where m is the number of edges and n is the number of states in the automaton. A bottleneck in the application of the algorithm is often the number of labels which may appear on the edges of the automaton. In this paper we adapt the Paige-Tarjan algorithm to the case where the labels are symbolically represented using Binary Decision Diagrams (BDDs). We show that our algorithm has an overall complexity of \({\mathcal O}(l \cdot m \cdot log{n})\) where ℓ is the size of the alphabet. This means that our algorithm will have the same worst case behavior as other algorithms. However, as shown by our prototype implementation, we get a vast improvement in performance due to the compact representation provided by the BDDs.
This work was supported by the the Swedish Research Council(http://www.vr.se/).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bouali, A.: Xeve, an esterel verification environment. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 500–504. Springer, Heidelberg (1998)
Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394–397. Springer, Heidelberg (1996)
Fernandez, J.C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Abdulla, P., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 348–360. Springer, Heidelberg (2004)
Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J.: Algorithmic improvements in regular model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 236–248. Springer, Heidelberg (2003)
Hopcroft, J.E.: An n logn algorithm for minimizing the states in a finite automaton. In: Kohavi, Z. (ed.) The Theory of Machines and Computations, pp. 189–196. Academic Press, London (1971)
Paige, R., Tarjan, R., Bonic, R.: A linear time solution to the single function coarsest partition problem. Theoretical Computer Science 40, 67–84 (1985)
Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM Journal on Computing 16, 973–989 (1987)
Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. Theoretical Computer Science 311, 221–256 (2004)
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers C-35, 677–691 (1986)
Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: ICCAD 1993: Proc. of the 1993 IEEE/ACM international conference on Computer-aided design, pp. 188–191. IEEE Computer Society Press, Los Alamitos (1993)
Fernandez, J.C.: An implementation of an efficient algorithm for bisimulation equivalence. Sci. Comput. Program. 13 (1989)
Bouali, A., de Simone, R.: Symbolic bisimulation minimisation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 96–108. Springer, Heidelberg (1993)
Klarlund, N.: An n logn algorithm for online bdd refinement. J. Algorithms 32, 133–154 (1999)
Fisler, K., Vardi, M.Y.: Bisimulation and model checking. In: Conference on Correct Hardware Design and Verification Methods, pp. 338–341 (1999)
Bouajjani, A., Fernandez, J., Halbwachs, N.: Minimal model generation (manuscript, 1990)
Lee, D., Yannakakis, M.: Online minimization of transition systems. In: Proc. 24 ACM Symp. on Theory of Computing (1992)
Andersen, H.R.: An introduction to binary decision diagrams. Technical Report DK-2800, Department of Information Technology, Technical University of Denmark (1998)
Somenzi, F.: Binary decision diagrams (1999)
Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench: A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems 15 (1993)
Kanellakis, P., Smolka, S.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86, 43–68 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Deneux, J., Kaati, L., Nilsson, M. (2006). Minimization of Non-deterministic Automata with Large Alphabets. In: Farré, J., Litovsky, I., Schmitz, S. (eds) Implementation and Application of Automata. CIAA 2005. Lecture Notes in Computer Science, vol 3845. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11605157_3
Download citation
DOI: https://doi.org/10.1007/11605157_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31023-5
Online ISBN: 978-3-540-33097-4
eBook Packages: Computer ScienceComputer Science (R0)