Publication Details

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

ABDULLA Parosh A., CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, CHEN Yu-Fang, MAYR Richard and VOJNAR Tomáš. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. FIT-TR-2010-02, Brno: Faculty of Information Technology BUT, 2010.
Czech title
Simulační pokrytí v Ramseyho testu univerzality a Inkluze Büchiho automatů
Type
technical report
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Clemente Lorenzo (UEDIN)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Hong Chih-Duo (ASIN)
Chen Yu-Fang (ASIN)
Mayr Richard (UEDIN)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

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

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.

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.

Published
2010
Pages
30
Publisher
Faculty of Information Technology BUT
Place
FIT-TR-2010-02, Brno, CZ
BibTeX
@TECHREPORT{FITPUB9207,
   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 = "https://www.fit.vut.cz/research/publication/9207"
}
Back to top