Affiliations: Instituto de Investigación en Ingeniería de Aragón (I3A), Universidad de Zaragoza, Zaragoza, Spain. [email protected] | Ecole Normale Supérieure de Cachan, LSV, CNRS UMR 8643, INRIA, Cachan, France. [email protected]
Note: [] This work has been partially supported by CICYT - FEDER project DPI2010-20413 and B174/11 of Gobierno de Aragón.
Note: [] Address for correspondence: Ecole Normale Supérieure de Cachan, LSV, CNRS UMR 8643, INRIA, Cachan, France This work has been partially supported by ImpRo (ANR-2010-BLAN-0317).
Abstract: At the end of the eighties, continuous Petri nets 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. Here we first establish the decidability of additional properties like coverability, boundedness and reachability set inclusion. We also design new decision procedures for reachability and lim-reachability problems with a better computational complexity. Finally we provide lower bounds characterising the exact complexity class of the reachability, the coverability, the boundedness, the deadlock freeness and the liveness problems. A small case study is introduced and analysed with these new procedures.
Keywords: Continuous Petri nets, structural analysis, complexity
