Informatics Report Series


Report   

EDI-INF-RR-1414


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Advanced Automata Minimization
Authors: Richard Mayr ; Lorenzo Clemente
Date:Oct 2012
Publication Title:POPL 2013
Publication Type:Conference Paper Publication Status:Pre-print
Abstract:
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.
Links To Paper
1st Link
Bibtex format
@InProceedings{EDI-INF-RR-1414,
author = { Richard Mayr and Lorenzo Clemente },
title = {Advanced Automata Minimization},
book title = {POPL 2013},
year = 2012,
month = {Oct},
url = {http://arxiv.org/abs/1210.6624},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh