Colored Petri Nets

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:

1. There are a single sender, and a single reciever.
2. 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.
3. The sender sends a packet of data to the reciever.
4. If the packet number received by the receiver is correct, then the receiver signals the sender
   that it's ready for the next packet.
5. 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.
6. 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:

1. 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.
2. "SendPacket" is only enabled for tokens from "Send" and "NextToSend" which have matching integers - thus, packet 1.
3. "SendPacket" fires, sending the token for packet one to "A", which enables "TransmitPacket", which sends it to "B".
4. Now, things get a bit interesting. "B" sends it to "ReceivePacket", which then looks at
   the integer sequence number, "n":
   1. 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".
   2. 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".
5. Whatever desired packet number was send by "RecievePacket" percolates forward to "NextToSend",
   where it starts the whole process over for the requested packet.
6. 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?