Patrick Totzke

What Makes Petri Nets Harder to Verify: Stack or Data?

We show how the yardstick construction of Stockmeyer, also developed as counter bootstrapping by Lipton, can be adapted and extended to obtain new lower bounds for the coverability problem for two prominent classes of systems based on Petri nets: ACKERMANN-hardness for unordered data Petri nets, and TOWER-hardness for pushdown vector addition systems.

This is an invited paper at International Symposium in Honour of Bill Roscoe's 60th Birthday (Bill-60).