Runtime monitors for Markov decision processes

DOI10.1007/978-3-030-81688-9_26zbMATH Open1493.68214arXiv2105.12322OpenAlexW3184761245MaRDI QIDQ832291FDOQ832291

Authors: Sebastian Junges, Hazem Torfah, Sanjit A. Seshia 

Publication date: 25 March 2022

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.

Full work available at URL: https://arxiv.org/abs/2105.12322

Recommendations

• Selective monitoring
• Selective monitoring
• Monitoring the Full Range of ω-Regular Properties of Stochastic Systems
• On the expressiveness and complexity of randomization in finite state monitors
• Verification and control of partially observable probabilistic systems

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40)

Cites Work

• An overview of the runtime verification tool Java PathExplorer
• Probabilistic black-box reachability checking (extended version)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Optimal cost almost-sure reachability in POMDPs
• The Complexity of Markov Decision Processes
• The quickhull algorithm for convex hulls
• Relationships between nondeterministic and deterministic tape complexities
• Title not available (Why is that?)
• Active Diagnosis for Probabilistic Systems
• Title not available (Why is that?)
• Partial-Observation Stochastic Games
• Algorithmic analysis of nonlinear hybrid systems
• Formal Modeling and Analysis of Timed Systems
• Model-based testing of probabilistic systems
• Verification and control of partially observable probabilistic systems
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Optimistic value iteration
• A tale of two diagnoses in probabilistic systems
• Interval iteration algorithm for MDPs and IMDPs
• Permissive Controller Synthesis for Probabilistic Systems
• Distinguishing Hidden Markov Chains
• Title not available (Why is that?)
• Title not available (Why is that?)
• Shield Synthesis:
• Monitoring Temporal Properties of Stochastic Systems
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Run-time optimization for learned controllers through quantitative games

Cited In (6)

• Monitoring \(k\)th order runs in binary processes
• Theoretical Aspects of Computing - ICTAC 2004
• Monitoring the Full Range of ω-Regular Properties of Stochastic Systems
• A practitioner's guide to MDP model checking algorithms
• Monitoring algorithmic fairness
• On probabilistic monitorability

Uses Software

• Qhull
• z3
• prob-black-reach

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)