Efficient On-the-Fly Algorithms for the Analysis of Timed Games. Cassez, F., David, A., Fleury, E., Larsen, K. G., & Lime, D. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653, of Lecture Notes in Computer Science, pages 66–80, 2005. Springer.
Efficient On-the-Fly Algorithms for the Analysis of Timed Games [pdf]Paper  Efficient On-the-Fly Algorithms for the Analysis of Timed Games [pdf]Slides  Efficient On-the-Fly Algorithms for the Analysis of Timed Games [link]Link  doi  abstract   bibtex   1 download  
In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure. Various optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.

Downloads: 1