Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing

Simulační pokrytí v Ramseyho testu univerzality a Inkluze Büchiho automatů

report

English

Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Chen Yu-Fang
Mayr Richard
Hong Chih-Duo
Abdulla Parosh
Clemente Lorenzo

• http://www.fit.vutbr.cz/~holik/pub/FIT-TR-2010-002.pdf

Büchi automata, universality, language inclusion, Ramsey-based methods, simulation subsumption

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.

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.

2010

30

Faculty of Information Technology BUT

FIT-TR-2010-02, Brno