D.: Efficient on-the-fly algorithms for the analysis of timed games

Abstract. In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reach-ability and safety properties1. The algorithm we propose is a symbolic extension of the on-the-fly al-gorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may ter-minate long before having explored the entire state-space. Also the in-dividual 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 reach-ability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.