Skip navigation
Skip navigation

Verified over-approximation of the diameter of propositionally factored transition systems

Mansour (Abdulaziz), Mohammad; Gretton, Charles; Norrish, Michael


To guarantee the completeness of bounded model checking (BMC) we require a completeness threshold. The diameter of the Kripke model of the transition system is a valid completeness threshold for BMC of safety properties. The recurrence diameter gives us an upper bound on the diameter for use in practice. Transition systems are usually described using (propositionally) factored representations. Bounds for such lifted representations are calculated in a compositional way, by first identifying and...[Show more]

CollectionsANU Research Publications
Date published: 2015
Type: Conference paper
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI: 10.1007/978-3-319-22102-1_1


File Description SizeFormat Image
01_Mansour+%28Abdulaziz%29_Verified_over-approximation_of_2015.pdf501.63 kBAdobe PDF    Request a copy

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

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator