Minimization of non-deterministic automata with large alphabets

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 Tar Jan. The algorithm has a complexity of 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 O((ℓ · m · 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. © Springer-Verlag Berlin Heidelberg 2006.