Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems

DOI10.1007/978-3-319-22102-1_1zbMath1465.68170OpenAlexW2109274831MaRDI QIDQ2945619

Charles Gretton, Michael Norrish, Mohammad Abdulaziz

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10072/125207

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Formally verified algorithms for upper-bounding state space diameters ⋮ A Verified Compositional Algorithm for AI Planning

Uses Software

• Nitpick
• HOL

Cites Work

• The computational complexity of propositional STRIPS planning
• Verifying a Hotel Key Card System
• A Brief Overview of HOL4
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems