PrIC3: Property Directed Reachability for MDPs

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 th...

Descripción completa

Detalles Bibliográficos
Autores principales: Batz, Kevin, Junges, Sebastian, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Matheja, Christoph, Schröer, Philipp
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363441/
http://dx.doi.org/10.1007/978-3-030-53291-8_27
_version_ 1783559655943831552
author Batz, Kevin
Junges, Sebastian
Kaminski, Benjamin Lucien
Katoen, Joost-Pieter
Matheja, Christoph
Schröer, Philipp
author_facet Batz, Kevin
Junges, Sebastian
Kaminski, Benjamin Lucien
Katoen, Joost-Pieter
Matheja, Christoph
Schröer, Philipp
author_sort Batz, Kevin
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7363441
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73634412020-07-16 PrIC3: Property Directed Reachability for MDPs Batz, Kevin Junges, Sebastian Kaminski, Benjamin Lucien Katoen, Joost-Pieter Matheja, Christoph Schröer, Philipp Computer Aided Verification Article 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. 2020-06-16 /pmc/articles/PMC7363441/ http://dx.doi.org/10.1007/978-3-030-53291-8_27 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Batz, Kevin
Junges, Sebastian
Kaminski, Benjamin Lucien
Katoen, Joost-Pieter
Matheja, Christoph
Schröer, Philipp
PrIC3: Property Directed Reachability for MDPs
title PrIC3: Property Directed Reachability for MDPs
title_full PrIC3: Property Directed Reachability for MDPs
title_fullStr PrIC3: Property Directed Reachability for MDPs
title_full_unstemmed PrIC3: Property Directed Reachability for MDPs
title_short PrIC3: Property Directed Reachability for MDPs
title_sort pric3: property directed reachability for mdps
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363441/
http://dx.doi.org/10.1007/978-3-030-53291-8_27
work_keys_str_mv AT batzkevin pric3propertydirectedreachabilityformdps
AT jungessebastian pric3propertydirectedreachabilityformdps
AT kaminskibenjaminlucien pric3propertydirectedreachabilityformdps
AT katoenjoostpieter pric3propertydirectedreachabilityformdps
AT mathejachristoph pric3propertydirectedreachabilityformdps
AT schroerphilipp pric3propertydirectedreachabilityformdps

Ejemplares similares