In: Proc. 2nd Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming (PPDP'2000), 20-23 September 2000, Montreal, Canada, pages 268-279. 2000.
Abstract: It has been shown recently that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on a particular class of problems -- coverability for (infinite state) Petri nets - and shows how existing techniques and tools for declarative programs can be successfully applied. In particular, the paper shows that a restricted form of partial deduction is already powerful enough to decide all coverability properties of Petri nets. It also proves that particular instances of partial deduction exactly compute the Karp-Miller tree as well as Finkel's minimal coverability set. A link is thus established between algorithms for Petri nets and logic program specialization.
Keywords: Petri nets, abstract interpretation, logic programming, model checking, partial evaluation, program analysis, program verification.