Continuous Petri Nets: Expressive Power and Decidability Issues

Laura Recalde Serge Haddad 1 Manuel Silva
1 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : State explosion is a fundamental problem in the analysis and synthesis of discrete event systems. Continuous Petri nets can be seen as a relaxation of the corresponding discrete model. The expected gains are twofold: improvements in complexity and in decidability. In the case of autonomous nets we prove that liveness or deadlock-freeness remain decidable and can be checked more efficiently than in Petri nets. Then we introduce time in the model which now behaves as a dynamical system driven by differential equations and we study it w.r.t. expressiveness and decidability issues. On the one hand, we prove that this model is equivalent to timed differential Petri nets which are a slight extension of systems driven by linear differential equations (LDE). On the other hand, (contrary to the systems driven by LDEs) we show that continuous timed Petri nets are able to simulate Turing machines and thus that basic properties become undecidable.
Type de document :
Article dans une revue
International Journal of Foundations of Computer Science, World Scientific Publishing, 2010, 21 (2), pp.235-256. 〈10.1142/S0129054110007222〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00779919
Contributeur : Stefan Haar <>
Soumis le : mardi 22 janvier 2013 - 17:08:32
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Lien texte intégral

Identifiants

Collections

Citation

Laura Recalde, Serge Haddad, Manuel Silva. Continuous Petri Nets: Expressive Power and Decidability Issues. International Journal of Foundations of Computer Science, World Scientific Publishing, 2010, 21 (2), pp.235-256. 〈10.1142/S0129054110007222〉. 〈hal-00779919〉

Partager

Métriques

Consultations de la notice

287