Formally verified algorithms for upper-bounding state space diameters
DOI10.1007/S10817-018-9450-ZzbMATH Open1451.68164OpenAlexW2789258134MaRDI QIDQ1663245FDOQ1663245
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
Recommendations
- Verified over-approximation of the diameter of propositionally factored transition systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal Verification of Infinite State Systems Using Boolean Methods
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Science Logic
- Verification of infinite-state dynamic systems using approximate quotient transition systems
- scientific article; zbMATH DE number 1678389
diametertransition systemsAI planningformal verificationbounded model checkingSAT-based planningcompleteness threshold
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- A Brief Overview of HOL4
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- A Formalisation of Finite Automata Using Hereditarily Finite Sets
- Verifying a Hotel Key Card System
- STRIPS: A new approach to the application of theorem proving to problem solving
- Title not available (Why is that?)
- Color-coding
- Finding a Path of Superlogarithmic Length
- Automata, Languages and Programming
- Fast approximation algorithms for the diameter and radius of sparse graphs
- Radius, diameter, and minimum degree
- The fast downward planning system
- Fast Estimation of Diameter and Shortest Paths (Without Matrix Multiplication)
- New Bounds on the Complexity of the Shortest Path Problem
- Planning as satisfiability: heuristics
- On the exponent of all pairs shortest path problem
- On the Magnitude of Completeness Thresholds in Bounded Model Checking
- Maximum diameter of regular digraphs
- Automatically generating abstractions for planning
- More Algorithms for All-Pairs Shortest Paths in Weighted Graphs
- Title not available (Why is that?)
- The small model property: How small can it be?
- Antichains and compositional algorithms for LTL synthesis
- The diameter of directed graphs
- Title not available (Why is that?)
- The diameter of almost Eulerian digraphs
- On the diameter of a graph
- Linear Completeness Thresholds for Bounded Model Checking
- Approximation and Fixed Parameter Subquadratic Algorithms for Radius and Diameter in Sparse Graphs
- A Constructive Theory of Regular Languages in Coq
- Diameter and maximum degree in Eulerian digraphs
- Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems
- Better Approximation Algorithms for the Graph Diameter
- A note on the complexity of longest path problems related to graph coloring
- Computing over-approximations with bounded model checking
- A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Title not available (Why is that?)
Cited In (2)
Uses Software
This page was built for publication: Formally verified algorithms for upper-bounding state space diameters
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663245)
