Colored Petri Nets

The big step in Petri nets – the one that really takes them from a theoretical toy to a

serious tool used by protocol developers – is the extension to *colored* Petri nets (CPNs). Calling them “colored” is a bit of a misnomer; the original idea was to assign colors to tokens, and allow color-based expressions on the elements of the net. But study of analysis models quickly showed

that you could go much further than that without losing the basic analyzability properties

that are so valuable. In the full development of CPNs, you can associate essentially arbitrary

collections of data with Petri net tokens, so long as you use a strong type system, and keep

appropriate restrictions on the expressions used in the net. The colors thus become

data types, describing the types of data that can be carried by tokens, and the kinds of tokens that

can located in a place in the net.

So that’s the fundamental idea of CPNs: tokens have types, and each token type has some data value associated with it. Below the fold, we’ll look at how we do that,

and what it means.

Colored Petri nets add a collection of extensions to the other elements of the net to take advantage of typed tokens carrying values:

- Each place in the net is also assigned a data type, and can only hold tokens of

its assigned type type. - Incoming edges of a transition can have
*conditions*: the transition is only

enabled when some set of tokens from the source places satisfy the full set of conditions

for its incoming edges. The conditions for the incoming edges of a transition can

reference the values from other incoming edges of the same transition – so, for example,

the conditions can require that the values of two tokens coming from different incoming

values match. - The edges going out of a transition can have
*expressions*specifying how to compute the

values of tokens being produced by the transition. When a transition is

successfully fired, the expressions on its outgoing edges are evaluated to produce new tokens

to feed into the place at the end of the edge.

Let’s look at a quick example of a CPN transition. Here’s a very simple CPN. It’s got 3 places: two of them have type

(Int×String), and one has type (Int). The transition takes one token of the pair type, and one of the integer type; and it produces one token of the pair type. The edges coming into the transition declare names for the elements of the token values, and the edge leaving the transition describes how to generate the values for outgoing tokens. This little net starts with two tokens, (4,”Foo”), and (2). The transition only fires if the integer token has a value greater than or equal to one, and produces a token multipying the two integers from the incoming token. So the transition would fire, consuming two two tokens shown in the graph, and producing a token (8, “Foo”) in the bottom place.

For colored nets, there are a ton of variations. The basic idea is that there’s some simple version of λ-calculus which is associated with elements of the CPN:

- Places are assigned lambda calculus types, which define the types of values carried by tokens that can be located in the place. At runtime, the place is a
*bag*of tokens. - Transitions are basically functions, where the incoming edges define a tuple of input parameters to the function, and the outgoing edges form a tuple of results from the function.

For our example, the transition is, basically “&lamba; (v,s),w → (v*w,s)”. - The transition can have
*conditions*for its firing: the condition will only

be enabled for incoming token values which meet the condition. In the example, the condition

is that the value coming on the edge from the integer-place must have a value greater than

or equal to one. This turns the lambda function into a guarded partial function: in our example, “&lamba; (v,s),w | w >= 1 → (v*w,s)”.

The power here should be obvious: there’s a lot more capability in colored nets than there were in

simple Petri nets. Colored nets are potentially Turing complete. But for tractability, implementations

often place constraints on the calculus used by the transitions to limit it to something simpler. Since Petri nets are used mainly for describing concurrency and coordination schemes, they don’t generally

need to be Turing complete, and by constraining the calculus, you get the ability to perform analyses

on the scheme defined by the net which can produce useful results. For example, you can prove that

there are no possible deadlocks; you can prove that some event X never occurs before some other

event Y; etc.

Let’s take a look at a real example of a colored net. This is a slightly simplified version of a net taken from a paper introducing colored Petri nets, written by a group that implements a CPN design and analysis tool:

It describes a very

simple communication protocol, which that works as follows:

- There are a single sender, and a single reciever.
- Both the sender and the reciever have a common sequence number, which is used to indicate that

they’re in sync with one another, and no data was lost. - The sender sends a packet of data to the reciever.
- If the packet number received by the receiver is correct, then the receiver signals the sender

that it’s ready for the next packet. - If the packet number recieved by the receiver is not correct, then it signals the sender

with the number of the packet that it’s expecting. - The sender can resend a packet no more than three times.

.

The Colored Petri net for this is a relatively straightforward rendition of the description

above. In this net, the green places and transitions are on the sender; the pink are the reciever; and the gold are the network. The shaded places are the places that indicate the point where tokens are transferred between entities. It works as follows:

- The net is initialized with 4 copies of tokens containing each packet of data in the “Send” place, and the integer “1” in both “NextToSend” and “NextRec”. So “NextToSend” initially contains one token, which contains the value 1, and “Send” contains a bunch of tokens containing data to send, numbered in order.
- “SendPacket” is only enabled for tokens from “Send” and “NextToSend” which have matching integers – thus, packet 1.
- “SendPacket” fires, sending the token for packet one to “A”, which enables “TransmitPacket”, which sends it to “B”.
- Now, things get a bit interesting. “B” sends it to “ReceivePacket”, which then looks at

the integer sequence number, “n”:- If “n” matches the integer “k” stored in “NextRec”, then “ReceivePacket” fires, sending

a token containing “n+1” to “NextRec”, and sending a token to “C” indicating that it

next wants to receive token “n+1”. - If “n” does not match “k”, then “RecievePacket” fires, sending a token containing “k”

to “C”, indicating that the reciever still hasn’t recieved packet “k”.

- If “n” matches the integer “k” stored in “NextRec”, then “ReceivePacket” fires, sending
- Whatever desired packet number was send by “RecievePacket” percolates forward to “NextToSend”,

where it starts the whole process over for the requested packet. - If the sequencing got mangled (because of data loss along the network), the protocol basically

requests a resend – that’s what the logic of “RecievePacket” is all about. Since there are four

copies of each packet in “Send”, it can re-send up to 3 times. (The initial send, and 3 re-sends.)

Hopefully, from this you can see the basic ideas of Petri nets. There are numerous other variants: stochastic Petri-nets, genomic Petri nets, heirarchical Petri nets, and more. But the basic idea

always remains the same: there are places that contain tokens, and transitions that consume one set of tokens and produce another; and the transitions provide a synchronization point for the processes that

have edges into them. From that basis, you get a great amount of power, and also a great amount of

analyzability.

Remember the rant that I started with, about Estelle, the formal specification language with no useful formal properties? A french group did produce a useful tool based on a variant of Estelle, called Esterelle. What Esterelle did was adopt colored petri net semantics, and constrained the actions

of the Estelle transition arcs to things that could be expressed in a CPN. Of course, that’s still a strange idea: they were taking a language based on communicating FSMs, and giving it semantics and

restrictions based on CPNs. Why not just give up and use the Petri nets?