Homogeneous Equations of Algebraic Petri Nets

Authors Marvin Triebel, Jan Sürmeli



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.14.pdf
  • Filesize: 0.61 MB
  • 14 pages

Document Identifiers

Author Details

Marvin Triebel
Jan Sürmeli

Cite AsGet BibTex

Marvin Triebel and Jan Sürmeli. Homogeneous Equations of Algebraic Petri Nets. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 14:1-14:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.14

Abstract

Algebraic Petri nets are a formalism for modeling distributed systems and algorithms, describing control and data flow by combining Petri nets and algebraic specification. One way to specify correctness of an algebraic Petri net model "N" is to specify a linear equation "E" over the places of "N" based on term substitution, and coefficients from an abelian group "G". Then, "E" is valid in "N" iff "E" is valid in each reachable marking of "N". Due to the expressive power of Algebraic Petri nets, validity is generally undecidable. Stable linear equations form a class of linear equations for which validity is decidable. Place invariants yield a well-understood but incomplete characterization of all stable linear equations. In this paper, we provide a complete characterization of stability for the subclass of homogeneous linear equations, by restricting ourselves to the interpretation of terms over the Herbrand structure without considering further equality axioms. Based thereon, we show that stability is decidable for homogeneous linear equations if "G" is a cyclic group.
Keywords
  • Algebraic Petri Nets
  • Invariants
  • Linear Equations
  • Validity
  • Stability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, and Mihaela Sighireanu. Invariant synthesis for programs manipulating lists with unbounded data. In CAV'10, volume 6174 of LNCS, pages 72-88. Springer, 2010. Google Scholar
  2. Hartmut Ehrig and Wolfgang Reisig. An algebraic view on petri nets. Bulletin of the EATCS, 61, 1997. Google Scholar
  3. Javier Esparza and Philipp Hoffmann. Reduction rules for colored workflow nets. In FASE'16, volume 9633 of LNCS, pages 342-358. Springer, 2016. Google Scholar
  4. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic. An smt-based approach to coverability analysis. In CAV'14, volume 8559 of LNCS, pages 603-619. Springer, 2014. Google Scholar
  5. Hartmann J. Genrich and Kurt Lautenbach. Special issue semantics of concurrent computation system modelling with high-level petri nets. Theoretical Computer Science, 13(1):109 - 135, 1981. Google Scholar
  6. Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Sylvain Schmitz, and Patrick Totzke. Coverability trees for petri nets with unordered data. In FOSSACS'16, pages 445-461, 2016. Google Scholar
  7. Kurt Jensen and Lars Michael Kristensen. Coloured Petri Nets - Modelling and Validation of Concurrent Systems. Springer, 2009. Google Scholar
  8. Kurt Jensen and Lars Michael Kristensen. Colored petri nets: a graphical language for formal modeling and validation of concurrent systems. Commun. ACM, 58(6):61-70, 2015. Google Scholar
  9. Gérard Memmi and Jacques Vautherin. Analysing nets by the invariant method. In Petri Nets: Central Models and Their Properties, pages 300-336, 1986. Google Scholar
  10. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1967. Google Scholar
  11. Wolfgang Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. Google Scholar
  12. Pierre-Alain Reynier and Arnaud Sangnier. Weak time petri nets strike back! In CONCUR'09, pages 557-571, 2009. Google Scholar
  13. Fernando Rosa-Velardo, María Martos-Salgado, and David de Frutos-Escrig. Accelerations for the coverability set of petri nets with names. Fundam. Inform., 113(3-4):313-341, 2011. Google Scholar
  14. Ognjen Savkovic, Elisa Marengo, and Werner Nutt. Query stability in monotonic data-aware business processes. In ICDT'16, volume 48 of LIPIcs, pages 16:1-16:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  15. Karsten Schmidt. Verification of siphons and traps for algebraic petri nets. In ICATPN'97, pages 427-446, 1997. Google Scholar
  16. M. Triebel and J. Sürmeli. Homogeneous Equations of Algebraic Petri Nets. ArXiv e-prints, June 2016. URL: http://arxiv.org/abs/1606.05490.
  17. T.A. Whitelaw. An introduction to abstract algebra. Blackie, 1978. Google Scholar