From Continuous Petri nets to Petri nets and Back

Serge Haddad
LSV, Cachan
Friday, 24 February, 2017 - 14:00
Salle Solvay (NO, 5th floor)
At the end of the eighties, continuous Petri nets (CPN) were introduced for: (1) alleviating the combinatory explosion triggered by discrete Petri nets (i.e. usual Petri nets) and, (2) modelling the behaviour of physical systems whose state is composed of continuous variables. Since then several works have established that the computational complexity of deciding some standard behavioural properties of Petri nets is reduced in this framework. This talk will be divided in three parts.

First I will describe in detail a polynomial time decision procedure for reachability  and give
an overview of the decision procedures for properties like coverability and boundedness. 
I will also show that reachability is PTIME-complete while deadlock freeness is coNP-complete.

Then I will study the application of the previous decision procedures to the coverability problem for Petri nets. Coverability 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. Here I will develop 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 our approach is the efficient encoding of the polynomial-time algorithm for       reachability in CPN into SMT. I also demonstrate the effectiveness of our approach on standard benchmarks from the literature.

Finally I will show that the logical encoding can also be applied to the
reachability set inclusion problem in CPN improving the complexity from EXPTIME to coNP. 
I also establish that this procedure is optimal, i.e. this problem is coNP-complete. 

Based on:
(1) L. Recalde, S. Haddad and M. Silva.  Continuous Petri Nets: Expressive Power and Decidability Issues.  International Journal of Foundations of Computer Science 21(2), pages 235-256, 2010
(2)  E. Fraca and S. Haddad.  Complexity Analysis of Continuous Petri Nets.  Fundamenta Informaticae 137(1), pages 1-28, 2015

(3)  M. Blondin, A. Finkel, C. Haase and S. Haddad.  Approaching the Coverability Problem Continuously, TACAS'16, LNCS 9636, pages 480-496, 2016