Completeness Results for Generalized Communication-free Petri Nets with Arbitrary Arc Multiplicities

Abstract

We investigate gcf-Petri nets, a generalization of communication-free Petri nets allowing arbitrary arc multiplicities, and characterized by the sole restriction that each transition has at most one incoming arc. We use canonical firing sequences with nice properties for gcf-PNs to show that the RecLFS, (zero-)reachability, covering, and boundedness problems of gcf-PNs are in PSPACE. By simulating PSPACE-Turing machines by gss-PNs, a subclass of gcf-PNs where additionally all transitions have at most one outgoing arc, we ultimately obtain PSPACE-completess for these problems in case of gss-PNs or gcf-PNs. Additionally, we prove PSPACE-completeness for the liveness problem of gcf-PNs. Last, we show PSPACE-hardness as well as a doubly exponential space upper bound for the containment and equivalence problems of gss-PNs or gcf-PNs.