Abstract
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.
Cite
CITATION STYLE
Batz, K., Junges, S., Kaminski, B. L., Katoen, J. P., Matheja, C., & Schröer, P. (2020). PrIC3: Property Directed Reachability for MDPs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12225 LNCS, pp. 512–538). Springer. https://doi.org/10.1007/978-3-030-53291-8_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
