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]
Collections | ANU 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 | Size | Format | Image |
---|---|---|---|---|
01_Mansour+%28Abdulaziz%29_Verified_over-approximation_of_2015.pdf | 501.63 kB | Adobe PDF | Request a copy |
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 20 July 2017/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator