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 . 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.

@inproceedings{HoltzenCAV21,
	author    = {Holtzen, Steven and Junges, Sebastian and Vazquez-Chanlatte, Marcell and Millstein, Todd and Seshia, Sanjit A. and Van den Broeck, Guy},
	title     = {Model Checking Finite-Horizon Markov Chains with Probabilistic Inference},
    booktitle = {Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV)},
    month   = 7,
    year    = {2021},
    url     = "http://starai.cs.ucla.edu/papers/HoltzenCAV21.pdf",
    keywords  = {conference,selective}
}