Efficient on-the-fly algorithms for the analysis of timed games

Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, Didier Lime

Research output: Contribution to journalConference paperpeer-review

177 Citations (Scopus)

Abstract

In this paper, we propose the 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.

Original languageEnglish
Pages (from-to)66-80
Number of pages15
JournalLecture Notes in Computer Science
Volume3653
Publication statusPublished - 2005
Externally publishedYes

Fingerprint Dive into the research topics of 'Efficient on-the-fly algorithms for the analysis of timed games'. Together they form a unique fingerprint.

Cite this