Approaching the Coverability Problem Continuously

The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this talk, I will present a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward-coverability framework. A cornerstone of the presented approach is the efficient encoding of a polynomial-time algorithm for reachability in continuous Petri nets into SMT. The effectiveness of the approach will be demonstrated by evaluating it on standard benchmarks from the literature, which shows that the approach decides significantly more instances than any existing tool and is in addition often much faster, in particular on large instances. Finally, I will briefly discuss how the developed logical characterization yields further decidability and complexity results for standard decision problems on continuous Petri nets.

Based on joint work with M. Blondin (TU Munich), A. Finkel and S. Haddad (ENS Cachan).

Speaker biography

Christoph Haase is a departmental lecturer at the Department of Computer Science at the University of Oxford. From 2012 until 2016, he held post-doctoral positions at ENS Cachan in France. He obtained his D.Phil. from the University of Oxford in 2012.