Model Checking Finite-Horizon Markov Chains with Probabilistic Inference

Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd D. Millstein, Sanjit A. Seshia, and Guy Van den Broeck. Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. In 33rd International Conference on Computer Aided Verification (CAV), pp. 577–601, Lecture Notes in Computer Science 12760, Springer, 2021.

Download

[HTML] 

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.

BibTeX

@inproceedings{holtzen-cav21,
  author    = {Steven Holtzen and
               Sebastian Junges and
               Marcell Vazquez{-}Chanlatte and
               Todd D. Millstein and
               Sanjit A. Seshia and
               Guy Van den Broeck},
  title     = {Model Checking Finite-Horizon Markov Chains with Probabilistic Inference},
  booktitle = {33rd International Conference on Computer Aided Verification (CAV)},
  series    = {Lecture Notes in Computer Science},
  volume    = {12760},
  pages     = {577--601},
  publisher = {Springer},
  year      = {2021},
  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.},
}