A Compositional Framework for Petri Nets

We define a bidirectional compositional framework for Petri nets based on a line of work about compositionally defining games and computation models. This relies on defining structures with open ends that form interfaces they can be composed along. Together with this syntactic construction, we give a graphical language of morphisms in a PROP and a semantic category that describes the evolution of markings in a Petri net. Compared to previous work, the novelty is that computations in a Petri net are stateful, requiring specific care. This framework allows us to solve reachability compositionally.