Time: Thursday 20.4.2005, 14:30
Place: Room A4-106, Fr. Bajersvej 7
This talk reports on on-going work with Franck Cassez, Alexandre David,
Emmanuel
Fleury and Didier Lime aiming at making a decisive contribution towards
efficient computation of winning strategies for timed games.
Though such games for long have been know to be decidable there is still a lack
of efficient, TRUELY on-the-fly algorithms for analyising timed games. For
finite-state systems local (or on-the-fly) algorithms for model checking has
been a research topic since the beginning of the 90's, with the proposed local
algorithm by Liu&Smolka (ICALP98) being particularly elegant (and optimal).
Our work provides a zone-based symbolic extension of this finite-state
algorithm
suitable for forward, on-the-fly algorithms for solving timed games with
respect
to reachability and safety properties. The symbolic algorithm is
theoretically
optimal having worst-case complexity linear in the underlying region-graph.
However, in practice the algorithm may terminate long before having explored
the
entire state-space, as its on-the-fly nature allows the algorithm to terminate
as soon as a winning strategy has been identified. Also, the individual steps
of the algorithm are carried out efficiently by the use of zones as the
underlying datastructure.
A small extension of the algorithm permits time-optimal winning strategies (for
reachability games) to be obtained, and the very nature of the algorithm points
directly to a distributed version of the algorithm (similar to the
distributed
version of UPPAAL for reachability analysis of timed automata).
The work reported on also contains our first steps toward an efficient
implementation of the algorithm using the DBM-library of UPPAAL experimentally
evaluated on a version of the Production Cell.