Model checking finite-horizon Markov chains with probabilistic inference
From MaRDI portal
Publication:832295
DOI10.1007/978-3-030-81688-9_27zbMATH Open1493.68210arXiv2105.12326OpenAlexW3184096451MaRDI QIDQ832295FDOQ832295
Steven Holtzen, Sanjit A. Seshia, Guy Van den Broeck, Marcell Vazquez-Chanlatte, Todd D. Millstein, Sebastian Junges
Publication date: 25 March 2022
Abstract: We revisit the symbolic verification of Markov chains with respect to finite horizon reachability properties. The prevalent approach iteratively computes step-bounded state reachability probabilities. By contrast, recent advances in probabilistic inference suggest symbolically representing all horizon-length paths through the Markov chain. We ask whether this perspective advances the state-of-the-art in probabilistic model checking. First, we formally describe both approaches in order to highlight their key differences. Then, using these insights we develop Rubicon, a tool that transpiles Prism models to the probabilistic inference tool Dice. Finally, we demonstrate better scalability compared to probabilistic model checkers on selected benchmarks. All together, our results suggest that probabilistic inference is a valuable addition to the probabilistic model checking portfolio -- with Rubicon as a first step towards integrating both perspectives.
Full work available at URL: https://arxiv.org/abs/2105.12326
Recommendations
- Bayesian inference by symbolic model checking
- Finite horizon analysis of Markov chains with the Mur\(\varphi \) verifier
- scientific article; zbMATH DE number 2080040
- Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
- Finite-horizon bisimulation minimisation for probabilistic systems
Computational methods in Markov chains (60J22) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Probabilistic graphical models.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theoretical Aspects of Computing - ICTAC 2004
- On probabilistic inference by weighted model counting
- Title not available (Why is that?)
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Probabilistic self-stabilization
- Semantics of probabilistic programs
- Inference and learning in probabilistic logic programs using weighted Boolean formulas
- Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems
- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking
- Symmetry Reduction for Probabilistic Model Checking
- Probabilistic verification of Herman's self-stabilisation algorithm
- Bayesian inference by symbolic model checking
- A game-based abstraction-refinement framework for Markov decision processes
- Symbolic model checking for factored probabilistic models
- Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
- Maximum causal entropy specification inference from demonstrations
- How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times
- Model Checking Probabilistic Systems
- Understanding Probabilistic Programs
- Verification of Markov Decision Processes Using Learning Algorithms
- Scenario-Based Verification of Uncertain MDPs
- Title not available (Why is that?)
- Bridging the Gap Between Probabilistic Model Checking and Probabilistic Planning: Survey, Compilations, and Empirical Comparison
- Conditional Probabilities over Probabilistic and Nondeterministic Systems
Cited In (9)
- Model checking hyperproperties for Markov decision processes
- Parameter synthesis for Markov models: covering the parameter space
- Automatically finding the right probabilities in Bayesian networks
- Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- Incremental Verification of Parametric and Reconfigurable Markov Chains
- Parameter synthesis in Markov models: a gentle survey
- Probabilistic program verification via inductive synthesis of inductive invariants
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
Uses Software
This page was built for publication: Model checking finite-horizon Markov chains with probabilistic inference
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832295)
