Small Vertex Cover makes Petri Net Coverability and Boundedness Easier

TL;DR

This paper demonstrates that the coverability and boundedness problems for Petri nets become more tractable when the associated graph has a small vertex cover number, leading to fixed-parameter tractable algorithms.

Contribution

It introduces a parameterized complexity approach for Petri net problems, showing they are in ParaPspace when parameterized by vertex cover number and maximum arc weight.

Findings

Coverability and boundedness are in ParaPspace with small vertex cover.

Extends results to model checking of generalized properties.

Provides a new fixed-parameter tractability framework for Petri net analysis.

Abstract

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.