research-article

The Logical View on Continuous Petri Nets

Authors:

Michael Blondin,

Christoph Haase,

Serge HaddadAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 18, Issue 3

Article No.: 24, Pages 1 - 28

https://doi.org/10.1145/3105908

Published: 04 August 2017 Publication History

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.

References

[1]

Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. 1996. General decidability theorems for infinite-state systems. In Proceedings of the Conference on Logic in Computer Science (LICS’96). IEEE Computer Society, 313--321.

[2]

André Arnold and Michel Latteux. 1978. Récursivit et cônes rationnels fermés par intersection. Calcolo 15, 4 (1978), 381--394.

[3]

Thomas Ball, Sagar Chaki, and Sriram K. Rajamani. 2001. Parameterized verification of multithreaded software libraries. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS (Lect. Notes Comp. Sci.), Vol. 2031. Springer, 158--173.

[4]

Leonard Berman. 1980. The complexitiy of logical theories. Theor. Comput. Sci. 11 (1980), 71--77.

Digital Library

[5]

Eike Best and Javier Esparza. 2016. Existence of home states in petri nets is decidable. Inf. Process. Lett. 116, 6 (2016), 423--427.

Digital Library

[6]

Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. 2016. Approaching the coverability problem continuously. In Tools and Algorithms for Construction and Analysis of Systems, TACAS (Lect. Notes Comp. Sci.), Vol. 9636. Springer, 480--496.

Digital Library

[7]

Itshak Borosh and Leon B. Treybing. 1976. Bounds on positive integral solutions of linear diophantine equations. P. Am. Math. Soc. 55, 2 (1976), 299--304.

[8]

Laura Bozzelli and Pierre Ganty. 2011. Complexity analysis of the backward coverability algorithm for VASS. In Reachability Problems, RP (Lect. Notes Comp. Sci.), Vol. 6945. Springer, 96--109.

[9]

E. Cardoza, Richard J. Lipton, and Albert R. Meyer. 1976. Exponential space complete problems for petri nets and commutative semigroups: Preliminary report. In Proceedings of the Symposium on Theory of Computing (STOC’76). 50--54.

Digital Library

[10]

Dmitry Chistikov, Christoph Haase, and Simon Halfon. 2017. Context-free commutative grammars with integer counters and resets. Theoret. Comput. Sci. (2017). In press.

[11]

René David and Hassane Alla. 1987. Continuous petri nets. In Proceedings of the 8th European Workshop on Application and Theory of Petri Nets. 275--294.

[12]

René David and Hassane Alla. 2010. Discrete, Continuous, and Hybrid Petri nets (2nd ed.). Springer.

[13]

Davide de Frutos Escrig and Colette Johnen. 1989. Decidability of Home Space Property. Technical Report LRI-503. Univ. de Paris-Sud, Centre d’Orsay, Laboratoire de Recherche en Informatique.

[14]

Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS (Lect. Notes Comp. Sci.), Vol. 4963. Springer, 337--340.

[15]

Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin. 2001. Attacking symbolic state explosion. In Computer Aided Verification, CAV (Lect. Notes Comp. Sci.), Vol. 2102. Springer, 298--310.

[16]

Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin. 2004. Covering sharing trees: A compact data structure for parameterized verification. Int. J. Softw. Tools Technol. Transf. 5, 2--3 (2004), 268--297.

Digital Library

[17]

Jörg Desel and Javier Esparza. 1995. Free Choice Petri nets. Cambridge Tracts in Theoret. Comp. Sci., Vol. 40. Cambridge University Press, New York, NY.

[18]

Emanuele D’Osualdo, Jonathan Kochems, and C.-H. Luke Ong. 2013. Automatic verification of erlang-style concurrency. In Static Analysis, SAS (Lect. Notes Comp. Sci.), Vol. 7935. Springer, 454--476.

[19]

Emanuele D’Osualdo, Jonathan Kochems, and Luke Ong. 2012. Soter: An automatic safety verifier for erlang. In Proceedings of the Conference on Programming Based on Actors, Agents, and Decentralized Control (AGERE’12). ACM, 137--140.

Digital Library

