Mathematical Structures in Computer Science · 2020 · 55 citations · 26 references
ComputingComputer ScienceDiagrammingFormal MethodsSemanticsCategory TheoryCompositional SemanticsPetri NetsMonoidal CategoriesOperational SemanticsPetri Net ModelsPetri Net SemanticsReachabilityStructural Operational SemanticsSubnets
Abstract The reachability semantics for Petri nets can be studied using open Petri nets. For us, an “open” Petri net is one with certain places designated as inputs and outputs via a cospan of sets. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Open Petri nets can be treated as morphisms of a category Open(Petri), which becomes symmetric monoidal under disjoint union. However, since the composite of open Petri nets is defined only up to isomorphism, it is better to treat them as morphisms of a symmetric monoidal double category ${\mathbb O}$ pen (Petri). We describe two forms of semantics for open Petri nets using symmetric monoidal double functors out of ${\mathbb O}$ pen (Petri). The first, an operational semantics, gives for each open Petri net a category whose morphisms are the processes that this net can carry out. This is done in a compositional way, so that these categories can be computed on smaller subnets and then glued together. The second, a reachability semantics, simply says which markings of the outputs can be reached from a given marking of the inputs.
26
An Algorithm for the General Petri Net Reachability Problem
Ernst Mayr · SIAM Journal on Computing · 1984 · 457 citations
José Meseguer, Ugo Montanari · Information and Computation · 1990 · 353 citations
Categories of continuous functors, I
Peter Freyd, G. M. Kelly · Journal of Pure and Applied Algebra · 1972 · 326 citations