The coverability and boundedness problems for Petri nets are known to be Expspace‐complete. Given a Petri net, we associate a graph with it. With the vertex cover number k of this graph and the maximum arc weight W as parameters, we show that coverability and boundedness are in ParaPspace. This means that these problems can be solved in space
, where ef(k,W) is some super‐polynomial function and poly(n) is some polynomial in the size of the input n. We then extend the ParaPspace result to model checking a logic that can express some generalizations of coverability and boundedness.
