Skip to Main content Skip to Navigation
Journal articles

The Logical View on Continuous Petri Nets

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [60 references]  Display  Hide  Download
Contributor : Serge Haddad Connect in order to contact the contributor
Submitted on : Thursday, November 30, 2017 - 4:50:04 PM
Last modification on : Friday, April 30, 2021 - 10:05:17 AM


Files produced by the author(s)


  • HAL Id : hal-01652793, version 1


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⟩



Les métriques sont temporairement indisponibles