Simulating "counted Petri nets" - an idea

Counted Petri nets are brought up by Mark Chu-Carroll in his blog

Counted Petri nets, he writes, extend standard Petri nets by specifying on each transition a capacity that specifies (or limits, I'm not quite clear on that, but I'll assume: specifies) the number of tokens a transition consumes from its input places. Clearly this number must always be at least 1 and at most the total number of input arcs in order to be meaningful.

How useful is this extension? Clearly, counted nets are at least as expressive as standard Petri nets, since the latter are subsumed as a special case (namely, the nets in which all transition capacities have the maximum values). But are they more expressive? Can we state things with them that cannot be stated with standard Petri nets?

In the most literal sense, we can: transition capacities are absent from standard Petri nets, and they clearly add meaning, affecting the execution semantics in a well-defined way.

But we can be a little more relaxed and just ask ourselves: does there exist, for every counted Petri net, some standard Petri net that is in some sense equivalent to that counted net?

Many kinds of equivalences are meaningful to consider. I don't want to discuss such equivalences here in general.

Instead, I want to look at particular mappings from counted nets to Petri nets and the equivalences they establish.

A direct simulation of counted nets with standard nets

The obvious way to translate counted nets into standard nets is to duplicate the transitions. For each transition with m input arcs and capacity n, introduce a transition for each possible combination of n out of the m input arcs, and remove the original transition. A firing of the original transition corresponds to a firing of one of its replacements in the result, and vice versa. In process-theoretical terms, we have created a simulation of the original counted Petri net.

This translation establishes a very close correspondence. But there is one slight drawback: a transition is replaced with a number of transitions that is, in general, exponential in the number of the transition's input arcs - so unless the number of input arcs of transitions stays below a fixed maximum, in general the transformation causes nets to blow up exponentially in size.

Multi-step, linear simulation of counted nets with standard nets

But there is another approach to translation. The idea is to implement the effect of the transition capacity by adding extra steps. One approach is to simply carry out the transition as if no capacity were specified, then put the right number of tokens back into the input places; another approach is to consume the tokens from the inputs one by one, with separate transitions, and additional transitions to ensure that the exact right number of tokens is consumed.

This doesn't produce as good a similarity: a firing of a transition is now simulated by a sequence of firings of transitions. Process theorists call these translations weak bisimulations, if I'm not mistaken.

The diagram shows the first construction on the left; it is a proper extension of the original counted net, except that the transition capacity becomes superfluous and can therefore be omitted.

The second construction is illustrated on the right.

(The illustration also demonstrates the kinds of additions we can make to Petri nets in order to verify their properties with simulation. In this case, the extra material has the purpose of verifying that the two constructs are behaviorally equivalent.)

Both construction are more complex than the one from the first diagram; but when we count the number of elements added, it turns out that they only increase linearly with the number of input arcs of the original transition.

So counted Petri nets are translatable to standard Petri nets in linear space, provided you're willing to accept extra ("silent") steps in the result.

Caveat emptor

I should really prove or disprove these statements, but I won't. The point was to sketch how the idea that counted nets aren't really (much) more expressive than standard Petri nets can be given mathematical rigor, not to actually do it.

Reinier "had my share" Post