[20]

Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp Meyer, and Filip Nikšić. 2014. An SMT-Based approach to coverability analysis. In Computer Aided Verification, CAV (Lect. Notes Comp. Sci.), Vol. 8559. Springer, 603--619.

Digital Library

[21]

Javier Esparza and Stephan Melzer. 2000. Verification of safety properties using integer programming: Beyond the state equation. Formal Meth. Syst. Design 16, 2 (2000), 159--189.

Digital Library

[22]

Alain Finkel and Jérôme Leroux. 2015. Recent and simple algorithms for petri nets. Softw. Syst. Model. 14, 2 (2015), 719--725.

Digital Library

[23]

Alain Finkel, Jean-François Raskin, Mathias Samuelides, and Laurent Van Begin. 2002. Monotonic extensions of petri nets: Forward and backward search revisited. Electr. Notes Theor. Comput. Sci. 68, 6 (2002), 85--106.

[24]

Alain Finkel and Philippe Schnoebelen. 2001. Well-structured transition systems everywhere&excl; Theor. Comput. Sci. 256, 1--2 (2001), 63--92.

Digital Library

[25]

Estíbaliz Fraca and Serge Haddad. 2015. Complexity analysis of continuous petri nets. Fundam. Inform. 137, 1 (2015), 1--28.

Digital Library

[26]

Pierre Ganty. 2002. Algorithmes et Structures De Données Efficaces Pour La Manipulation De Contraintes Sur Les Intervalles (in French). Master’s thesis. Université Libre de Bruxelles, Belgium.

[27]

Pierre Ganty, Cédric Meuter, Giorgio Delzanno, Gabriel Kalyon, Jean-François Raskin, and Laurent Van Begin. 2007. Symbolic Data Structure for Sets of -uples. Technical Report 570. Université Libre de Bruxelles, Belgium.

[28]

Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. 2006. Expand, enlarge and check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72, 1 (2006), 180--203.

Digital Library

[29]

Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. 2010. On the efficient computation of the minimal coverability set of petri nets. Int. J. Found. Comput. Sci. 21, 2 (2010), 135--165.

[30]

Thomas Geffroy, Jérôme Leroux, and Grégoire Sutre. 2016. Occam’s razor applied to the petri net coverability problem. In Reachability Problems, RP (Lect. Notes Comp. Sci.), Vol. 9899. Springer, 77--89.

[31]

Steven M. German and A. Prasad Sistla. 1992. Reasoning about systems with many Processes. J. ACM 39, 3 (1992), 675--735.

Digital Library

[32]

Michel Henri Théodore Hack. 1974. The recursive equivalence of the reachability problem and the liveness problem for petri nets and vector addition systems. In Proceedings of the Conference on Switching and Automata Theory (SWAT’74) (FOCS). IEEE Computer Society, 156--164.

Digital Library

[33]

Michel Henri Théodore Hack. 1976. Decidability questions for Petri Nets. Ph.D. Dissertation. Massachusetts Institute of Technology, USA.

[34]

Monika Heiner, David R. Gilbert, and Robin Donaldson. 2008. Petri nets for systems and synthetic biology. In Formal Methods for Computational Systems Biology, 8th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM (Lect. Notes Comp. Sci.), Vol. 5016. Springer, 215--264.

[35]

Petr Jančar. 2017. Deciding structural liveness of petri nets. In Current Trends in Theory and Practice of Computer Science, SOFSEM (Lect. Notes Comp. Sci.), Vol. 10139. Springer, 91--102.

[36]

Ji Jank. 2009. Issue Tracking Systems. Master’s thesis. Masarykova univerzita, Czech Republic.

[37]

Alexander Kaiser, Daniel Kroening, and Thomas Wahl. 2012. Efficient coverability analysis by proof minimization. In Proceedings of the Conference on Concurrency Theory (CONCUR’12). Springer, 500--515.

Digital Library

[38]

Alexander Kaiser, Daniel Kroening, and Thomas Wahl. 2014. A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36, 4 (2014), 14:1--14:29. http://doi.acm.org/10.1145/2629608

Digital Library

[39]

Richard M. Karp and Raymond E. Miller. 1967. Parallel program schemata: A mathematical model for parallel computation. In Proceedings of the Conference on Switching and Automata Theory (SWAT’67) (FOCS). IEEE Computer Society, 55--61.

