Formally verified algorithms for upper-bounding state space diameters
From MaRDI portal
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
Cites work
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- scientific article; zbMATH DE number 4144019 (Why is no real title available?)
- scientific article; zbMATH DE number 1953038 (Why is no real title available?)
- scientific article; zbMATH DE number 1903351 (Why is no real title available?)
- A Brief Overview of HOL4
- A constructive theory of regular languages in Coq
- A formalisation of finite automata using hereditarily finite sets
- A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
- A note on the complexity of longest path problems related to graph coloring
- Antichains and compositional algorithms for LTL synthesis
- Approximation and Fixed Parameter Subquadratic Algorithms for Radius and Diameter in Sparse Graphs
- Automata, Languages and Programming
- Automatically generating abstractions for planning
- Better approximation algorithms for the graph diameter
- Color-coding
- Computing over-approximations with bounded model checking
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Diameter and maximum degree in Eulerian digraphs
- Fast Estimation of Diameter and Shortest Paths (Without Matrix Multiplication)
- Fast approximation algorithms for the diameter and radius of sparse graphs
- Finding a Path of Superlogarithmic Length
- Linear completeness thresholds for bounded model checking
- Maximum diameter of regular digraphs
- More Algorithms for All-Pairs Shortest Paths in Weighted Graphs
- New Bounds on the Complexity of the Shortest Path Problem
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- On the diameter of a graph
- On the exponent of all pairs shortest path problem
- On the magnitude of completeness thresholds in bounded model checking
- Planning as satisfiability: heuristics
- Radius, diameter, and minimum degree
- STRIPS: A new approach to the application of theorem proving to problem solving
- The diameter of almost Eulerian digraphs
- The diameter of directed graphs
- The fast downward planning system
- The small model property: How small can it be?
- Verified over-approximation of the diameter of propositionally factored transition systems
- Verifying a Hotel Key Card System
Cited in
(3)
Describes a project that uses
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)
