Expected reachability-time games
From MaRDI portal
Abstract: Probabilistic timed automata are a suitable formalism to model systems with real-time, nondeterministic and probabilistic behaviour. We study two-player zero-sum games on such automata where the objective of the game is specified as the expected time to reach a target. The two players---called player Min and player Max---compete by proposing timed moves simultaneously and the move with a shorter delay is performed. The first player attempts to minimise the given objective while the second tries to maximise the objective. We observe that these games are not determined, and study decision problems related to computing the upper and lower values, showing that the problems are decidable and lie in the complexity class NEXPTIME co-NEXPTIME.
Recommendations
- Expected reachability-time games
- Reachability in Stochastic Timed Games
- Reachability-Time Games on Timed Automata
- Minimum-Time Reachability in Timed Games
- Timeability of extensive-form games
- Automata, Languages and Programming
- Optimal reachability in divergent weighted timed games
- Probabilistic robust timed games
- Concurrent reachability games
- Stochastic timed games revisited
Cites work
- scientific article; zbMATH DE number 1303059 (Why is no real title available?)
- scientific article; zbMATH DE number 549853 (Why is no real title available?)
- scientific article; zbMATH DE number 1134975 (Why is no real title available?)
- A theory of timed automata
- Automata, Languages and Programming
- Automatic Synthesis of Robust and Optimal Controllers – An Industrial Case Study
- Automatic verification of real-time systems with discrete probability distributions.
- Average-time games
- Checking timed Büchi automata emptiness efficiently
- Concavely-Priced Probabilistic Timed Automata
- Expected reachability-time games
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Formal Modeling and Analysis of Timed Systems
- Hybrid Systems: Computation and Control
- Improved undecidability results on weighted timed automata
- Minimum-Time Reachability in Timed Games
- Model Checking Probabilistic Timed Automata with One or Two Clocks
- Model checking for probabilistic timed automata
- On probabilistic timed automata.
- Probabilistic robust timed games
- Quantitative solution of omega-regular games
- Reachability in Stochastic Timed Games
- Reachability-Time Games on Timed Automata
- State explosion in almost-sure probabilistic reachability
- Stochastic Real-Time Games with Qualitative Timed Automata Objectives
- Symbolic minimum expected time controller synthesis for probabilistic timed automata
- Symbolic model checking for probabilistic timed automata
- The complexity of mean payoff games on graphs
- The complexity of stochastic games
- Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata
- Value Iteration
- Verification of open interactive Markov chains
- What good are digital clocks?
Cited in
(10)- Stochastic timed games revisited
- Verification and control for probabilistic hybrid automata with finite bisimulations
- Expected reachability-price games
- Expected reachability-time games
- On time with minimal expected cost!
- Minimum-Time Reachability in Timed Games
- Reachability-Time Games on Timed Automata
- Reachability in Stochastic Timed Games
- Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
- Reachability Switching Games
This page was built for publication: Expected reachability-time games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q278757)
