The reachability problem for standard Petri nets is EXPSPACE hard, and the coverability problem is EXPSPACE complete. However, more efficient algorithms exist for variants of the standard nets. Continuous Petri nets are such a variant that allows the number of tokens to be a rational number. As in other problems, replacing integers by rationals leads to easier problems. For this class, the reachability problem can be defined in the first-order theory of the rationals with addition and order. This leads to a polynomial-time algorithm for checking reachability. The computation for continuous Petri nets can be used as an over-approximation for standard Petri nets.

In this paper, the authors exploit the encoding in the theory of the rationals further to establish the complexity class for additional problems, like inclusion, epsilon liveness, and the home state problem, about continuous Petri nets. As an application of this encoding, the authors show that it can be used as a pruning criterion for the backward algorithm to decide coverability for standard Petri nets.

The authors recall all relevant definitions and known results, so the general reader might get a good overview. However, to fully grasp the details, the reader has to be familiar with recent results for Petri nets, including the previous work of the authors. For the benefit of this group, detailed proofs are included.