Coverability of reset petri nets and other well-structured transition systems by partial deduction

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. 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 infinite state model checking.