Batz, K;
Junges, S;
Kaminski, BL;
Katoen, J-P;
Matheja, C;
Schröer, P;
(2020)
PrIC3: Property Directed Reachability for MDPs.
In:
International Conference on Computer Aided Verification CAV 2020: Computer Aided Verification.
(pp. pp. 512-538).
Springer, Cham
Preview |
Text
Kaminski_Batz2020_Chapter_PrIC3PropertyDirectedReachabil.pdf - Published Version Download (791kB) | Preview |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | PrIC3: Property Directed Reachability for MDPs |
| Event: | 32nd International Conference on Computer-Aided Verification (CAV 2020) |
| Location: | online |
| Dates: | 21 July 2020 - 24 July 2020 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-53291-8_27 |
| Publisher version: | https://doi.org/10.1007/978-3-030-53291-8_27 |
| Language: | English |
| Additional information: | This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. |
| Keywords: | PDR, IC3, Property Directed Reachability, MDPs, Markov Decision Processes, probabilistic model checking, quantitative reachability |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10097743 |
Archive Staff Only
 |
View Item |
