PrIC3: Property Directed Reachability for MDPs
Not on the map. Why?
Abstract (arXiv)
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.
Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). First posted on arXiv 30 Apr 2020.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2026: 1.
1 paper.