Reseña: Verified over-approximation of the diameter of propositionally factored transition systems
Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre verificación titulado Verified over-approximation of the diameter of propositionally factored transition systems.
Sus autores son
+ Mohammad Abdulaziz (del Software Systems Research Group del NICTA en Camberra, Australia),
+ Charles Gretton (de la Australian National University en Camberra, Australia) y
+ Michael Norrish (del Software Systems Research Group del NICTA en Camberra, Australia)
Su resumen es
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 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 compositional 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.
El trabajo se presentó el 26 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).
El código de las correspondientes teorías en HOL4 se encuentra aquí.