Simulation Subsumption in Ramsey-Based Büchi Automata Universality and 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


There are two main classes of methods for checking universality and language inclusion of Büchi-automata: Rank-based methods and Ramsey-based methods. While rank-based methods have a better worst-case complexity, Ramsey-based methods have been shown to be quite competitive in practice [10,9]. It was shown in [10] (for universality checking) that a simple subsumption technique, which avoids exploration of certain cases, greatly improves the performance of the Ramsey-based method. Here, we present a much more general subsumption technique for the Ramsey-based method, which is based on using simulation preorder on the states of the Büchi-automata. This technique applies to both universality and inclusion checking, yielding a substantial performance gain over the previous simple subsumption approach of [10].
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-642-14295-6
ISBN (Print)978-3-642-14294-9
Publication statusPublished - 2010


Dive into the research topics of 'Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing'. Together they form a unique fingerprint.

Cite this