Laurent Doyen ; Jean-Francois Raskin - Antichains for the Automata-Based Approach to Model-Checking

lmcs:1027 - Logical Methods in Computer Science, March 2, 2009, Volume 5, Issue 1 - https://doi.org/10.2168/LMCS-5(1:5)2009
Antichains for the Automata-Based Approach to Model-CheckingArticle

Authors: Laurent Doyen ; Jean-Francois Raskin

    We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buechi automata, and the emptiness problem for alternating Buechi automata. To obtain those algorithms, we establish the existence of simulation pre-orders that can be exploited to efficiently evaluate fixed points on the automata defined during the complementation step (that we keep implicit in our approach). We evaluate the performance of the algorithm to check the universality of Buechi automata using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, our algorithm outperforms the standard ones by several orders of magnitude.


    Volume: Volume 5, Issue 1
    Published on: March 2, 2009
    Imported on: August 13, 2007
    Keywords: Computer Science - Logic in Computer Science,F.4.1,I.1.2

    19 Documents citing this article

    Consultation statistics

    This page has been seen 990 times.
    This article's PDF has been downloaded 415 times.