PrIC3: Property Directed Reachability for MDPs

2020/04/30 by Batz, Kevin, Junges, Sebastian, Kaminski, Benjamin Lucien +3 · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2004.14835

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.

Cited by

• Property-driven Causal Abstractions for Markov Decision Processes

Related

• Property Directed Reachability with Extended Resolution
• Symbolic Reachability Analysis of B through ProB and LTSmin
• Verifying Reachability Properties in Markov Chains via Incremental Induction
• Multi-core and/or Symbolic Model Checking
• The model checking fingerprints of CTL operators