Digital Library

[40]

Johannes Kloos, Rupak Majumdar, Filip Niksic, and Ruzica Piskac. 2013. Incremental, inductive coverability. In Computer Aided Verification, CAV (Lect. Notes Comp. Sci.), Vol. 8044. Springer, 158--173.

Digital Library

[41]

S. Rao Kosaraju. 1982. Decidability of reachability in vector addition systems (preliminary version). In Proceedings of the Symposium on Theory of Computing (STOC’82). ACM, 267--281.

Digital Library

[42]

Jean-Luc Lambert. 1992. A structure to decide reachability in petri nets. Theoret. Comput. Sci. 99, 1 (1992), 79--104.

Digital Library

[43]

Jérôme Leroux. 2009. The general vector addition system reachability problem by presburger inductive invariants. In Proceedings of the Conference on Logic in Computer Science (LICS’09). IEEE Computer Society, 4--13.

Digital Library

[44]

Jérôme Leroux. 2011. Vector addition system reachability problem: A short self-contained proof. In Language and Automata Theory and Applications, LATA (Lect. Notes Comp. Sci.), Vol. 6638. Springer, 41--64.

[45]

Jérôme Leroux. 2012. Vector addition systems reachability problem (a simpler solution). In The Alan Turing Centenary Conference. EasyChair, 214--228. http://www.easychair.org/publications/?page=1673703727

[46]

Jérôme Leroux and Sylvain Schmitz. 2015. Demystifying reachability in vector addition systems. In Proceedings of the Conference on Logic in Computer Science (LICS’15). IEEE, 56--67.

Digital Library

[47]

Richard J. Lipton. 1976. The Reachability Problem Requires Exponential Space. Technical Report 63. Department of Computer Science, Yale University.

[48]

Rupak Majumdar, Roland Meyer, and Zilong Wang. 2013. Static provenance verification for message passing programs. In Static Analysis, SAS (Lect. Notes Comp. Sci.), Vol. 7935. Springer, 366--387.

[49]

Ernst W. Mayr. 1981. An algorithm for the general petri net reachability problem. In Proceedings of the Symposium on Theory of Computing (STOC’81). ACM, 238--246.

Digital Library

[50]

Charles Rackoff. 1978. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6 (1978), 223--231.

[51]

Laura Recalde, Enrique Teruel, and Manuel Silva Suárez. 1999. Autonomous continuous P/T systems. In Application and Theory of Petri Nets, ICATPN (Lect. Notes Comp. Sci.), Vol. 1639. Springer, 107--126.

[52]

Venkatramana N. Reddy, Michael N. Liebman, and Michael L. Mavrovouniotis. 1996. Qualitative analysis of biochemical reaction systems. Comput. Biol. Med. 26, 1 (1996), 9--24.

[53]

Pierre-Alain Reynier and Frédéric Servais. 2013. Minimal coverability set for petri nets: Karp and miller algorithm with pruning. Fundam. Inform. 122, 1--2 (2013), 1--30.

Digital Library

[54]

Philippe Schnoebelen. 2010. Revisiting ackermann-hardness for lossy counter machines and reset petri nets. In Mathematical Foundations of Computer Science, MFCS (Lect. Notes Comp. Sci.), Vol. 6281. Springer, 616--628.

[55]

Alexander Schrijver. 1998. Theory of Linear and Integer Programming. Wiley.

[56]

Eduardo D. Sontag. 1985. Real addition and the polynomial hierarchy. Inf. Process. Lett. 20, 3 (1985), 115--120.

[57]

Filip Thoen and Francky Catthoor. 2000. Modeling, Verification and Exploration of Task-level Concurrency in Real-time Embedded Systems. Springer US, Boston, MA.

[58]

Antti Valmari and Henri Hansen. 2014. Old and new algorithms for minimal coverability sets. Fundam. Inform. 131, 1 (2014), 1--25.

Digital Library

[59]

Wil M. P. van der Aalst. 1998. The application of petri nets to workflow management. J. Circuit. Syst. Comp. 8, 1 (1998), 21--66.

[60]

Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. 2005. On the complexity of equational horn clauses. In Automated Deduction—CADE-20 (Lect. Notes Comp. Sci.), Vol. 3632. Springer, 337--352.

Digital Library

Cited By

Balasubramanian ASobocinski PLago UEsparza J(2024)Decidability and Complexity of Decision Problems for Affine Continuous VASSProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662124(1-13)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662124
Haar SHaddad S(2024)On the Expressive Power of Transfinite Sequences for Continuous Petri NetsApplication and Theory of Petri Nets and Concurrency10.1007/978-3-031-61433-0_6(109-131)Online publication date: 13-Jun-2024
https://doi.org/10.1007/978-3-031-61433-0_6
Finkel AHilaire M(2024)Resilience and Home-Space for WSTSVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_7(147-168)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50524-9_7
Show More Cited By

Index Terms

The Logical View on Continuous Petri Nets
1. Theory of computation

Recommendations

SAT-Solving the Coverability Problem for Petri Nets

Net unfoldings have attracted great attention as a powerful technique for combating state space explosion in model checking, and have been applied to verification of finite state systems including 1-safe (finite) Petri nets and synchronous products of ...
On persistent reachability in Petri nets

The notion of persistency, based on the rule ''no action can disable another one'' is one of the classical notions in concurrency theory. In this paper, we deal with arbitrary place/transition nets, but concentrate on their persistent computations. It ...
Linear time analysis of properties of conflict-free and general Petri nets

We introduce the notion of a T-path within Petri nets, and propose to adopt the model of directed hypergraphs in order to determine properties of nets; in particular, we study the relationships between T-paths and firable sequences of transitions. Let ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 18, Issue 3

July 2017

273 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3130378

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 August 2017

Accepted: 01 May 2017

Revised: 01 March 2017

Received: 01 September 2016

Published in TOCL Volume 18, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

ERC project EQualIS
Labex Digicosme, Univ. Paris-Saclay, project VERICONISS
Fonds de recherche du Québec - Nature et technologies (FRQNT)
“Chaire Digiteo, ENS Cachan— École Polytechnique”
French Centre national de la recherche scientifique (CNRS)

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
203
Total Downloads

Downloads (Last 12 months)22
Downloads (Last 6 weeks)3

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Balasubramanian ASobocinski PLago UEsparza J(2024)Decidability and Complexity of Decision Problems for Affine Continuous VASSProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662124(1-13)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662124
Haar SHaddad S(2024)On the Expressive Power of Transfinite Sequences for Continuous Petri NetsApplication and Theory of Petri Nets and Concurrency10.1007/978-3-031-61433-0_6(109-131)Online publication date: 13-Jun-2024
https://doi.org/10.1007/978-3-031-61433-0_6
Finkel AHilaire M(2024)Resilience and Home-Space for WSTSVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_7(147-168)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50524-9_7
Hofman PMazowiecki FOfftermatt P(2023)Fast Termination and Workflow NetsComputer Aided Verification10.1007/978-3-031-37706-8_7(132-155)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_7
Czerwiński WLefaucheux EMazowiecki FPurser DWhiteland M(2022)The boundedness and zero isolation problems for weighted automata over nonnegative rationalsProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533336(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533336
Blondin MMazowiecki FOfftermatt P(2022)Verifying Generalised and Structural Soundness of Workflow Nets via RelaxationsComputer Aided Verification10.1007/978-3-031-13188-2_23(468-489)Online publication date: 6-Aug-2022
https://doi.org/10.1007/978-3-031-13188-2_23
Blondin MEsparza J(2022)Separators in Continuous Petri NetsFoundations of Software Science and Computation Structures10.1007/978-3-030-99253-8_5(81-100)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99253-8_5
Finkel AHaddad SKhmelnitsky I(2021)Commodification of accelerations for the Karp and Miller ConstructionDiscrete Event Dynamic Systems10.1007/s10626-020-00331-z31:2(251-270)Online publication date: 1-Jun-2021
https://dl.acm.org/doi/10.1007/s10626-020-00331-z
Blondin MHaase COfftermatt P(2021)Directed Reachability for Infinite-State SystemsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72013-1_1(3-23)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72013-1_1
Blondin M(2020)The ABCs of petri net reachability relaxationsACM SIGLOG News10.1145/3436980.34369847:3(29-43)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1145/3436980.3436984
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents