Technical reportABDULLA, P., A., CHEN, Y., CLEMENTE, L., HOLÍK, L., HONG, C., MAYR, R. and VOJNAR, T.. Advanced Ramseybased Büchi Automata Inclusion Testing. FITTR201103, Brno: Faculty of Information Technology BUT, 2011.  Publication language:  english 

Original title:  Advanced Ramseybased 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:  45 

Place:  FITTR201103, Brno, CZ 

Year:  2011 

Publisher:  Faculty of Information Technology BUT 

URL:  http://www.fit.vutbr.cz/~vojnar/Publications/fittr201103.pdf [PDF] 

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 (PSPACEcomplete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the Ramseybased approach. It has recently been shown that the basic Ramseybased approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the searchspace 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 realworld model checking benchmarks, and on the TabakovVardi random model, thus showing the usefulness of the proposed techniques. 
BibTeX: 

@TECHREPORT{
author = {A. Parosh Abdulla and YuFang Chen and Lorenzo Clemente and
Luk{\'{a}}{\v{s}} Hol{\'{i}}k and ChihDuo Hong and Richard
Mayr and Tom{\'{a}}{\v{s}} Vojnar},
title = {Advanced Ramseybased B{\"{u}}chi Automata Inclusion
Testing},
pages = {45},
year = {2011},
location = {FITTR201103, Brno, CZ},
publisher = {Faculty of Information Technology BUT},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.en?id=9721}
} 
