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.
翻译:我们重新审视了Markov链条对有限地平线可达性特性的象征性核查。 流行的方法迭代地计算了分步测距的可达性概率。 相反, 最近的概率推论进展表明, 符号性地代表了通过Markov链条的所有地平线长路径。 我们问这个观点是否在概率模型检查中提高了最先进的水平。 首先, 我们正式描述这两种方法, 以突出它们的关键差异。 然后, 我们利用这些洞察力开发了Rubicon, 这个工具可以将Prism模型转换为概率推论工具 Dice。 最后, 我们展示了比选定基准的概率模型检验器更好的可伸缩性。 总之, 我们的结果表明, 概率推论是对概率模型组合核对的有价值的补充 -- 用Rubicon作为将两种观点结合起来的第一步。