
We propose in [1] an antichainbased algorithm for solving safety games
of imperfect information. We show that the algorithm can be used to solve
games of imperfect information defined by (discretetime) retcangular automata.
In [2], we extend the result to omegaregular 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, JeanFrançois Raskin.
A Lattice Theory for Solving Games of Imperfect Information.
Proceedings of HSCC 2006, LNCS 3927, SpringerVerlag, Santa Barbara, 2006. 
[2] 
Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger and JeanFrançois Raskin.
Algorithms for Omegaregular 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, SpringerVerlag, Toronto, 2008. 

BibTex List 



Finite word automata


We propose in [4] antichainbased 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 (BDDbased) modelchecker has been implemented. See the tool Alaska.
 Papers:
 Slides:
Antichains: A New Algorithm for Checking Universality of Finite Automata (PDF)


Infinite words and Linear Temporal Logic (LTL)


We propose in [5] antichainbased 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 modelchekcing of LTL in [6].
 Implementation: Enumerative and symbolic (BDDbased) modelcheckers 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 modelchecking (PDF)
[5] 
Laurent Doyen and JeanFrançois Raskin.
Improved algorithms for the automata based approach to modelchecking.
Proceedings of TACAS 2007, LNCS 4424, SpringerVerlag, Braga, 2007.

[6] 
Martin De Wulf, Laurent Doyen, Nicolas Maquet, JeanFrançois Raskin.
Antichains: Alternative Algorithms for LTL Satisfiability and ModelChecking.
Proceedings of TACAS 2008, LNCS 4693, SpringerVerlag, Budapest, 2008.

[7] 
Martin De Wulf, Laurent Doyen, Nicolas Maquet, JeanFrançois Raskin.
Alaska: antichains for logic, automata and symbolic Kripke structures analysis.
Proceedings of ATVA 2008, LNCS, SpringerVerlag, Seoul, 2008.


BibTex List 



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 OmegaAutomata and Logics, National Taiwan University.




Other related publications


Automata Theory
 A. Bouajjani, P. Habermehl, L. Holik, T. Touili, and T. Vojnar.
Antichainbased Universality and Inclusion Testing over Nondeterministic
Finite Tree Automata. Proceedings of 13th International Conference on
Implementation and Application of Automata (CIAA), LNCS, SpringerVerlag, San Francisco, 2008.
 S. Klüppelholz and C. Baier. AlternatingTime Stream Logic for
Multiagent Systems. Proceedings of 10th International Conference on
Coordination Models and Languages (COORDINATION), LNCS 5052, SpringerVerlag, 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 OntheFly 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, SpringerVerlag, Pisa, 2007.
 P. Bouyer and F. Chevalier. On the Control of Timed and Hybrid Systems.
EATCS Bulletin 89, 2006.


  