The Logical View on Continuous Petri Nets

Serge Haddad 1, 2 Michael Blondin 2 Christoph Haase 2, 3 Alain Finkel 2
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 : Continuous Petri nets are a relaxation of classical discrete Petri nets in which transitions can be fired a fractional number of times, and consequently places may contain a fractional number of tokens. Such continuous Petri nets are an appealing object to study since they over approximate the set of reachable configurations of their discrete counterparts, and their reachability problem is known to be decidable in polynomial time. The starting point of this paper is to show that the reachability relation for continuous Petri nets is definable by a sentence of linear size in the existential theory of the rationals with addition and order. Using this characterization, we obtain decidability and complexity results for a number of classical decision problems for continuous Petri nets. In particular, we settle the open problem about the precise complexity of reachability set inclusion. Finally, we show how continuous Petri nets can be incorporated inside the classical backward coverability algorithm for discrete Petri nets as a pruning heuristic in order to tackle the symbolic state explosion problem. The cornerstone of the approach we present is that our logical characterization enables us to leverage the power of modern SMT-solvers in order to yield a highly performant and robust decision procedure for coverability in Petri nets. We demonstrate the applicability of our approach on a set of standard benchmarks from the literature.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2017, 18 (3)
Liste complète des métadonnées

Littérature citée [60 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01652793
Contributeur : Serge Haddad <>
Soumis le : jeudi 30 novembre 2017 - 16:50:04
Dernière modification le : dimanche 18 mars 2018 - 13:42:01

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01652793, version 1

Citation

Serge Haddad, Michael Blondin, Christoph Haase, Alain Finkel. The Logical View on Continuous Petri Nets. ACM Transactions on Computational Logic, Association for Computing Machinery, 2017, 18 (3). 〈hal-01652793〉

Partager

Métriques

Consultations de la notice

222

Téléchargements de fichiers

58