Reductions of petri nets and unfolding of propositional logic programs

Abstract

We present in this paper a new method for computing the reachability set associated with a Petri net. The method proceeds, first, by coding the reachability problem into a predicate defined by a logic program with arithmetic constraints, then by transforming the encoding program. Each transition of the Petri net is encoded as a clause. The guards appearing in the clauses correspond to the enabling conditions of the corresponding transitions. In order to characterize arithmetically the least model of the transformed program, we define a system of two reduction rules which apply iteratively to the program. When the process of reduction terminates with success, it generates a formula of Presburger arithmetic, which contains the components of the initial marking as parameters. In the particular case of a BPP-net (i.e., a Petri net where every transition has exactly one input place), the process is guaranteed to succeed, thus providing us with an exact and generic characterization of the reachability set. We show finally how unfolding of propositional logic programs can be viewed as transformation of BPP-nets.