Formalization of Karp-Miller tree construction on petri nets

Abstract

Karp-Miller tree construction on Petri nets is a classical well-known algorithm to construct the minimal coverability set via forward analysis. It enables us to construct decision procedures for several problems such as coverability and (place) boundedness. This paper formalizes Karp-Miller tree construction on Petri nets, and its correctness with respect to coverability using Coq and Ssreflect. Instead of showing soundness and completeness for trees directly, we prove these properties for transition systems derived from Petri nets, and then relate them with trees so we can make use of well-established libraries and also avoid making proofs complicated. Termination of the tree construction is guaranteed by defining it as a Coq function with a well-foundedness proof. Although the termination proof for Karp-Miller tree is usually made with classical reasoning, we avoided it so the whole formalization can be done in an axiom-free way with respect the default Coq theory. This work will provide us with a basis for further formalization of several optimized algorithms, some of which are known to be error prone, and also a template for Karp-Miller style algorithms on extended variants of Petri nets.