Solving coverability problems of petri nets by partial deduction
Michaël Leuschel, Helko Lehmann · 2000
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one particular class of problem--coverability for (infinite state) Petri nets--and shows how existing techniques and tools for declarative programs can be successfully applied. In particular, we show that a restricted form of partial deduction is already powerful enough to decide all coverability properties of Petri Nets. We also prove that two particular instances of partial deduction exactly compute the Karp-Miller tree as well as Finkel's minimal coverability set. We thus establish an interesting link between algorithms for Petri nets and logic program specialisation.