The Logical View on Continuous Petri Nets - Archive ouverte HAL Access content directly
Journal Articles ACM Transactions on Computational Logic Year : 2017

The Logical View on Continuous Petri Nets

(1, 2) , (2) , (2, 3) , (2)
1
2
3

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.
Fichier principal
Vignette du fichier
main.pdf (594.89 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01652793 , version 1 (30-11-2017)

Identifiers

  • HAL Id : hal-01652793 , version 1

Cite

Serge Haddad, Michael Blondin, Christoph Haase, Alain Finkel. The Logical View on Continuous Petri Nets. ACM Transactions on Computational Logic, 2017, 18 (3). ⟨hal-01652793⟩
281 View
221 Download

Share

Gmail Facebook Twitter LinkedIn More