Games on Probabilistic Timed Automata

Abstract.

Two-player zero-sum games on finite automata, as a mechanism for supervisory controller synthesis of discrete event systems, were introduced by Ramadge and Wonham. In this setting the two players---called Min and Max---represent the `controller' and the `environment' and control-program synthesis corresponds to finding a winning (or optimal) strategy of the `controller' for some given performance objective. If the objectives are dependent on time, e.g. when the objective corresponds to completing a given set of tasks within some deadline, then games on timed automata are a well-established approach for controller synthesis.
In this talk we discuss an extension of this approach to systems which are quantitative in terms of time and probabilistic behaviour. Probabilistic information is important for modelling, e.g., faulty or unreliable components, the random coin flips of distributed communication and security protocols, and performance characteristics. We consider games on probabilistic timed automata, a modelling framework for real-time systems exhibiting both nondeterministic and probabilistic behaviour. We concentrate on expected reachability-time games, where the performance objective concerns the expected minimum time the controller can ensure for the system to reach a target, regardless of uncontrollable (environmental) events. This approach has many practical applications, including job-shop scheduling, where machines can be faulty or have variable execution times, and both routing and task graph scheduling problems, where both time and stochastic behaviour is also relevant. We also discuss discounted-time games where, intuitively, at each transition the system breaks down with some non-zero probability, and the players try to optimise the expected time to breakdown.

Relevant Papers.