Timed Games with TCTL specificationsSalvatore La Torre
(latorre@dia.unisa.it) 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. In this talk, we consider timed games modeled as nondeterministic timed automata, with winning conditions given 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. We will describe an automata-theoretic approach that gives an exponential-time algorithm to check for the existence of a winning strategy in TCTL games, where equality is not allowed in the timing constraints. This approach consists of 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. (Joint work with Marco Faella and Aniello Murano) |