2016/07/18 by Thomas Geffroy, Geffroy, Thomas, Jérôme Leroux +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Petri Nets in System Modeling
paper · doi:10.48550/arxiv.1607.05956
openalex publication_date 2016/07/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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. 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.