UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

PrIC3: Property Directed Reachability for MDPs

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 Green open access

[img]
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 > 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
Downloads since deposit
24Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item