Formally verified algorithms for upper-bounding state space diameters
DOI10.1007/s10817-018-9450-zzbMath1451.68164OpenAlexW2789258134MaRDI QIDQ1663245
Mohammad Abdulaziz, Michael Norrish, Charles Gretton
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-9450-z
diameterformal verificationtransition systemsAI planningbounded model checkingSAT-based planningcompleteness threshold
Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Planning as satisfiability: heuristics
- Antichains and compositional algorithms for LTL synthesis
- The diameter of almost Eulerian digraphs
- Diameter and maximum degree in Eulerian digraphs
- Radius, diameter, and minimum degree
- Automatically generating abstractions for planning
- On the exponent of all pairs shortest path problem
- A note on the complexity of longest path problems related to graph coloring
- The diameter of directed graphs
- The small model property: How small can it be?
- On the diameter of a graph
- STRIPS: A new approach to the application of theorem proving to problem solving
- A Constructive Theory of Regular Languages in Coq
- Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems
- On the Magnitude of Completeness Thresholds in Bounded Model Checking
- More Algorithms for All-Pairs Shortest Paths in Weighted Graphs
- A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
- Linear Completeness Thresholds for Bounded Model Checking
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- A Formalisation of Finite Automata Using Hereditarily Finite Sets
- Verifying a Hotel Key Card System
- A Brief Overview of HOL4
- Maximum diameter of regular digraphs
- New Bounds on the Complexity of the Shortest Path Problem
- Fast Estimation of Diameter and Shortest Paths (Without Matrix Multiplication)
- Color-coding
- Finding a Path of Superlogarithmic Length
- Approximation and Fixed Parameter Subquadratic Algorithms for Radius and Diameter in Sparse Graphs
- Better Approximation Algorithms for the Graph Diameter
- Automata, Languages and Programming
- Fast approximation algorithms for the diameter and radius of sparse graphs
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
This page was built for publication: Formally verified algorithms for upper-bounding state space diameters
