M-nets: An algebra of high-level Petri nets, with an application to the semantics of concurrent programming languages. This paper describes a high-level Petri net model called M-nets (for modular multilabelled nets). A distinctive feature of this model is that it allows both: unfolding, as do most other high-level net models; and composition – in particular, synchronisation – in a process algebraic style, turning the set of M-nets into an algebraic domain. It turns out that the composition operations of this domain have various algebraic properties. Moreover, the model is such that composition operations are coherent with unfolding, in the sense that the unfolding of a composite high-level net is the composition of the unfoldings of its components. One of the motivations for M-nets is that they be a vehicle for giving semantics of concurrent programming languages. To illustrate their capability for that, the compositional semantics of B(PN)2 – a simple, expressive concurrent programming language – is given. An associated low-level net semantics is described, and the coherence of these high-level and low-level semantics is proved.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Kindler, Ekkart: Modelling local and global behaviour: petri nets and event coordination (2012)
- Valero, Valentín; Macià, Hermenegilda; Pardo, Juan José; Cambronero, María Emilia; Díaz, Gregorio: Transforming web services choreographies with priorities and time constraints into prioritized-time colored Petri nets (2012)
- Ciobanu, Gabriel; Koutny, Maciej: Timed mobility in process algebra and Petri nets (2011)
- Thanh, Cécile Bui; Klaudel, Hanna: Object-oriented modelling with high-level modular Petri nets (2004)
- Devillers, Raymond; Klaudel, Hanna; Riemann, Robert-C.: General parameterised refinement and recursion for the M-net calculus (2003)
- Thanh, C.Bui; Klaudel, H.; Pommereau, F.: Petri nets with causal time for system verification (2003)
- Klaudel, Hanna; Pommereau, Franck: A class of composable and preemptible high-level Petri nets with an application to multi-tasking systems (2002)
- Klaudel, Hanna: Compositional high-level Petri net semantics of a parallel programming language with procedures (2001)
- Klaudel, Hanna; Pommereau, Franck: A concurrent semantics of static exceptions in a parallel programming language (2001)
- Klaudel, Hanna; Pommereau, Franck: Asynchronous links in the PBC and M-nets (1999)