PrIC3: Property Directed Reachability for MDPs

Lecture notes in computer science, pp. 512–538

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.

Authors 6

1. Kevin Batz corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen, University, Aachen, Germany

2. Sebastian Junges

   University of California, Berkeley

   Affiliation as printed

   University of California, Berkeley, USA

   University of California—Berkeley, USA

3. Benjamin Lucien Kaminski

   University College London

   Affiliation as printed

   University College London, London, UK

   Univ College London, London, UK

4. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen, University, Aachen, Germany

5. Christoph Matheja

   ETH Zurich

   Affiliation as printed

   ETH Zürich, Zürich, Switzerland

   ETH Zurich Zurich Switzerland

6. Philipp Schröer Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   RWTH Aachen, University, Aachen, Germany