Trustworthy Systems

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

Authors

Mohammad Abdulaziz, Charles Gretton and Michael Norrish

NICTA

Australian National University

Griffith University

Abstract

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 proper- ties. 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 calaculated in a compositional way, by first identifying and bounding atomic subsystems, and then composing those results according to subsystem dependencies to arrive at a bound for the concrete system. Compositional approaches are invalid when using the diameter to bound atomic subsystems, and valid when using the recurrence diameter. We provide a novel overapproximation of the diameter, called the sublist diameter, that is tighter than the recurrence diameter. We prove that composi- tional approaches are valid using it to bound atomic subsystems. Those proofs are mechanised in HOL4. We also describe a novel verified compositional bounding technique which provides tighter overall bounds compared to existing bottom-up approaches.

BibTeX Entry

  @inproceedings{Abdulaziz_GN_15_2,
    address          = {Nanjing, China},
    author           = {Abdulaziz, Mohammad and Gretton, Charles and Norrish, Michael},
    booktitle        = {International Conference on Interactive Theorem Proving},
    keywords         = {bounded model checking, planning, interactive theorem proving},
    month            = aug,
    pages            = {1--16},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8655.pdf},
    title            = {Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems},
    year             = {2015}
  }

Download