Logic in Computer Science (LICS 2002)

Paper: Dense Real-time Games (at LICS 2002)

Authors: Marco Faella Salvatore La Torre Aniello Murano

Abstract

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 in the universal fragment of the branching-time logic \tctl\ ($\forall$\tctl). The main result of this paper is an exponential-time algorithm to check for the existence of a winning strategy for $\forall$\tctl\ games where the equality is not allowed in the timing constraints. This result 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.

BibTeX

  @InProceedings{FaellaTorreMurano-DenseRealtimeGames,
    author = 	 {Marco Faella and Salvatore La Torre and Aniello Murano},
    title = 	 {Dense Real-time Games},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }