TY - JOUR
T1 - Petri nets are monoids
AU - Meseguer, José
AU - Montanari, Ugo
N1 - Funding Information:
* Supported by Office of Naval Research Contracts NOOO14-86-C-0450 and NOOO14-88-C-0618, NSF Grant CCR-8707155 and by a grant from the System Development Foundation. A summarized version of this paper appeared in Meseguer and Montanari (1988). ’ Also Center for the Study of Language and Information, Stanford University, Stanford, California 94305. * Dipartimento di Informatica, Universita di Pisa, I-56100 Pisa, Italy; research performed while on leave at SRI International.
PY - 1990/10
Y1 - 1990/10
N2 - Petri nets are widely used to model concurrent systems. However, their composition and abstraction mechanisms are inadequate: we solve this problem in a satisfactory way. We start by remarking that place/transition Petri nets can be viewed as ordinary, directed graphs equipped with two algebraic operations corresponding to parallell and sequential composition of transitions. A distributive law between the two operations captures a basic fact about concurrency. New morphisms are defined, mapping single, atomic transitions into whole computations, thus relating system descriptions at different levels of abstraction. Categories equipped with products and coproducts (corresponding to parallel and nondeterministic compositions) are introduced for Petri nets with and without initial markings. Petri net duality is expressed as a duality functor, and several new invariants are introduced. A tensor product is defined on nets, and their category is proved to be symmetric monoidal closed. This construction is generalized to a large class of algebraic theories on graphs. These results provide a formal basis for expressing the semantics of concurrent languages in terms of Petri nets. They also provide a new understanding of concurrency in terms of algebraic structures over graphs and categories that should apply to other models besides Petri nets and thus contribute to the conceptual unification of concurrency.
AB - Petri nets are widely used to model concurrent systems. However, their composition and abstraction mechanisms are inadequate: we solve this problem in a satisfactory way. We start by remarking that place/transition Petri nets can be viewed as ordinary, directed graphs equipped with two algebraic operations corresponding to parallell and sequential composition of transitions. A distributive law between the two operations captures a basic fact about concurrency. New morphisms are defined, mapping single, atomic transitions into whole computations, thus relating system descriptions at different levels of abstraction. Categories equipped with products and coproducts (corresponding to parallel and nondeterministic compositions) are introduced for Petri nets with and without initial markings. Petri net duality is expressed as a duality functor, and several new invariants are introduced. A tensor product is defined on nets, and their category is proved to be symmetric monoidal closed. This construction is generalized to a large class of algebraic theories on graphs. These results provide a formal basis for expressing the semantics of concurrent languages in terms of Petri nets. They also provide a new understanding of concurrency in terms of algebraic structures over graphs and categories that should apply to other models besides Petri nets and thus contribute to the conceptual unification of concurrency.
UR - http://www.scopus.com/inward/record.url?scp=0025500231&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0025500231&partnerID=8YFLogxK
U2 - 10.1016/0890-5401(90)90013-8
DO - 10.1016/0890-5401(90)90013-8
M3 - Article
AN - SCOPUS:0025500231
SN - 0890-5401
VL - 88
SP - 105
EP - 155
JO - Information and Computation
JF - Information and Computation
IS - 2
ER -