Automata-theoretic decision of timed games
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)].NEWLINENEWLINEFor 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.NEWLINENEWLINENo implementation or experimental results are reported either in the paper or in papers I found citing the preliminary version.NEWLINENEWLINEThere 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.NEWLINENEWLINEFinally, 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\).
- A theory of timed automata
- Alternating-time temporal logic
- ATL with strategy contexts: expressiveness and model checking
- Automatic synthesis of switching controllers for linear hybrid systems: safety control
- Computer Aided Verification
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Decision problems for lower/upper bound parametric timed automata
- Deterministic generators and games for LTL fragments
- Enriched MU-Calculi Module Checking
- Finite automata on timed \(\omega\)-trees
- Formal Modeling and Analysis of Timed Systems
- scientific article; zbMATH DE number 3492660 (Why is no real title available?)
- scientific article; zbMATH DE number 1303059 (Why is no real title available?)
- scientific article; zbMATH DE number 1361131 (Why is no real title available?)
- scientific article; zbMATH DE number 1142314 (Why is no real title available?)
- scientific article; zbMATH DE number 2080198 (Why is no real title available?)
- scientific article; zbMATH DE number 1775458 (Why is no real title available?)
- scientific article; zbMATH DE number 2086509 (Why is no real title available?)
- scientific article; zbMATH DE number 3106184 (Why is no real title available?)
- Model-checking in dense real-time
- Modular strategies for recursive game graphs
- Module checking
- O-minimal hybrid reachability games
- On the synthesis of strategies in infinite games
- Optimal bounds in parametric LTL games
- Optimal paths in weighted timed automata
- Parametric Metric Interval Temporal Logic
- Parametric temporal logic for “model measuring”
- Program Complexity in Hierarchical Module Checking
- Pushdown module checking
- Pushdown module checking with imperfect information
- Reachability-Time Games on Timed Automata
- Reasoning about infinite computations
- Reasoning about strategies
- Robust reachability in timed automata: a game-based approach
- Strategy logic
- Timed tree automata with an application to temporal logic.
- Using branching time temporal logic to synthesize synchronization skeletons
- What makes \textsc{Atl}* decidable? A decidable fragment of strategy logic
- A game approach to determinize timed automata
- A game approach to determinize timed automata
- Combining symbolic representations for solving timed games
- scientific article; zbMATH DE number 6862072 (Why is no real title available?)
- scientific article; zbMATH DE number 2086509 (Why is no real title available?)
- A unifying approach to decide relations for timed automata and their game characterization
- Reachability-Time Games on Timed Automata
This page was built for publication: Automata-theoretic decision of timed games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q386611)
