PrIC3: Property Directed Reachability for MDPs

Kevin Batz; Sebastian Junges; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja; Philipp Schröer

doi:10.1007/978-3-030-53291-8_27

CAV2020顶会

PrIC3: Property Directed Reachability for MDPs

Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer

arXiv DOI 出版方

2020年份

15被引次数

6顶会引用

摘要

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.