In: Lecture Notes in Artificial Intelligence, Vol. 1861: Computational Logic, Proceedings of CL 2000, pages 101-115. Springer-Verlag, 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. It has also been shown that partial deduction is powerful enough to mimic certain algorithms to decide coverability properties of Petri nets. These algorithms are forward algorithms and hard to scale up to deal with more complicated systems. Recently, it has been proposed to use a backward algorithm scheme instead. This scheme is applicable to so-called well-structured transition systems and was successfully used, e.g., to solve coverability problems for reset Petri nets. This paper discusses how partial deduction can mimic many of these backward algorithms as well. This link is proven in particular for reset Petri nets and Petri nets with transfer and doubling arcs. Thus a surprising link between algorithms in Petri net theory and program specialization has been established, and also light has been shed on the power of using logic program specialization for infinite state model checking.
Keywords: coverability, partial deduction, reset Petri nets, well-structured transition systems.