|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| 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
| ASCII Text | x | ||
| Marco Faella, Salvatore La Torre, Aniello Murano, "Dense Real-Time Games," Logic in Computer Science, Symposium on, pp. 167, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2002.1029826, author = {Marco Faella and Salvatore La Torre and Aniello Murano}, title = {Dense Real-Time Games}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2002}, issn = {1043-6871}, pages = {167}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029826}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - Dense Real-Time Games SN - 1043-6871 SP EP A1 - Marco Faella, A1 - Salvatore La Torre, A1 - Aniello Murano, PY - 2002 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
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.
