Computing minimum and maximum reachability times in probabilistic systems
From MaRDI portal
This work considers the classes of stochastic shortest path problems in which the costs are all non-negative or all non-positive. The paper presents efficient methods for solving those two problems based on algorithms to transform the original problems into problems that satisfy the required assumptions. The methods lead to the computation of the minimum probability of reaching a target set and the computation of the minimum expected time to reach the set. For the entire collection see [Zbl 0921.00028].
Recommendations
- Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
- Tools and Algorithms for the Construction and Analysis of Systems
- scientific article; zbMATH DE number 1884411
- scientific article; zbMATH DE number 1324653
- Finite-horizon bisimulation minimisation for probabilistic systems
- Formal Modeling and Analysis of Timed Systems
- A stochastic approximation method for reachability computations
- scientific article; zbMATH DE number 1864589
- Extended Directed Search for Probabilistic Timed Reachability
- Validation of Stochastic Systems
Cited in
(30)- Automatic verification of real-time systems with discrete probability distributions.
- Computation tree measurement language (CTML)
- Categorical foundations for randomly timed automata
- Probabilistic reach-avoid problems in nondeterministic systems with time-varying targets and obstacles
- Automatic verification of concurrent stochastic systems
- Automatic verification of competitive stochastic systems
- Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
- Nearly optimal verifiable data streaming
- A Tutorial on Interactive Markov Chains
- Symbolic minimum expected time controller synthesis for probabilistic timed automata
- Concavely-Priced Probabilistic Timed Automata
- Maximizing the conditional expected reward for reaching the goal
- Play to Test
- Probabilistic Verification of Uncertain Systems Using Bounded-Parameter Markov Decision Processes
- scientific article; zbMATH DE number 1884411 (Why is no real title available?)
- Energy-utility analysis for resilient systems using probabilistic model checking
- Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
- Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games
- Percentile queries in multi-dimensional Markov decision processes
- Formal Modeling and Analysis of Timed Systems
- A game-based abstraction-refinement framework for Markov decision processes
- On probability-raising causality in Markov decision processes
- Foundations of probability-raising causality in Markov decision processes
- Equilibria-based probabilistic model checking for concurrent stochastic games
- On Skolem-hardness and saturation points in Markov decision processes
- Risk-averse optimization of total rewards in Markovian models using deviation measures
- Demonic variance and a non-determinism score for Markov decision processes
- State explosion in almost-sure probabilistic reachability
- Performance analysis of probabilistic timed automata using digital clocks
- Parametric probabilistic transition systems for system design and analysis
This page was built for publication: Computing minimum and maximum reachability times in probabilistic systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4270052)
