Solving Coverability Problems of Petri Nets by Partial Deduction

Michael Leuschel and Helko Lehmann

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000

Abstract

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.