We investigate fork-free Petri nets (ff-PNs), which are those Petri nets for which each transition has at most one output place, connected by an arc with arbitrary multiplicity. We show that, for each reachable marking, there is a canonical firing sequence with nice properties leading to the marking. The existence of such sequences enables us to apply a mathematical framework for Petri nets which provides upper bounds for many classical problems. Using this framework and known lower bounds we show that the (zero-)reachability, boundedness, and covering problems of ff-PNs are PSPACE-complete. For the liveness problem of ff-PNs we obtain membership in PSPACE. Last, we show that the containment and equivalence problems of ff-PNs are PSPACE-hard and decidable in exponential space.     «

We investigate fork-free Petri nets (ff-PNs), which are those Petri nets for which each transition has at most one output place, connected by an arc with arbitrary multiplicity. We show that, for each reachable marking, there is a canonical firing sequence with nice properties leading to the marking. The existence of such sequences enables us to apply a mathematical framework for Petri nets which provides upper bounds for many classical problems. Using this framework and known lower bounds we sh...     »