Model checking finite-horizon Markov chains with probabilistic inference

DOI10.1007/978-3-030-81688-9_27zbMath1493.68210arXiv2105.12326OpenAlexW3184096451MaRDI QIDQ832295

Steven Holtzen, Sanjit A. Seshia, Guy Van den Broeck, Marcell Vazquez-Chanlatte, Sebastian Junges, Todd D. Millstein

Publication date: 25 March 2022

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

Mathematics Subject Classification ID

Computational methods in Markov chains (60J22) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (1)

Parameter synthesis in Markov models: a gentle survey

Uses Software

• PRISM
• PASS
• ProbLog
• Stan

Cites Work

• A game-based abstraction-refinement framework for Markov decision processes
• Probabilistic self-stabilization
• Semantics of probabilistic programs
• Probabilistic verification of Herman's self-stabilisation algorithm
• Symbolic model checking for factored probabilistic models
• Bayesian inference by symbolic model checking
• 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
• On probabilistic inference by weighted model counting
• Model Checking Probabilistic Systems
• Understanding Probabilistic Programs
• Verification of Markov Decision Processes Using Learning Algorithms
• 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
• Inference and learning in probabilistic logic programs using weighted Boolean formulas
• Scenario-Based Verification of Uncertain MDPs
• Bridging the Gap Between Probabilistic Model Checking and Probabilistic Planning: Survey, Compilations, and Empirical Comparison
• Conditional Probabilities over Probabilistic and Nondeterministic Systems
• Theoretical Aspects of Computing - ICTAC 2004
• Symmetry Reduction for Probabilistic Model Checking
• Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking finite-horizon Markov chains with probabilistic inference