Occam's Razor applied to the Petri net coverability problem

Citations of this article
Mendeley users who have this article in their library.
Get full text


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 ago. Driven by the concurrency revolution, it has regained a lot of interest over the last decade. In this paper, we propose a generic and simple approach to solve this problem. Our method is inspired from the recent approach of Blondin, Finkel, Haase and Haddad presented at TACAS in 2016. Basically, we combine forward invariant generation techniques for Petri nets with backward reachability for well-structured transition systems. An experimental evaluation demonstrates the efficiency of our approach.




Geffroy, T., Leroux, J., & Sutre, G. (2018). Occam’s Razor applied to the Petri net coverability problem. Theoretical Computer Science, 750, 38–52. https://doi.org/10.1016/j.tcs.2018.04.014

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free