论文标题
PRIC3：MDP的属性指示可达性
PrIC3: Property Directed Reachability for MDPs
论文作者
论文摘要
IC3一直是符号模型检查中的飞跃。本文提出了Pric3（发音为Pricy-Three），这是IC3的保守扩展到MDP的符号模型检查。我们的主要重点是发展基础Pric3的理论。除了，我们提出了PRIC3的首次实现，包括来自IC3的关键成分，例如概括，恢复和传播。
IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our main focus is to develop the theory underlying PrIC3. Alongside, we present a first implementation of PrIC3 including the key ingredients from IC3 such as generalization, repushing, and propagation.
