Parameterized complexity results for 1-safe Petri nets

TL;DR

This paper investigates the parameterized complexity of problems related to 1-safe Petri nets by associating them with graphs and analyzing parameters like treewidth, benefit depth, and vertex cover number, providing new hardness results and an FPT algorithm.

Contribution

It establishes W[1]-hardness results for several problems based on graph parameters and introduces an FPT algorithm for MSO model checking on 1-safe Petri nets using vertex cover and formula size.

Findings

W[1]-hardness results for problems parameterized by treewidth and benefit depth.

A fixed-parameter tractable algorithm for MSO model checking using vertex cover.

Proves a conjecture on the hardness of graph pebbling problems.

Abstract

We associate a graph with a 1-safe Petri net and study the parameterized complexity of various problems with parameters derived from the graph. With treewidth as the parameter, we give W[1]-hardness results for many problems about 1-safe Petri nets. As a corollary, this proves a conjecture of Downey et. al. about the hardness of some graph pebbling problems. We consider the parameter benefit depth (that is known to be helpful in getting better algorithms for general Petri nets) and again give W[1]-hardness results for various problems on 1-safe Petri nets. We also consider the stronger parameter vertex cover number. Combining the well known automata-theoretic method and a powerful fixed parameter tractability (FPT) result about Integer Linear Programming, we give a FPT algorithm for model checking Monadic Second Order (MSO) formulas on 1-safe Petri nets, with parameters vertex cover number and the size of the formula.