Program

In this talk I will present the model of weighted timed games, which is used to represent resources (like energy or cost) in timed systems. I will give an overview of the results that have been obtained these last couple of years, that concern the optimization and the management of those resources.

Like most models used in model-checking, timed automata are an ideal mathematical model to represent systems with strong timing requirements. In such mathematical models, properties can be violated, due to unlikely events. Following ideas of Varacca and Völzer in their LICS'06 paper, we aim at defining a notion of ``fair'' correctness for timed systems. For this purpose, we introduce a probabilistic semantics for timed automata, which ignores unlikely (sequence of) events, and naturally raises a notion of almost-sure satisfaction of properties in timed systems. We prove that the almost-sure satisfaction has a corresponding topological interpretation in terms of largeness of the set of paths satisfying the property. We discuss both the relation between the two semantics and the decidability of the almost-sure satisfaction for omega-regular properties. This talks is based on joint works with Christel Baier, Nathalie Bertrand, Patricia Bouyer, Marcus Groesser, Marcin Jurdzinski and Nicolas Markey.

MTL is a classical real-time extension of LTL. In MTL, the modalities are equipped with intervals over the reals, that allow to specify when the event should occur. For instance, one can specify properties such as time-bounded response: for every request, an acknowledgement will follow within t times units, where t is in [3,5]. Ouaknine and Worrell have recently proved that the model-checking of an MTL property on a system specified by an arbitrary timed automaton on finite words is decidable, when the pointwise semantics is considered. Their algorithm consists in encoding the models of the MTL property in an alternating timed automaton with one clock. Then, they show that the problem of deciding the language inclusion between a Timed automaton and a one clock alternating timed automaton is decidable. This result is obtained by further reducing the inclusion problem to a reachability problem in an infinite transition system, which is proved to be decidable by well-quasi ordering arguments. In this work, we present a prototype implementation of an MTL model checker, based on the works of Ouaknine and Worrell. The actual implementation exploits new ideas and tries to be as efficient as possible by considering successive approximations of the infinite transition system that has to be analysed to decide the inclusion. Preliminary experimental results show that this approach is promising.

The average-price (a.k.a. mean payoff) optimization has been studied since 1950's in the context of Markov decision processes and stochastic games. Solving games with the average-price payoff is well understood for finite graphs, even if its exact computational complexity is not known (it is in NP and co-NP, but no polynomial-time algorithm is known). Bellman optimality equations and strategy improvement algorithms provide elegant and constructive proofs of (positional) determinacy and decidability for average-price games on finite graphs. In this talk we discuss generalizations of those classical results to average-price games on the infinite graphs of configurations of timed and hybrid automata. We establish the following two results. 1. Games with the average-price-per-reward payoff (which is a generalization of the average-price payoff) are determined and decidable on (first-order definable) hybrid systems with strong resets. 2. Games with the average-time payoff (which is less general than the average-price payoff) are determined and EXPTIME-complete on timed automata with at least two clocks.

The semantics of timed automata assumes infinite precision and perfect synchronization of the clock variables. Therefore, properties that hold true on a timed automaton can be lost when it comes to "implementing" the timed automaton on real hardware, because these assumptions are not realizable in practice. We develop a possible approach to this problem, based on considering a relaxed semantics for timed automata. This talk is based on joint works with Patricia Bouyer, Martin De Wulf, Laurent Doyen, Jean-François Raskin and Pierre-Alain Reynier.

In this talk, I will summarize several recent works on efficient algorithms for solving the emptiness problem of alternating automata operating on finite and infinite words. I will also sketches current research questions we are working on.

We study the decidability and complexity of verification problems for timed automata over time intervals of fixed, bounded length. In particular, we investigate language inclusion for automata as well as model checking Metric Temporal Logic and monadic first- and second-order logics over the reals with order and the +1 function. We also consider the satisfiability problems for these logics and their relative expressiveness over bounded intervals. We discuss relevant applications, and compare our findings with known results in the subject. This is joint work with Alex Rabinovich and James Worrell.

In this talk we consider the complexity of the satisfiability problem for the safety fragment of Metric Temporal Logic. We relate this problem to the fair termination problem for channel machines with insertion errors, and thence to the termination of a version of the hydra game.