Publication Details

Advanced Ramsey-based Büchi Automata Inclusion Testing

ABDULLA Parosh A., CHEN Yu-Fang, CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, MAYR Richard and VOJNAR Tomáš. Advanced Ramsey-based Büchi Automata Inclusion Testing. Lecture Notes in Computer Science, vol. 2011, no. 6901, pp. 187-202. ISSN 0302-9743.
Czech title
Pokročilé techniky testování inkluze na Büchiho automatech s využitím technik založených na Ramseyho teorému
Type
journal article
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Chen Yu-Fang (ASIN)
Clemente Lorenzo (UEDIN)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Hong Chih-Duo (ASIN)
Mayr Richard (UEDIN)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

Büchi automata, inclusion checking, Ramsey theorem, simulation relations

Abstract

Checking language inclusion between two nondeterministic Büchi automata A and B is computationally hard (PSPACE-complete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the Ramsey-based approach. It has recently been shown that the basic Ramsey-based approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the search-space when looking for counterexamples to inclusion. While previous works only used subsumption based on set inclusion or forward simulation on A and B, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on A and B. (2) A method to additionally use forward simulation between A and B. (3) Abstraction techniques that can speed up the computation and lead to early detection of counterexamples. The new algorithm was implemented and tested on automata derived from real-world model checking benchmarks, and on the Tabakov-Vardi random model, thus showing the usefulness of the proposed techniques.

Published
2011
Pages
187-202
Journal
Lecture Notes in Computer Science, vol. 2011, no. 6901, ISSN 0302-9743
Publisher
Springer Verlag
BibTeX
@ARTICLE{FITPUB9722,
   author = "A. Parosh Abdulla and Yu-Fang Chen and Lorenzo Clemente and Luk\'{a}\v{s} Hol\'{i}k and Chih-Duo Hong and Richard Mayr and Tom\'{a}\v{s} Vojnar",
   title = "Advanced Ramsey-based B{\"{u}}chi Automata Inclusion Testing",
   pages = "187--202",
   journal = "Lecture Notes in Computer Science",
   volume = 2011,
   number = 6901,
   year = 2011,
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9722"
}
Back to top