Skip navigation
Skip navigation

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

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

Description

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
URI: http://hdl.handle.net/1885/103343
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

Download

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:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator