Occam's Razor Applied to the Petri Net Coverability Problem

Thomas Geffroy, Jérôme Leroux, Grégoire Sutre

The verification of safety properties for concurrent systems often reduces to the coverability problem for Petri nets. This problem was shown to be ExpSpace-complete forty years ag…