Technical report

 
Abdulla, P., A., Clemente, L., Holík, L., Hong, C., Chen, Y., Mayr, R., Vojnar, T.: Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing, FIT-TR-2010-02, Brno, CZ, FIT VUT, 2010, p. 30
Publication language:english
Original title:Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing
Title (cs):Simulační pokrytí v Ramseyho testu univerzality a Inkluze Büchiho automatů
Pages:30
Place:FIT-TR-2010-02, Brno, CZ
Year:2010
Publisher:Faculty of Information Technology BUT
URL:http://www.fit.vutbr.cz/~holik/pub/FIT-TR-2010-002.pdf [PDF]
Keywords
Büchi automata, universality, language inclusion, Ramsey-based methods, simulation subsumption
Annotation
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.
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.
BibTeX:
@TECHREPORT{
   author = {A. Parosh Abdulla and Lorenzo Clemente and Lukáš Holík and
	Chih-Duo Hong and Yu-Fang Chen and Richard Mayr and Tomáš
	Vojnar},
   title = {Simulation Subsumption in Ramsey-based Büchi Automata
	Universality and Inclusion Testing},
   pages = {30},
   year = {2010},
   location = {FIT-TR-2010-02, Brno, CZ},
   publisher = {Faculty of Information Technology BUT},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9207}
}