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
journal article
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)

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


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.

Lecture Notes in Computer Science, vol. 2011, no. 6901, ISSN 0302-9743
Springer Verlag
   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 = ""
Back to top