Exploiting adjoints in property directed reachability analysis

DOI10.1007/978-3-031-37703-7_3MaRDI QIDQ6535527zbMATH OpenFDO

Authors Flavio Ascari, Filippo Bonchi, Roberto Bruni, Roberta Gori, Ichiro Hasuo

Publication date 12 January 2024

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

lattice theoryadjointsMDPsover-approximationPDR

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• The Lattice-Theoretic Essence of Property Directed Reachability Analysis
• Property directed polyhedral abstraction
• Property directed abstract interpretation
• scientific article; zbMATH DE number 1884411
• Generalized property directed reachability

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 1759702 (Why is no real title available?)
• scientific article; zbMATH DE number 195199 (Why is no real title available?)
• scientific article; zbMATH DE number 2120508 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Ensuring the reliability of your model checker: interval iteration for Markov decision processes
• Generalized property directed reachability
• Making abstract interpretations complete
• Optimistic value iteration
• Principles of abstract interpretation
• Property directed reachability for automated planning
• SAT-Based Model Checking without Unrolling
• Sound up-to techniques and complete abstract domains
• Sound value iteration
• The Lattice-Theoretic Essence of Property Directed Reachability Analysis
• \textsf{PrIC3}: property directed reachability for MDPs

This page was built for publication: Exploiting adjoints in property directed reachability analysis

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