Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

DOI10.1016/j.tcs.2005.07.022zbMath1081.90066OpenAlexW2152342144WikidataQ57801899 ScholiaQ57801899MaRDI QIDQ2575731

Christel Baier, Holger Hermanns, Boudewijn R. Haverkort, Joost-Pieter Katoen

Publication date: 6 December 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://research.utwente.nl/en/publications/efficient-computation-of-timebounded-reachability-probabilities-in-uniform-continuoustime-markov-decision-processes(bf215a64-e175-4e6e-a41d-451af9663a37).html

zbMATH Keywords

Markov decision processModel checkingTemporal logicContinuous-timeTime-bounded reachability

Mathematics Subject Classification ID

Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ Time-Bounded Verification ⋮ Optimal decisions for continuous time Markov decision processes over finite planning horizons ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Precisely deciding CSL formulas through approximate model checking for CTMCs ⋮ A Tutorial on Interactive Markov Chains ⋮ Computing Behavioral Relations for Probabilistic Concurrent Systems ⋮ Numerical analysis of continuous time Markov decision processes over finite horizons ⋮ Deciding Simulations on Probabilistic Automata ⋮ A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains ⋮ Efficient computation of the bounds of continuous time imprecise Markov chains ⋮ Three-valued abstraction for probabilistic systems ⋮ Engineering constraint solvers for automatic analysis of probabilistic hybrid automata ⋮ Delayed Nondeterminism in Continuous-Time Markov Decision Processes ⋮ Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates ⋮ Probabilistic model checking of biological systems with uncertain kinetic rates ⋮ Compositional Abstraction for Stochastic Systems ⋮ Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games ⋮ Model checking for performability ⋮ Efficient approximation of optimal control for continuous-time Markov games ⋮ Smoothed model checking for uncertain continuous-time Markov chains

Uses Software

• PRISM

Cites Work

• Interactive Markov chains. And the quest for quantified quality
• Model-checking large structured Markov chains.
• Model checking of probabilistic and nondeterministic systems
• Uniformization for semi-Markov decision processes under stationary policies
• Sequencing Tasks with Exponential Service Times to Minimize the Expected Flow Time or Makespan
• Exact and ordinary lumpability in finite Markov chains
• Tools and Algorithms for the Construction and Analysis of Systems
• Model-checking continuous-time Markov chains
• CONCUR 2003 - Concurrency Theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item