Kim G. Larsen

CISS, Department of Computer Science, Aalborg University, Denmark.

Time: Thursday 20.4.2005, 14:30
Place: Room A4-106, Fr. Bajersvej 7

UPPAAL Tiga: Efficient Controller Synthesis of Timed Systems

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.