Advanced Automata Minimization

Richard Mayr, Lorenzo Clemente

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We present an efficient algorithm to reduce the size of nondeterministic Buchi word automata, while retaining their language. Additionally, we describe methods to solve PSPACE-complete automata problems like universality, equivalence and inclusion for much larger instances (1-3 orders of magnitude) than before. This can be used to scale up applications of automata in formal verification tools and decision procedures for logical theories. The algorithm is based on new transition pruning techniques. These use criteria based on combinations of backward and forward trace inclusions. Since these relations are themselves PSPACE-complete, we describe methods to compute good approximations of them in polynomial time. Extensive experiments show that the average-case complexity of our algorithm scales quadratically. The size reduction of the automata depends very much on the class of instances, but our algorithm consistently outperforms all previous techniques by a wide margin. We tested our algorithm on Buchi automata derived from LTL-formulae, many classes of random automata and automata derived from mutual exclusion protocols, and compared its performance to the well-known automata tool GOAL.
Original languageEnglish
Title of host publicationPOPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
PublisherACM
Pages63-74
Number of pages12
ISBN (Print)978-1-4503-1832-7
DOIs
Publication statusPublished - Jan 2013

Fingerprint

Dive into the research topics of 'Advanced Automata Minimization'. Together they form a unique fingerprint.

Cite this