2011 | OriginalPaper | Buchkapitel
Advanced Ramsey-Based Büchi Automata Inclusion Testing
verfasst von : Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukáš Holík, Chih-Duo Hong, Richard Mayr, Tomáš Vojnar
Erschienen in: CONCUR 2011 – Concurrency Theory
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Checking language inclusion between two nondeterministic Büchi automata
$\mathcal A$
and
$\mathcal 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
$\mathcal A$
and
$\mathcal B$
, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on
$\mathcal A$
and
$\mathcal B$
. (2) A method to additionally use forward simulation
between
$\mathcal A$
and
$\mathcal 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.