\textsf{PrIC3}: property directed reachability for MDPs

DOI10.1007/978-3-030-53291-8_27MaRDI QIDQ2226756zbMATH OpenOpenAlexFDO

Authors Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Philipp Schröer, Joost-Pieter Katoen

Publication date 9 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2004.14835

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Markov and semi-Markov decision processes (90C40)

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.

Recommendations

• Generalized property directed reachability
• scientific article; zbMATH DE number 2080040
• scientific article; zbMATH DE number 2087806
• Understanding IC3
• Property directed abstract interpretation

Cited in

(9)

• Abstraction-based incremental inductive coverability for Petri nets
• Out of control: reducing probabilistic models by control-state elimination
• Generalized property directed reachability
• Symbolic verification and strategy synthesis for turn-based stochastic games
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis
• Exploiting adjoints in property directed reachability analysis
• Probabilistic program verification via inductive synthesis of inductive invariants
• Adjointness in property directed reachability analysis
• Latticed \(k\)-induction with an application to probabilistic programs

Describes a project that uses

Uses Software

• iscasMc

This page was built for publication: \textsf{PrIC3}: property directed reachability for MDPs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2226756)