Back to the workshop page


Weighted Timed Automata: Model-Checking and Games
Patricia Bouyer (based on joint works with Thomas Brihaye, Ed Brinksma, Véronique Bruyère, Franck Cassez, Emmanuel Fleury, Kim G. Larsen, Nicolas Markey, Jean-François Raskin, and Jacob Illum Rasmussen)

In this talk, I will present weighted/priced timed automata, an extension of timed automaton with costs, and several solutions to interesting problems on that model.



Verification and control of o-minimal hybrid systems
Thomas Brihaye (joint work with Patricia Bouyer, Fabrice Chevalier, Christian Michaux, Cédric Rivière et Christophe Troestler)

O-minimal hybrid systems enjoy rich continuous dynamics, nevertheless they admit finite bisimulation. This result was first proved in 2000 by G.Lafferriere, G.J.Pappas and S.Sastry. In this talk, we will show how finite words can be used in order to encode symbolically trajectories of o-minimal hybrid systems. We will see that this words encoding technique can help when studying o-minimal hybrid systems (i) to obtain a new proof of the existence of a finite bisimulation; (ii) to study control (reachability) problem.



Monitoring and Fault-Diagnosis with Digital Clocks
Franck Cassez (joint work with Karine Altisen and Stavros Tripakis)

We study the monitoring and fault-diagnosis problems for dense-time real-time systems, where observers (moni- tors and diagnosers) have access to digital rather than ana- log clocks. Analog clocks are infinitely-precise, thus, not implementable. We show how, given a specification mod- eled as a timed automaton and a timed automaton model of the digital clock, a sound and optimal (i.e., as precise as possible) digital-clock monitor can be synthesized. We also show how, given plant and digital clock modeled as timed automata, we can check existence of a digital-clock diagnoser and, if one exists, how to synthesize it. Finally, we consider the problem of existence of digital-clock diag- nosers where the digital clock is unknown. We show that there are cases where a digital clock, no matter how pre- cise, does not exist, even though the system is diagnosable with analog clocks.



PHAVer: Recent developments and applications
Goran Frehse



Optimal Strategies for One-Clock Priced Timed Automata
Kim G. Larsen (joint work with Patricia Bouyer, Nicolas Markey and Jacob Illum Rasmussen)



A Lattice Theory to Solve Games of Imperfect Information
Jean-François Raskin

In this talk, I will present a fixed point theory to solve games of imperfect information. The fixed point theory is defined on the lattice of antichains of sets of states. Contrary to the classical solution proposed by Reif, the new solution does not involve determinization. As a consequence, it is readily applicable to classes of systems that do not admit determinization. Notable examples of such systems are timed and hybrid automata. As an application, I will show that the discrete control problem for games of imperfect information defined by rectangular automata is decidable. This result extends a result by Henzinger and Kopke. Finally, I will also show that the ideas underlying the new algorithms can be applied to solve classical problems of automata on finite words.


The CORTOS project webpage
Last modified: Mon Aug 21 18:11:18 CEST 2006