Model Checking Finite-Horizon Markov Chains with Probabilistic Inference
International Conference on Computer Aided Verification (CAV 2021), July 18-24, 2021.
Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd Millstein, Sanjit A. Seshia, Guy Van den Broeck
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.
[PDF | Implementation]