Verified over-approximation of the diameter of propositionally factored transition systems
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|
|Source:||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|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.