Small Vertex Cover Makes Petri Net Coverability and Boundedness Easier

摘要

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 O (ef(k, W)poly(n)), where ef(k, W) is some exponential function and poly(n) is some polynomial in the size of the input. We then extend the ParaPspace result to model checking a logic that can express some generalizations of coverability and boundedness.