×

Flexibility in algebraic nets. (English) Zbl 1523.68043

Desel, Jörg (ed.) et al., Application and theory of Petri nets 1998. 19th international conference, ICATPN’98, Lisbon, Portugal, June 22–26, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1420, 345-364 (1998).
Summary: Algebraic Petri nets as defined by W. Reisig [Theor. Comput. Sci. 80, No. 1, 1–34 (1991; Zbl 0727.68080)] lack a feature for modelling distributed network algorithms, viz. flexible arcs. In this paper we equip algebraic Petri nets with flexible arcs and we call the resulting extension algebraic system nets. We demonstrate that algebraic system nets are better suited for modelling distributed algorithms.
Besides this practical motivation for introducing algebraic system nets there is a theoretical one. The concept of place invariants introduced along with algebraic Petri nets has a slight insufficiency: There may be place invariants of an unfolded algebraic Petri net which cannot be expressed as a place invariant of the algebraic Petri net itself. By introducing algebraic system nets along with a slightly more general concept of place invariants we also eliminate this insufficiency.
Moreover, we generalize the concept of place invariants which we call simulations. Many well-known concepts of Petri net theory such as siphons, traps, modulo-invariants, sur-invariants and sub-invariants are special cases of a simulation. Still, a simulation can be verified in the same style as classical place invariants of algebraic Petri nets.
For the entire collection see [Zbl 1499.68015].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68W15 Distributed algorithms

Citations:

Zbl 0727.68080
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] E. Best and C. Fernández. Nonsequential Processes. Springer, 1988. · Zbl 0656.68005
[2] J. Billington. Extending coloured Petri nets. Technical Report 148, University of Cambridge, Computer Laboratory, Oct. 1988.
[3] J. Billington. Extensions to Coloured Petri Nets and their Application to Protocols. Technical Report 222, University of Cambridge, May 1991.
[4] M. Broy. On the design and verification of a simple distributed spanning tree algorithm. SFB-Bericht 342/24/90 A, Technische Universtität München, Dec. 1990.
[5] J. Desel, K.-P. Neuendorf, and M.-D. Radola. Proving nonreachability by moduloinvariants. Theoretical Computer Science, 153:49-64, 1996. · Zbl 0872.68131 · doi:10.1016/0304-3975(95)00117-4
[6] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 1, Equations and Initial Semantics, Springer, 1985. · Zbl 0557.68013
[7] U. Goltz and W. Reisig. The non-sequential behaviour of Petri nets. Information and Control, 57:125-147, 1983. · Zbl 0551.68050 · doi:10.1016/S0019-9958(83)80040-0
[8] K. Jensen. Coloured Petri Nets, Volume 1: Basic Concepts. Springer, 1992. · Zbl 0762.68004
[9] K. Jensen. Coloured Petri Nets. Volume 2: Analysis Methods. Springer, 1995. · Zbl 0865.68084
[10] E. Kindler and W. Reisig. Algebraic system nets for modelling distributed algorithms. Petri Net Newsletter, 51:16-31, Dec. 1996.
[11] E. Kindler and W. Reisig. Verification of distributed algorithms with algebraic Petri nets. In C. Freksa, M. Jantzen, and R. Valk, editors, Foundations of Computer Science: Potential — Theory — Cognition, LNCS 1337, pp. 261-270. Springer 1997. · Zbl 0899.68058
[12] E. Kindler, W. Reisig, H. Völzer, and R. Walter. Petri net based verification of distributed algorithms: An example. Formal Aspects of Computing, 9:409-424, 1997. · Zbl 0889.68071 · doi:10.1007/BF01211299
[13] E. Kindler and H. Völzer. Flexibility in algebraic nets. Informatik-Bericht 89, Humboldt-Universität zu Berlin, Institut für Informatik, 1997. Available at http://www.informatik.hu-berlin.de/ kindler/papers.html · Zbl 1523.68043
[14] G. Memmi and G. Roucairol. Linear algebra in net theory. In W. Brauer, editor, Net Theory and Applications, LNCS 84, pp. 213-223. Springer, Oct. 1979.
[15] J. L. Peterson. Petri Net Theory And The Modeling of Systems. Prentice-Hall 1981. · Zbl 0461.68059
[16] W. Reisig. Petri Nets, Springer, 1985. · Zbl 0555.68033
[17] W. Reisig. Petri nets and algebraic specifications. Theoretical Computer Science, 80:1-34, May 1991. · Zbl 0727.68080 · doi:10.1016/0304-3975(91)90203-E
[18] W. Reisig. Petri net models of distributed algorithms. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, LNCS 1000, pp. 441-454. Springer, 1995. · Zbl 0875.00060
[19] K. Schmidt. Verification of siphons and traps for algebraic Petri nets. In P. Azéma and G. Balbo, editors, Application and Theory of Petri Nets 1997, International Conference, Proceedings, LNCS 1248, pp. 427-446. Springer, June 1997. · Zbl 1510.68069
[20] E. Smith and W. Reisig. The semantics of a net is a net, an exercise in general net theory. In K. Voss, H. Genrich, and G. Rozenberg, editors, Concurrency and Nets. Springer, 1987. · Zbl 0635.68055
[21] R. Valk. Bridging the gap between place-and Floyd-invariants with applications to preemptive scheduling. In M. A. Marsan (ed), Application and Theory of Petri Nets 1993, International Conference, Proceedings, LNCS 691, pp. 431-452. Springer, June 1993.
[22] J. Vautherin. Parallel systems specifications with coloured Petri nets and algebraic specifications. In G. Rozenberg, editor, Advances in Petri Nets, LNCS 266, pp. 293-308. Springer, 1987. · Zbl 0633.68053
[23] H. Völzer. Verifying fault tolerance of distributed algorithms formally: An example. In CSD98, ‘International Conference on Application of Concurrency to System Design’, Aizu-Wakamatsu City, Japan, Mar. 1998. IEEE Computer Society Press.
[24] M. Weber, R. Walter, H. Völzer, T. Vesper, W. Reisig, S. Peuker, E. Kindler, J. Freiheit, and J. Desel. DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen. Informatik-Bericht 88, Humboldt-Universität zu Berlin, Dec. 1997.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.