Runtime monitors for Markov decision processes
From MaRDI portal
(Redirected from Publication:832291)
Abstract: We investigate the problem of monitoring partially observable systems with nondeterministic and probabilistic dynamics. In such systems, every state may be associated with a risk, e.g., the probability of an imminent crash. During runtime, we obtain partial information about the system state in form of observations. The monitor uses this information to estimate the risk of the (unobservable) current system state. Our results are threefold. First, we show that extensions of state estimation approaches do not scale due the combination of nondeterminism and probabilities. While convex hull algorithms improve the practical runtime, they do not prevent an exponential memory blowup. Second, we present a tractable algorithm based on model checking conditional reachability probabilities. Third, we provide prototypical implementations and manifest the applicability of our algorithms to a range of benchmarks. The results highlight the possibilities and boundaries of our novel algorithms.
Recommendations
Cites work
- scientific article; zbMATH DE number 700091 (Why is no real title available?)
- scientific article; zbMATH DE number 2107836 (Why is no real title available?)
- scientific article; zbMATH DE number 7559459 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 2238781 (Why is no real title available?)
- A survey of challenges for runtime verification from advanced application domains (beyond software)
- A tale of two diagnoses in probabilistic systems
- Active Diagnosis for Probabilistic Systems
- Algorithmic analysis of nonlinear hybrid systems
- An overview of the runtime verification tool Java PathExplorer
- Distinguishing hidden Markov chains
- Formal Modeling and Analysis of Timed Systems
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- Interval iteration algorithm for MDPs and IMDPs
- Model-based testing of probabilistic systems
- Monitoring Temporal Properties of Stochastic Systems
- Optimal cost almost-sure reachability in POMDPs
- Optimistic value iteration
- Partial-observation stochastic games, how to win when belief fails
- Permissive controller synthesis for probabilistic systems
- Probabilistic black-box reachability checking (extended version)
- Relationships between nondeterministic and deterministic tape complexities
- Run-time optimization for learned controllers through quantitative games
- Selective monitoring
- Shield synthesis: runtime enforcement for reactive systems
- The Complexity of Markov Decision Processes
- The quickhull algorithm for convex hulls
- Verification and control of partially observable probabilistic systems
Cited in
(10)- Monitoring the Full Range of ω-Regular Properties of Stochastic Systems
- Monitoring of perception systems: deterministic, probabilistic, and learning-based fault detection and identification
- Monitoring \(k\)th order runs in binary processes
- A practitioner's guide to MDP model checking algorithms
- Monitoring algorithmic fairness
- Selective monitoring
- Theoretical Aspects of Computing - ICTAC 2004
- On probabilistic monitorability
- Timely monitoring of partially observable stochastic systems
- Selective monitoring
This page was built for publication: Runtime monitors for Markov decision processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832291)
