Journal article

 
Abdulla, P., A., Chen, Y., Clemente, L., Holík, L., Hong, C., Mayr, R., Vojnar, T.: Advanced Ramsey-based Büchi Automata Inclusion Testing, In: Lecture Notes in Computer Science, Vol. 2011, No. 6901, DE, p. 187-202, ISSN 0302-9743
Publication language:english
Original title:Advanced Ramsey-based Büchi Automata Inclusion Testing
Title (cs):Pokročilé techniky testování inkluze na Büchiho automatech s využitím technik založených na Ramseyho teorému
Pages:187-202
Place:DE
Year:2011
Journal:Lecture Notes in Computer Science, Vol. 2011, No. 6901, DE
ISSN:0302-9743
URL:http://www.springerlink.com/content/e14t15u580x7n332 [HTML]
Keywords
Büchi automata, inclusion checking, Ramsey theorem, simulation relations
Annotation
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.
BibTeX:
@ARTICLE{
   author = {A. Parosh Abdulla and Yu-Fang Chen and Lorenzo Clemente and
	Lukáš Holík and Chih-Duo Hong and Richard Mayr and Tomáš
	Vojnar},
   title = {Advanced Ramsey-based Bü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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=9722}
}