Keywords: Rewriting Logic, Algebraic Petri Nets, Coloured Petri Nets, High-Level Petri Nets
Petri nets have been developped by Carl Adam Petri in 1962 and are a graphical, intuitive but formal means to specify concurrent and distributed systems. Due to the practical demand for an increase in expressivity and modelling power various kinds of high-level Petri nets have been proposed and implemented in Petri net tools. The graphical nature of Petri nets makes them a suitable formalism to brige the gap between formal methods and visual specification techniques, two fields that are receiving considerable attention in academia and industry at present.
Coloured Petri nets are one of the most popular high-level Petri net formalisms that still preserve the essential principles of the basic model of place/transition nets. They combine a language to describe describe data types and operations with Petri nets to capture synchronization, concurreny, nondeterminsm and flow of data objects. The underlying language of coloured Petri nets can be just set theory (which comes for free if we use a shallow embedding). However, since execution is an important validation technique, a (functional) programming language can be more suitable. As essential feature of a coloured Petri net is however that as a system model it is completely determined in every aspect, just as in a programming language every program has a single well-defined denotation.
Migrating from a single coloured Petri net to a possibly rich class of Petri nets yields some advantages that have first been observed in the context of algebraic Petri net specifications which use an algebraic specification language to specify data types and operations. Instead of specifying a single system model, an algebraic Petri net represents a class of models that often differ only in a few parameters. Such a compact parameterized description is unavoidable for modular specification and economic verification of net models.
In this project we further develop the idea of Petri net specifications using more expressive languages, such as membership equational logic that generalizes pure algebraic specification languages considerably. Simultaneously, we use rewriting logic which contains membership equational logic as a sublanguage, to equip net specifications with a rewriting semantics. The rewriting semantics reduces the gap between Petri nets and equational specification languages and has a number of applications such as high-speed execution, exploration and analysis of system models. Furthermore, the rewriting semantics provides a formal representation of nets specifications that can be a basis for abstract execution and rigorous formal verification using interactive theorem proving.
We expect that the unifying view suggested by rewriting logic can help to cope with the diversity of high-level Petri nets models that are in use today and we think that it may also provide a guideline for further generalizations. On the practical side, the rewriting semantics suggests a new approach to developping tools for Petri nets using existing rewriting technology such as the Maude engine. Since rewriting logic can serve as a framework for other formal systems such as logics and programming languages the approach should also lead to a better integration between Petri nets, formal theorem proving, and other paradigms that can be naturally expressed in rewriting logic, object-oriented and agent-oriented specification/programming being only one example.
Relevant References: