Automata-theoretic decision of timed games (Q386611): Difference between revisions

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\).