Advanced Ramsey-based Büchi Automata Inclusion Testing

Abstract : Checking language inclusion between two nondeterministic B ̈ chi au- u tomata 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 rela- tion 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) Ab- straction 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.
Type de document :
Communication dans un congrès
CONCUR, 2011, Aachen, Germany. 2011
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
Contributeur : Sofia Cassel <>
Soumis le : vendredi 2 décembre 2011 - 11:24:10
Dernière modification le : jeudi 7 février 2019 - 14:59:47
Document(s) archivé(s) le : dimanche 4 décembre 2016 - 14:58:30


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00647523, version 1



Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukáš Holík, Chih-Duo Hong, et al.. Advanced Ramsey-based Büchi Automata Inclusion Testing. CONCUR, 2011, Aachen, Germany. 2011. 〈hal-00647523〉



Consultations de la notice


Téléchargements de fichiers