Based on a draft version of ISO/IEC 15909-1:2004 High-level Petri nets - Part 1: Concepts, definitions and graphical notation.

Useful for setting the ontology.

Arc inscriptions are expressions that are evaluated.

Place markings are multisets of tokens of a sort/type.

Transition conditions are boolean expressions that are evaluated. Used to determine if transition is enabled.

Expressions in pnml can be many-sorted algebras. Declaration, Term, Sort, Multiset, Variable, are among the concepts used to define expressions.

Terms

Terms have sorts: the sort of the variable or the output sort of the operator.

Terms can be buit from built-in operators and sorts, and user-defined variables. These are defined in variable declarations, a kind of annotation label attached to pages and nets.

A transition can have a condition, a term of sort boolean, which imposes restrictions on when the transition may fire.

Sorts

named sorts are constructed from existing sorts and given a new name.

arbitrary sort is not defined in core, is not allowed in Symmetric Nets. HLPNG adds arbitrary declarations, sorts of lists, strings, integers to Symmetric Nets.

The sort of a term is the sort of the variable or the output sort of the operator.

Operators

An operator can be: built-in constant, built-in operator, multiset operator or tuple operator.

User-defined operators, or named operators are abbreviations, built from existing operators and parameter variables.

There will be arbitrary operator declarations for High-Level Petri Net Graphs, but not for Symmetric Nets.

Operators have a sequence of input sorts and a single output sort.

Variables

TBD

Notes on Petri Nets

Multiset Rewriting Systems

I. Cervesato: Petri Nets as Multiset Rewriting Systems in a Linear Framework

This addresses Place Transition Nets. High-level Petri nets explictily use multisets.

factor out the multiplicity of the elements of the underlying set. This is achieved by first defining the notion of singleton multisets and then by writing arbitrary multisets as linear combination of singleton multisets.

a rewrite rule can be viewed as a singleton multiset

Petri nets are meant to represent evolving systems. To represent this dynamic flavor, we will rely on the notion of multiset rewriting systems.

Continuous, Open and Other Petri Nets

Allow marking, inscription, conditions to be floating point even when standard wants an integer. This allows continuous nets.

See Petri.jl and AlgebraicPetri.jl for some continuous Petri Net use-cases.

TODO: Hybrid nets combining floating point/continuous and integer/discrete inscription/marking.