Antichain    ANTICHAINS ALGORITHMS


An antichain is a set of pairwise incomparable elements. In general, when a pre-order ≤ is given over a set (for example set inclusion over a powerset), a downward-closed set is a set S that contains all the elements x such that x ≤ y for some y ∈ S. The maximal elements of a set S is the set ⌈S⌉ = {x ∈ S | ∀ y ∈ S: x ≤ y ⇒ y ≤ x}. When dealing with downward-closed sets, we use the maximal elements as a concise and canonical representation of sets. When ≤ is a partial order, the set of maximal elements is an ≤-antichain.

Efficient antichain-based algorithms have been proposed to solve games of imperfect information, language inclusion and universality of nondeterministic finite automata over finite and infinite words, emptiness of alternating automata over finite and infinifte words, LTL satisfiability and model-checking. Applications to tree automata are currently under study.

NEW The tool Alaska (Antichains for Logic, Automata and Symbolic Kripke structure Analysis) can be found here.

Game    Games of imperfect information


We propose in [1] an antichain-based algorithm for solving safety games of imperfect information. We show that the algorithm can be used to solve games of imperfect information defined by (discrete-time) retcangular automata. In [2], we extend the result to omega-regular objectives and we consider randomized strategies. We give an algorithm for computing the set of states from which a player can win with probability 1 for a Büchi objective. An algorithm that constructs a winning strategy using antichains is presented in [3] for parity games with imperfect information.

  •  Implementation: a prototype has been implemented in HyTech.
  •  Papers:
    [1] Martin De Wulf, Laurent Doyen, Jean-François Raskin. A Lattice Theory for Solving Games of Imperfect Information. Proceedings of HSCC 2006, LNCS 3927, Springer-Verlag, Santa Barbara, 2006.
    [2] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger and Jean-François Raskin. Algorithms for Omega-regular games of Incomplete Information (extended version). Logical Methods in Computer Science 3(3:4), 2007.
    [3] Dietmar Berwanger, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger and Sangram Raje. Strategy construction for parity games with imperfect information. Proceedings of CONCUR 2008, LNCS, Springer-Verlag, Toronto, 2008.
    bib BibTex List

    Finite    Finite word automata


    We propose in [4] antichain-based algorithms for checking universality and language inclusion for finite word automata. Experiments show excellent performances of the algorithm for universality: we can analyze automata with 5000 states while previous tools were limited to 200 states.

    •  Implementation: a symbolic (BDD-based) model-checker has been implemented. See the tool Alaska.
    •  Papers:
    •  Slides: Antichains: A New Algorithm for Checking Universality of Finite Automata (PDF)
      • [4] Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-François Raskin. Antichains: A New Algorithm for Checking Universality of Finite Automata. Proceedings of CAV 2006, LNCS 4144, Springer-Verlag, Seattle, 2006.
      bib BibTex List

      Infinite    Infinite words and Linear Temporal Logic (LTL)


      We propose in [5] antichain-based algorithms for checking universality and language inclusion for Büchi automata. Experiments show excellent performances of the algorithm for universality: we can analyze automata with roughly 120 states while previous tools were limited to roughly 10 states. We apply these algorihms to attack the satisfiability and model-chekcing of LTL in [6].

      •  Implementation: Enumerative and symbolic (BDD-based) model-checkers have been implemented. See the tool Alaska.
      •  mh: a prototype for checking universality of nondeterministic Büchi automata (NBW).
      •  Papers:
      •  Slides: Improved algorithms for the automata based approach to model-checking (PDF)
        • [5] Laurent Doyen and Jean-François Raskin. Improved algorithms for the automata based approach to model-checking. Proceedings of TACAS 2007, LNCS 4424, Springer-Verlag, Braga, 2007.
        [6] Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-François Raskin. Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking. Proceedings of TACAS 2008, LNCS 4693, Springer-Verlag, Budapest, 2008.
        [7] Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-François Raskin. Alaska: antichains for logic, automata and symbolic Kripke structures analysis. Proceedings of ATVA 2008, LNCS, Springer-Verlag, Seoul, 2008.
        bib BibTex List

        Tree    Tree automata


        Ongoing work.

        People    People


        Krishnendu Martin Laurent Tom Nicolas JF
        Krishnendu Chatterjee Martin De Wulf Laurent Doyen Thomas A. Henzinger Nicolas Maquet Jean-François Raskin



        		The Verification Group at Université Libre de Bruxelles.


        Link       Related works


        • dk.brics.automaton, a tool for extended regular expressions, University of Aarhus.
        • reAnimator, Visualizing Regular Expressions, Oliver Steele.
        • LTL2BA, LTL to Büchi automata translator, LIAFA - Paris 7
        • GOAL, Graphical Tool for Omega-Automata and Logics, National Taiwan University.

        Link       Other related publications


        Automata Theory

        • A. Bouajjani, P. Habermehl, L. Holik, T. Touili, and T. Vojnar. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. Proceedings of 13th International Conference on Implementation and Application of Automata (CIAA), LNCS, Springer-Verlag, San Francisco, 2008.
        • S. Klüppelholz and C. Baier. Alternating-Time Stream Logic for Multi-agent Systems. Proceedings of 10th International Conference on Coordination Models and Languages (COORDINATION), LNCS 5052, Springer-Verlag, Oslo, 2008.
        Timed Control
        • F. Cassez, A. David, K. Larsen, D. Lime, and J.-F. Raskin. Timed Control with Observation Based and Stuttering Invariant Strategies. Proceedings of 5th International Symposium on Automated Technology for Verification and Analysis (ATVA), LNCS 4762, Tokyo. 2007.
        • F. Cassez. Efficient On-the-Fly Algorithms for Partially Observable Timed Games. Proceedings of 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), LNCS 4763, Salzburg, 2007.
        • D. Del Vecchio. A Partial Order Approach to Discrete Dynamic Feedback in a Class of Hybrid Systems. Proceedings of 10th International Workshop Hybrid Systems: Computation and Control (HSCC), LNCS 4416, Springer-Verlag, Pisa, 2007.
        • P. Bouyer and F. Chevalier. On the Control of Timed and Hybrid Systems. EATCS Bulletin 89, 2006.

        Page maintained by Laurent Doyen
        Last update: Wed August 6 11:04 CEST 2008
        Antichain
        Statistics