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