Přístupnostní navigace
E-application
Search Search Close
Publication detail
HOLÍK, L. VOJNAR, T. CHEN, Y. MAYR, R. HONG, C. ABDULLA, P. CLEMENTE, L.
Original Title
Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing
Type
article in a collection out of WoS and Scopus
Language
English
Original Abstract
There are two main classes of methods for checking universality and language inclusion of Büchi-automata: Rank-based methods and Ramsey-based methods. While rank-based methods have a better worst-case complexity, Ramsey-based methods have been shown to be quite competitive in practice. Previously, it was also shown (for universality checking) that a simple subsumption technique, which avoids exploration of certain cases, greatly improves the performance of the Ramsey-based method. Here, we present a much more general subsumption technique for the Ramsey-based method, which is based on using simulation preorder on the states of the Büchi-automata. This technique applies to both universality and inclusion checking, yielding a substantial performance gain over the previously known simple subsumption approach.
Keywords
Büchi automata, universality, language inclusion, Ramsey-based methods, simulation subsumption
Authors
HOLÍK, L.; VOJNAR, T.; CHEN, Y.; MAYR, R.; HONG, C.; ABDULLA, P.; CLEMENTE, L.
RIV year
2010
Released
28. 7. 2010
Publisher
Springer Verlag
Location
Berlín
ISBN
978-3-642-14294-9
Book
Computer Aided Verification
Edition
Lecture Notes in Computer Science
Pages from
132
Pages to
147
Pages count
16
URL
http://www.springerlink.com/content/n81060p2685rl46v/
BibTex
@inproceedings{BUT34732, author="Lukáš {Holík} and Tomáš {Vojnar} and Yu-Fang {Chen} and Richard {Mayr} and Chih-Duo {Hong} and Parosh {Abdulla} and Lorenzo {Clemente}", title="Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing", booktitle="Computer Aided Verification", year="2010", series="Lecture Notes in Computer Science", volume="6174", pages="132--147", publisher="Springer Verlag", address="Berlín", isbn="978-3-642-14294-9", url="http://www.springerlink.com/content/n81060p2685rl46v/" }