Good Math, Bad Math

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.

i-7c3ed91904f3eecb56075c2de22ea09e-colored-net.png

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:

i-9723bce5b4c7aa921dcff8659e320348-petri-protocol.png

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?

Comments

  1. #1 Samuel A. Falvo II
    October 10, 2007

    To me, PNs look and apparently behave exactly the same as ordinary flowcharts. A type-safe flowchart would be a CPN then. I guess I’m a bit underwhelmed by their significance.

  2. #2 rodrigo
    October 10, 2007

    @Samuel,

    You’re failing to take into account that places in a PN can accumulate tokens for a while, until a condition (maybe affecting a different place) is met.

    If you think of control in a flowchart as represented by a (single) token that moves from action to action, the big difference would be that a PN can have several tokens moving at once through it.

  3. #3 rodrigo
    October 10, 2007

    Mark, I think the NextToSend node should be type int, not (int, data).

  4. #4 Reinier Post
    October 11, 2007

    Samuel and rodrigo:

    Not only that, but Petri nets are also concurrent splits and joins: when a transition fires, it consumes a token on *every* incoming arc, and produces a token on *every* outgoing ars. Flowcharts do not support this (activity diagrams do).

    With Petri nets, you list all the different tasks that need to be done; then, you list all the relevant conditions (pre- and postconditions to tasks) and you connect them with arrows. With flowcharts, you also need to remove all the nondeterminism by picking the exact order in which the steps will actually be taken. That is not always something you need to do. It is if all of these tasks are going to be executed by a single processor (e.g. a single person) and that processor needs to be supplied in advance with a fully deterministic procedure for determining the next step to take at every point, before it can even start to do any work. Single-processor computers are a bit like that, but they are the exception rather than the rule.

  5. #5 Jon L
    October 11, 2007

    Good post. Lately you’ve been following my algorithms class pretty well. We did studied gauss’s fast multiplication a few weeks before your fast addition post and we just finished the basics of graphs (in fact most of the test I just took was about finding red and blue verticies in a graph. Not the same as colored petri nets, but kinda similar.) FYI, the next chapter is on greedy algorithms.

    Anyway, my question is how does this tie into pi-calculus (as I’m sure it does). Are places representations of channels and is there any way to do process replication? colored petri nets seem much more intuitive for understanding concurrency than pi-calculus.

  6. #6 Doug
    October 12, 2007

    http://flash.lakeheadu.ca/~dlaw/3251.htmlHi Mark,

    I had not thought of using color in this manner.

    I have seen color used in biochemistry metabolic pathways:
    http://flash.lakeheadu.ca/~dlaw/3251.html

    Multiple tokens may take the form of various energy quanta such as ATP and other nucleotides, protons or electrons in transfer, for example.

  7. #7 Reinier Post
    October 13, 2007

    Jon L:

    Pi calculus was designed for mobile processes, where communication channels are determined and established dynamically.

    I believe names in pi calculus play a role similar to places in Petri nets. Pi calculus also has a diagrammatic notation. So there is some similarity.

    But pi calculus can pass names around to remote processes, which can then establish communication with them. It’s as if you have Petri nets in which places are passed around as tokens, after which some receiving transition dynamically creates arcs to or from them. While this sort of thing is possible in some extensions of Petri nets (R. Valk already published on “Self-modifying Petri nets” in 1978), it is not very typical. Most Petri nets, including most colored ones, have a fixed structure.

  8. #8 Torbjörn Larsson, OM
    October 13, 2007

    energy quanta

    References to old quantum theory are confusing in modern days.

    In any case, if the term still makes sense it is as the force carriers produced by quantization of fields, or possibly as pseudoparticles produced by quantized collective excitations in other systems (such as phonons in solids).

    That molecules have quantized states is a different thing. And in some cases of chemical interactions (like van der Waal forces) I doubt we can attribute any localized state.

The site is currently under maintenance and will be back shortly. New comments have been disabled during this time, please check back soon.