Skip navigation
Skip navigation

Formally Verified Algorithms for Upper-Bounding State Space Diameters

Abdulaziz, Mohammad; Norrish, Michael; Gretton, Charles


A completeness threshold is required to guarantee the completeness of planning as satisfiability, and bounded model checking of safety properties. We investigate completeness thresholds related to the diameter of the underlying transition system. A valid threshold,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...[Show more]

CollectionsANU Research Publications
Date published: 2018
Type: Journal article
Source: Journal of Automated Reasoning
DOI: 10.1007/s10817-018-9450-z


File Description SizeFormat Image
01_Mansour+%28Abdulaziz%29_Formally_Veri%EF%AC%81ed_Algorithms_2018.pdf1.1 MBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator