Email Gateway (Aug 22 2022 at 18:37): Email Gateway (Aug 22 2022 at 18:37):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
the new AFP-entry
Upper Bounding Diameters of State Spaces of Factored Transition Systems
by Friedrich Kurz and Mohammad Abdulaziz
is now available.
https://www.isa-afp.org/entries/Factored_Transition_System_Bounding.html
Cheers,
René
Abstract:
A completeness threshold is required to guarantee the completeness of planning
as satisfiability, and bounded model checking of safety properties. One valid
completeness threshold is the diameter of the underlying transition system. The
diameter is the maximum element in the set of lengths of all shortest paths
between pairs of states. The diameter is not calculated exactly in our setting,
where the transition system is succinctly described using a (propositionally)
factored representation. Rather, an upper bound on the diameter is calculated
compositionally, by bounding the diameters of small abstract subsystems, and
then composing those. We port a HOL4 formalisation of a compositional algorithm
for computing a relatively tight upper bound on the system diameter. This
compositional algorithm exploits acyclicity in the state space to achieve
compositionality, and it was introduced by Abdulaziz et. al. The formalisation
that we port is described as a part of another paper by Abdulaziz et. al. As a
part of this porting we developed a libray about transition systems, which shall
be of use in future related mechanisation efforts.
signature.asc
Last updated: Apr 26 2024 at 01:06 UTC