Blondin, M;
Finkel, A;
Haase, C;
Haddad, S;
(2017)
The Logical View on Continuous Petri Nets.
ACM Transactions on Computational Logic
, 18
(3)
, Article 24. 10.1145/3105908.
Preview |
Text
Haase_bfhh-17.pdf - Accepted Version Download (608kB) | Preview |
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 article 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 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 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: | Article |
|---|---|
| Title: | The Logical View on Continuous Petri Nets |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3105908 |
| Publisher version: | https://doi.org/10.1145/3105908 |
| Language: | English |
| Additional information: | This version is the version of record. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Petri nets, vector addition systems, coverability, arithmetic theories, linear programming |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10088921 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
