Automata-theoretic decision of timed games (Q386611): Difference between revisions
From MaRDI portal
Changed an Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 04:17, 30 January 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Automata-theoretic decision of timed games |
scientific article |
Statements
Automata-theoretic decision of timed games (English)
0 references
10 December 2013
0 references
This paper presents automata-theoretic decision procedures for timed games with winning conditions given in either (untimed) CTL or (untimed) LTL. It extends the preliminary version [\textit{M. Faella} et al., Lect. Notes Comput. Sci. 2294, 94--108 (2002; Zbl 1057.68057)]. For a CTL winning condition a winning strategy exists iff the intersection of two tree automata is not empty. The first automaton accepts representative samples of strategies. The second automaton accepts trees that fulfill the given winning condition. The number of existential quantifiers in the winning condition is used to limit the branching degree in both automata. The procedure for LTL winning conditions is based on the same principle, but somewhat simpler as the branching degree of the automata can be limited independent of the winning condition. The complexities of both procedures match known lower complexity bounds. No implementation or experimental results are reported either in the paper or in papers I found citing the preliminary version. There is a paper [\textit{M. Faella} et al., ``Dense real-time games'', in: Proceedings of the 17th annual IEEE symposium on logic in computer science, LICS 2002, Copenhagen, Denmark, 2002. IEEE, 167--176 (2002)] by the same authors that uses part of the ideas in this paper for decision of timed CTL objectives for timed games. Finally, there is a small mistake in Example 1/Figure 2. If the dashed edge is removed, then \(r'\) cannot be reached: in \(r\) we have that \(0 < x < y < z < 1\), on the edges we have either \(x = 2\) or \(y = 2\) (hence, \(z > 2\)), but in \(r'\) it is required that \(1 < z < 2\).
0 references
timed games
0 references
temporal logic
0 references
tree automata
0 references