|
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. |
|
BibTex List |
|
|
|
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:
|
|
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:
[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.
|
|
BibTex List |
- Slides:
Improved algorithms for the automata based approach to model-checking (PDF)
|
|
|
Tree automata
|
|
|
People
|
|
|
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.
|
|
|
|
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.
|
|
| | |