Advanced Ramsey-Based Büchi Automata Inclusion Testing

Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukás Holík, Chih-Duo Hong, Richard Mayr, Tomás Vojnar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Checking language inclusion between two nondeterministic B¨uchi 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.
Original languageEnglish
Title of host publicationCONCUR 2011 - Concurrency Theory
Subtitle of host publication 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings
PublisherSpringer
Pages187-202
Number of pages16
Volume6901
ISBN (Electronic)978-3-642-23217-6
ISBN (Print)978-3-642-23216-9
DOIs
Publication statusPublished - 2011

Fingerprint

Dive into the research topics of 'Advanced Ramsey-Based Büchi Automata Inclusion Testing'. Together they form a unique fingerprint.

Cite this