Coverability of reset petri nets and other wellstructured transition systems by partial deduction

Abstract. In recent work it has been shown that innite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. It has also been shown that par-tial deduction is powerful enough to mimic certain algorithms to decide coverability properties of Petri nets. These algorithms are forward al-gorithms and hard to scale up to deal with more complicated systems. Recently, it has been proposed to use a backward algorithm scheme in-stead. 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. In this paper, we discuss how partial deduction can mimic many of these backward algorithms as well. We prove this link in particular for reset Petri nets and Petri nets with transfer and doubling arcs. We thus establish a surprising link between algorithms in Petri net theory and program specialisation, and also shed light on the power of using logic program specialisation for innite state model checking.