Petri nets and Span(Graph)

I have been thinking about Petri nets since a student of mine, Filippo Schiavio, has just written an interpreter for executing expressions in Span(Graph), with a graphic output (using the graphic package Graphviz). It seemed an idea to imitate some Petri net examples.

For the relation between Petri nets and multigraphs see this post.

The program Filippo wrote was based on the fact that expressions in  symmetric monoidal category in which every object has a separable algebra structure compatible with the tensor may be represented as cospans of multigraphs (a fact we discussed in [1] and [2], but rediscovered by Filippo). By a multigraph I mean a pair of functions d0,d1: Arcs -> Vertices* (Vertices* is the free monoid on Vertices), so every arc has a list of input vertices and a list of output vertices. Commonly for a multigraph the arcs are represented as boxes rather than arrows, and the vertices as (nodes on) wires rather than plain nodes. The program works by calculating in Cospan(Multigraph) the multigraph of a Span(Graph) expression before then calculating an execution essentially by finding elements in the limit of the multigraph diagram of spans.

An example of a Petri-net like expression in Span(Graph) for mutual exclusion between two processes.

If you click on the design you will see a  short (but repeated)  execution, in which green means non-critical actions, red means critical actions, and blue is a permision to enter the critical region.The first frame has the names of the components and the second the initial states.

The graphical output while useful  is not quite what we would like because GraphViz doesn't easily accomodate multigraphs.

Here is the code for  for Filippo's interpreter  describing the above expression of spans of graphs.

// Analogue of a Petri net for mutal exclusion. There are really only three special components d=delay, synch=synchronizer, and choose. Other components were introduced to simplify the expression and to improve the display

bsync=span(3,1){
00, 01, 10, 11
00 -> 00 : 0,0,0/0
// 00 -> 10 : 0,3,0/0
00 -> 01 : 0,0,1/0
00 -> 11 : 0,3,1/0
10 -> 11 : 5,0,1/0
10 -> 10 : 5,0,0/0
01 -> 11 : 5,3,0/0
01 -> 01 : 5,0,0/0
11 -> 00 : 0,0,0/2
}

tsync=span(3,1){
00, 01, 10, 11
00 -> 00 : 0,0,0/0
00 -> 10 : 1,0,0/0
// 00 -> 01 : 0,3,0/0
00 -> 11 : 1,3,0/0
10 -> 11 : 0,3,5/0
10 -> 10 : 0,0,5/0
01 -> 11 : 1,0,5/0
01 -> 01 : 0,0,5/0
11 -> 00 : 0,0,0/2
}

choose=span(2,2){
x -> x : 0,0/0,0
x -> y : 0,1/0,0
y -> y : 0,0/0,0
x -> y : 1,0/0,0
y -> x : 0,0/0,3
y -> x : 0,0/3,0
}

d=span(1,1){
0->0 : 0/0
0->1 : 1/0
1->1 : 1/1
1->0 : 0/1
}

crit=span(1,1){
0->0 : 0/0
0->1 : 2/0
1->1 : 2/1
1->0 : 0/1
}


d3=d;d;d
d4=d;d;d;d


diagonal_delay = crit ; D

expr = (tsync * bsync) ; (diagonal_delay * diagonal_delay) ; (ID * choose * ID) ; ( d3 * ID * ID * d4)

expr_feed = (U * ID * ID * U) ; (ID * U * ID * ID * ID * ID * U * ID) ; (ID * ID * expr * ID * ID) ; (ID * CU * ID * ID * CU * ID) ; (CU * CU)

 ProceedToNextStateDrawingGraph(expr_feed,[00,00,0,0,y,1,0,0,0,0,1,0],99,out_petri/,out_petri/,{
transitions_colors -> {0 -> white, 1-> green,2 -> red, 3 -> blue, 5 -> yellow}
})

//----------------------------------------------------

We actually did write a paper [3] describing the implementation of Petri nets in Span(Graph) in 1997.

[1] R. Rosebrugh, N. Sabadini, R.F.C. Walters, Calculating colimits compositionally, Montanari Festschrift, LNCS 5065, pp. 581–592, 2008.(also arXiv:0712.2525)

[2] R. Rosebrugh, N. Sabadini, R.F.C. Walters, Generic commutative separable algebras and cospans of graphs, Theory and Applications of Categories, 15, 264-177, 2005.

[3] Katis P, Sabadini N, Walters RFC, Representing P/T nets in Span(Graph), Proceedings AMAST '97, SLNCS 1349, 307-321, 1997.