Technical reportABDULLA, P., A., CLEMENTE, L., HOLÍK, L., HONG, C., CHEN, Y., MAYR, R. and VOJNAR, T.. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. FIT-TR-2010-02, Brno: Faculty of Information Technology BUT, 2010. | 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{\'{a}}{\v{s}}
Hol{\'{i}}k and Chih-Duo Hong and Yu-Fang Chen and Richard
Mayr and Tom{\'{a}}{\v{s}} Vojnar},
title = {Simulation Subsumption in Ramsey-based B{\"{u}}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.en?id=9207}
} |
|