This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
Dense Real-Time Games
Copenhagen, Denmark
July 22-July 25
ISBN: 0-7695-1483-9
Marco Faella, Università degli Studi di Salerno
Salvatore La Torre, Università degli Studi di Salerno and University of Pennsylvania
Aniello Murano, Università degli Studi di Salerno and Rice University
The rapid development of complex and safety-critical systems requires the use of reliable verification methods and tools for system design (synthesis). Many systems of interest are reactive, in the sense that their behavior depends on the interaction with the environment. A natural framework to model them is a two-player game: the system versus the environment. In this context, the central problem is to determine the existence of a winning strategy according to a given winning condition. We focus on real-time systems, and choose to model the related game as a nondeterministic timed automaton. We express winning conditions by formulas of the branching-time temporal logic TCTL. While timed games have been studied in the literature, timed games with dense-time winning conditions constitute a new research topic. The main result of this paper is an exponential-time algorithm to check for the existence of a winning strategy for TCTL games where equality is not allowed in the timing constraints. Our approach consists on translating to timed tree automata both the game graph and the winning condition, thus reducing the considered decision problem to the emptiness problem for this class of automata. The proposed algorithm matches the known lower bound on timed games. Moreover, if we relax the limitation we have placed on the timing constraints, the problem becomes undecidable.
Citation:
Marco Faella, Salvatore La Torre, Aniello Murano, "Dense Real-Time Games," lics, pp.167, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.