Linear Logic and Petri Nets

Wow! Elena Di Lavore and Xiaoyan Li explained how to make a category of Petri nets that’s a model of linear logic! I consider myself a sort of expert on Petri nets, but I didn’t know this stuff:

• Elena Di Lavore and Xiaoyan Li, Linear logic flavoured composition of Petri nets, The n-Category Café, 27 July 2020.

It has great pictures, too. Let me summarize a tiny bit.

A Petri net is a very simple thing. Here’s a Petri net that shows how healthy white blood cells (H), individual viruses (V) and infected white blood cells (I) interact when someone gets AIDS:

The yellow boxes are different kinds of things, called species; the aqua boxes are processes, called transitions.

There are different ways to form categories using Petri nets. Jade Master and I have focused on two:

1) How to turn a Petri net into a category where the morphisms say what the Petri net can do.

2) How to make a category with ‘open’ Petri nets as morphisms. Composing these lets you build big Petri nets from smaller pieces.

Di Lavore and Li instead explain:

3) How to make a category with elementary Petri nets as objects: a morphism from one elementary Petri net to another turns each transition of the first into a transition of the second.

An elementary Petri net is one where each transition uses each species at most once as an input and at most once as an output:

The category they get has lots of interesting structure! Like products, shown here:

In fact it has products, coproducts, two other monoidal structures, and exponentials—all fitting together in a wonderful way, as described by intuitionistic linear logic! To prove this, the key is to use Valeria de Paiva’s work on “Dialectica categories”. They explain how.

This is not original research: Elena Di Lavore and Xiaoyan Li wrote this blog article for the ACT2020 Adjoint School, and they’re explaining Carolyn Brown and Doug Gurr’s paper “A categorical linear framework for Petri nets”.

It’s worth comparing this paper:

• Uffe Engberg and Glynn Winskel, Petri nets as models of linear logic, in Colloquium on Trees in Algebra and Programming, Springer, Berlin, 1990, pp. 147–161.

Engberg and Winskel get a model of linear logic—or to be precise, a ‘commutative quantale’—by taking the category you get from a single Petri net as in item 1) and massaging it a bit. I explained it here:

• John Baez, Quantales from Petri nets, Azimuth, 6 October 2019.