Petri Nets: Concurrency, Reachability & Invariants

A state machine puts the whole system in one control state. A Petri net instead distributes state across places and lets several local events become possible at once. That small change makes resource competition, synchronization, causal independence, and unbounded accumulation explicit rather than forcing them into one exponentially large product state.

This entry fixes one baseline throughout: a weighted place/transition net (P/T net) with nonnegative integer tokens and no capacities, guards, priorities, time, or probability. Extensions are useful, but their extra rules must be named because they change enabling, firing, and sometimes decidability.

The typed P/T-net contract #

The underlying graph is directed and bipartite: arcs go only from a place to a transition or from a transition to a place. The maps are intentionally typed on $P\times T$ in both directions. The argument order identifies a place and a transition; Pre versus Post identifies the arc direction. This avoids the common mistake of declaring a pre-incidence map in the output direction.

Once orders for $P$ and $T$ are fixed, a marking is a vector $M\in\mathbb N^{|P|}$ and Pre and Post are $|P|\times|T|$ matrices. For one transition $t$, write $\mathop{\mathrm{Pre}}_t$ and $\mathop{\mathrm{Post}}_t$ for its columns.

Two restricted terms are worth keeping separate:

• An ordinary net has only unit nonzero arc weights. A weighted P/T net permits any nonnegative integer weights.
• A pure net has no place-transition pair with both $\mathop{\mathrm{Pre}}(p,t)>0$ and $\mathop{\mathrm{Post}}(p,t)>0$. General P/T semantics does not require purity. Such a self-loop can require tokens while returning them, even though its net incidence is zero.

Places are not intrinsically “conditions” and transitions are not intrinsically “random events.” Those are possible interpretations. Formally, a marking is a token-count vector and firing chooses an enabled transition nondeterministically unless an explicitly stochastic extension supplies probabilities or rates.

Enabling and firing are local and atomic #

A transition $t$ is enabled at marking $M$ exactly when every input requirement is available:

$$M\geq\mathop{\mathrm{Pre}}_t \quad\Longleftrightarrow\quad \forall p\in P:\ M(p)\geq\mathop{\mathrm{Pre}}(p,t).$$

If $t$ fires, all its input consumption and output production form one atomic state change:

$$M[t\rangle M' \quad\Longleftrightarrow\quad M\geq\mathop{\mathrm{Pre}}_t \land M'=M-\mathop{\mathrm{Pre}}_t+\mathop{\mathrm{Post}}_t.$$

The brackets $M[t\rangle M'$ mean that $t$ is enabled at $M$ and its firing yields $M'$. Enabling must be checked against Pre, not against the net token change. A self-loop may have zero incidence while still requiring a token.

Steps and multisets of transitions #

Formal step semantics treats a finite step as a transition multiset $\nu\in\mathbb N^{|T|}$. It is enabled when the marking can pay for all occurrences together:

$$M\geq \mathop{\mathrm{Pre}}\nu.$$

Its firing yields

$$M'=M-\mathop{\mathrm{Pre}}\nu+\mathop{\mathrm{Post}}\nu.$$

This formulation matters when a step contains two occurrences of one transition or two transitions sharing an input place: individual enabling is not enough; their combined demand must fit.

Concurrency, conflict, and interleaving #

These three ideas describe different facts.

Co-enabled

Distinct transitions $t$ and $u$ are each individually enabled at the same marking $M$.

Step-concurrent at $M$

The two-transition multiset is enabled: $M\geq\mathop{\mathrm{Pre}}_t+\mathop{\mathrm{Pre}}_u$. Both resource demands can be met together.

Pairwise semantic conflict at $M$

$t$ and $u$ are co-enabled, but their two-transition multiset is not enabled. Their individual demands fit separately, while their combined demand does not.

Interleaving

A linear sequence records one firing before another. It is an observation order, not automatically a causal dependency.

Pairwise conflict is only the binary case. More generally, a finite nonempty transition multiset $G$ is in semantic conflict at $M$ when every one-transition restriction $G|_{\{t\}}$ is enabled with its full multiplicity, but $G$ itself is not. This matters: if three transitions each consume one token from the same place and $M(p)=2$, every pair is a valid step while the triple is in conflict. At $M(p)=3$, the same structure is conflict-free for that triple.

Post-firing disabling is a stronger, separate predicate. If two self-looping transitions each consume and immediately replace the only token in $p$, they are in pairwise semantic conflict because the joint step needs two tokens; nevertheless, firing either one restores the token and leaves the other enabled. A conflict definition based only on what remains enabled after one firing would miss this case.

If $t$ and $u$ are step-concurrent in a weighted P/T net, both serializations are possible and meet at the same marking:

$$M[t\rangle M_t[u\rangle M_{tu}, \qquad M[u\rangle M_u[t\rangle M_{ut}, \qquad M_{tu}=M_{ut}.$$

The reason is algebraic. The joint enabling inequality leaves enough input tokens for either transition after the other consumes its share, and vector addition commutes. Interleaving semantics represents the one concurrent step as two paths; it preserves the final marking but forgets that neither event had to cause the other.

Conflict is different. If a place contains one token and both $t$ and $u$ require it without immediately replacing it, each is individually enabled but their joint step is not. In this canonical choice case, firing one also removes the witness that enabled the other.

Confusion: when concurrency changes a choice #

Let $t\mathrel{\mathrm{conf}_M}u$ mean that $t$ and $u$ are in pairwise semantic conflict at reachable marking $M$. A confusion exists at $M$ when distinct transitions $a,b,c$ can be chosen such that $a$ and $b$ are step-concurrent at $M$, but firing one of them changes whether the other is in conflict with $c$. In other words, an event that is causally independent of part of a choice changes that choice's enabled conflict set.

This is a marking-dependent interaction, not merely the presence of one conflict and one concurrent pair somewhere in the same net. It covers the symmetric pattern in which $a$ and $b$ are concurrent while both compete with $c$, and the asymmetric pattern in which the ordering of a concurrent event creates or removes a later conflict. The distinction matters to distributed scheduling: a supposedly local concurrent decision can change which global alternative remains available.

One structural subclass prevents this mixing. For an ordinary unit-weight P/T structure, define

$$p^{\bullet}=\{u\in T\mid\mathop{\mathrm{Pre}}(p,u)>0\}, \qquad {}^{\bullet}t=\{q\in P\mid\mathop{\mathrm{Pre}}(q,t)>0\}.$$

The net is free-choice when every input arc $(p,t)$ satisfies

$$p^{\bullet}=\{t\} \quad\text{or}\quad {}^{\bullet}t=\{p\}.$$

Therefore, if a place offers more than one outgoing choice, every candidate transition has that place as its only input. An unrelated synchronization input cannot selectively enable only some candidates. In an ordinary 1-safe net, this separates choice from synchronization and rules out the classical confusion pattern above.

Free-choice structure alone is not enough for the marking-dependent conflict relation when places may hold several tokens. Let $M(p)=M(r)=1$; let $a$ consume the token in $r$ and produce one in $p$; and let $b$ and $c$ each consume one token from $p$. The structure is free-choice, and $a$ is step-concurrent with $b$. Initially $b\mathrel{\mathrm{conf}_M}c$, but after $a$ fires, $p$ contains two tokens and $b$ and $c$ are jointly enabled, so their pairwise semantic conflict disappears. The firing of an independent event changed the enabled choice without violating the structural free-choice condition. Weighted variants likewise need an explicitly stated generalization: unequal input weights can make candidates enabled under different token counts even when the unweighted support graph looks free-choice.

Worked bounded example: fork, independent completion, join #

Let the place order be

$$(I,L,R,L_d,R_d),$$

where $I$ is an idle job, $L$ and $R$ are active branches, and $L_d$ and $R_d$ are completed branches. The four transitions are:

Start from

$$M_0=(1,0,0,0,0).$$

One exact firing trace is

$$\begin{aligned} (1,0,0,0,0) &[\mathtt{fork}\rangle(0,1,1,0,0)\\ &[\mathtt{finish\_L}\rangle(0,0,1,1,0)\\ &[\mathtt{finish\_R}\rangle(0,0,0,1,1)\\ &[\mathtt{join}\rangle(1,0,0,0,0). \end{aligned}$$

After fork, finish_L and finish_R are step-concurrent. Reversing their order gives the other path through $(0,1,0,0,1)$ and reaches the same pre-join marking $(0,0,0,1,1)$. join is disabled until both completions are present, so synchronization is an enabling constraint rather than a special control primitive.

The reachable set is exactly the five markings drawn in the upper panel. Inspection already suggests that the net is safe, deadlock-free, live, reversible, and persistent. The definitions below make those claims testable rather than visual guesses.

Reachability is exact; coverability is an upper question #

A firing sequence $\sigma=t_1\cdots t_k$ is executable from $M$ when there are markings

$$M=M_0'[t_1\rangle M_1'[t_2\rangle\cdots[t_k\rangle M_k'.$$

Write $M[\sigma\rangle M'$ for the complete path and

$$R(M_0)=\{M\in\mathbb N^{|P|}\mid\exists\sigma:\ M_0[\sigma\rangle M\}$$

for the reachability set. A target $M$ is reachable only when some execution ends at that exact vector.

A target marking $K$ is coverable when

$$\exists M\in R(M_0):\ M\geq K$$

componentwise. Coverability asks whether the net can reach at least the requested token counts, perhaps with additional tokens elsewhere. It compares a reachable marking with the target $K$, not with the initial marking.

Reachability graph #

The reachability graph has one vertex for every marking in $R(M_0)$ and an edge

$$M\xrightarrow{t}M'$$

for every firing $M[t\rangle M'$. It is finite exactly when the marked net is bounded. For the fork/join example, the graph is finite and exact; paths answer reachability, deadlock, reversibility, and liveness questions directly. Its size can still grow exponentially with the number of concurrent components because all distinguishable token distributions remain explicit.

Karp–Miller-style acceleration and the $\omega$ boundary #

An unbounded net can have an infinite reachability graph. For example, one input-free transition that adds one token to place $p$ reaches $0,1,2,3,\ldots$. The core idea of Karp–Miller-style acceleration is to compare a descendant with an ancestor on its branch and replace components that can keep growing by $\omega$.

The symbol obeys $n<\omega$ and $\omega\pm n=\omega$ for finite $n$. It means arbitrarily large finite values are coverable in that component. It is not a token count and not an exact reachable marking.

That sentence is the intuition, not the complete algorithm. A correct finite construction must also specify which symbolic nodes are expanded, how loop ends and repeated labels are handled, and why the expansion terminates. Hack's complete coverability-tree construction supplies those details for weighted P/T nets. Its finite tree decides coverability: a finite target is coverable exactly when it is componentwise dominated by an appropriate symbolic node. It also exposes unbounded components. But acceleration deliberately loses exact-count information such as parity and correlations between places. Therefore:

• a reachability graph is exact but may be infinite;
• a complete $\omega$-accelerated coverability tree is finite and sufficient for coverability and boundedness;
• the $\omega$ abstraction does not decide exact reachability or liveness by itself.

General P/T-net reachability is nevertheless decidable. Mayr's 1981 paper presented an algorithm for the general Petri-net reachability problem, establishing that result by a substantially deeper construction. “The coverability tree cannot answer it” and “the problem is undecidable” are not equivalent claims.

Behavioral properties with quantifiers #

Let $\mathop{\mathrm{En}}(M)=\{t\in T\mid M\geq\mathop{\mathrm{Pre}}_t\}$.

$k$-bounded

For a specified $k\in\mathbb{N}$, the net is $k$-bounded when $\forall M\in R(M_0),\ \forall p\in P:\ M(p)\leq k$. A net is bounded if some finite $k$ satisfies this condition.

Safe

The net is 1-bounded: every reachable place count belongs to $\{0,1\}$. Safety never means token values $\{1,2\}$.

Deadlocked marking

$M$ is deadlocked when $\mathop{\mathrm{En}}(M)=\varnothing$. The net is deadlock-free when every reachable marking enables at least one transition.

Live transition and live net

A transition $t$ is live when, from every $M\in R(M_0)$, some continuation can eventually fire $t$: $\forall M\in R(M_0),\ \exists\sigma,M',M'':\ M[\sigma\rangle M'[t\rangle M''$. The net is live when every transition is live.

Reversible

$\forall M\in R(M_0):\ M_0\in R(M)$. Every reachable marking can return to the initial marking. More generally, a home marking is reachable from every reachable marking.

Persistent

For every reachable $M$ and every pair of distinct enabled transitions $t,u$, firing either does not disable the other: $M[t\rangle M'\Rightarrow u\in\mathop{\mathrm{En}}(M')$, with the universally quantified swapped pair covering the other direction.

Liveness is stronger than deadlock freedom: a system may always have some enabled transition while permanently starving another. Persistence is not the negation of that definition; it is the preservation of an already enabled alternative after another firing.

For the fork/join net, the five-node reachability graph proves all six claims:

• every coordinate is 0 or 1, so it is safe and bounded;
• every node has an outgoing edge, so it is deadlock-free;
• from any node the cycle can progress until every transition fires, so every transition is live;
• every node reaches $M_0$, so it is reversible;
• the only marking with two enabled transitions is the post-fork marking, and either completion leaves the other enabled, so it is persistent.

These are properties of the marked net $(N,M_0)$. Changing only $M_0$ can change every conclusion.

Incidence matrix and the state equation #

Fix place rows and transition columns. Define

$$C=\mathop{\mathrm{Post}}-\mathop{\mathrm{Pre}} \in\mathbb Z^{|P|\times|T|}.$$

For the fork/join net, using row order $(I,L,R,L_d,R_d)$ and column order (fork, finish_L, finish_R, join),

$$C= \begin{bmatrix} -1&0&0&1\\ 1&-1&0&0\\ 1&0&-1&0\\ 0&1&0&-1\\ 0&0&1&-1 \end{bmatrix}.$$

If an executable sequence $\sigma$ fires transition $t$ exactly $x(t)$ times, its Parikh vector is $x=\Psi(\sigma)\in\mathbb N^{|T|}$. Summing each firing equation gives the state equation

$$M=M_0+Cx.$$

This equation is a necessary condition for reachability: every executable sequence supplies a nonnegative integer solution. It is not sufficient because $C$ records only net token change. It forgets the order of firings and whether the intermediate input requirements were ever available.

A spurious state-equation solution #

Take places $(p,q)$ and one transition $t$ with

$$\mathop{\mathrm{Pre}}_t=(1,1)^\mathsf T, \qquad \mathop{\mathrm{Post}}_t=(0,2)^\mathsf T, \qquad C_t=(-1,1)^\mathsf T.$$

From $M_0=(1,0)^\mathsf T$, the equation with $x(t)=1$ yields the nonnegative candidate

$$M_0+C_tx=(0,1)^\mathsf T.$$

Yet $t$ is not enabled initially because $q$ has no token, and there is no other transition. The target satisfies the state equation but is unreachable. Any analysis that solves $M=M_0+Cx$ must still prove that some ordering of the proposed transition multiset is executable.

P-invariants and T-invariants #

The incidence matrix exposes exact linear certificates.

For the fork/join net,

$$y=(2,1,1,1,1)^\mathsf T$$

satisfies $y^\mathsf TC=0$, giving

$$2M(I)+M(L)+M(R)+M(L_d)+M(R_d)=2.$$

The coefficient 2 accounts for the one idle token becoming two branch tokens. Because every coefficient is positive, this invariant supplies a finite upper bound for every place. A nonnegative invariant with zero coefficients may bound only the places in its support; an invariant with negative coefficients is an algebraic conservation law but not directly a token bound.

Here

$$x=(1,1,1,1)^\mathsf T$$

is a T-invariant: one fork, each completion once, and one join have zero total marking change. The exact trace above realizes that multiset and returns to $M_0$.

The equations do not supply their own executions:

• a P-invariant constrains reachable markings but does not characterize the reachability set;
• a T-invariant need not have any enabled ordering from the chosen $M_0$;
• even a realizable T-invariant does not by itself prove that every transition is live, that the net is reversible, or that the cycle is reachable from every reachable marking;
• a basis of linear invariants may miss nonlinear and ordering constraints.

Use invariants to prove impossibility, conservation, or bounds; use behavioral reasoning to prove an execution exists.

Traps and siphons are structural certificates #

For a place set $S\subseteq P$, define

$${}^{\bullet}S=\{t\in T\mid\exists p\in S:\mathop{\mathrm{Post}}(p,t)>0\}, \qquad S^{\bullet}=\{t\in T\mid\exists p\in S:\mathop{\mathrm{Pre}}(p,t)>0\}.$$

Thus ${}^{\bullet}S$ contains transitions that put tokens into $S$, while $S^{\bullet}$ contains transitions that take tokens from $S$.

• A trap satisfies $S^{\bullet}\subseteq{}^{\bullet}S$. Every transition that removes tokens from the set also returns at least one token somewhere in it. Once a trap is marked, it remains marked.
• A siphon satisfies ${}^{\bullet}S\subseteq S^{\bullet}$. Every transition that adds tokens to the set also requires tokens from it. Once a siphon is empty, it remains empty.

These implications follow directly from the arc sets and firing rule, including weighted arcs. They are not complete deadlock tests. A marked trap need not be bounded; an empty siphon need not deadlock the whole net; and whether a trap starts marked or a siphon can become empty is behavioral information tied to $M_0$. Stronger conclusions require a theorem for a stated net subclass.

Structural facts versus marked behavior #

The unmarked structure is $N=(P,T,\mathop{\mathrm{Pre}},\mathop{\mathrm{Post}})$; adding $M_0$ produces a marked net. This division prevents two frequent reasoning errors.

An invariant equation is structural, but its conserved constant $y^\mathsf TM_0$ and the bound inferred from it depend on the initial marking. Conversely, finding no useful linear invariant does not prove that the marked net is unbounded.

Graph reductions have the same boundary. Removing a place, fusing transitions, or collapsing a subnet is valid only under a specific reduction theorem whose structural, weight, marking, and target-property side conditions have been checked. There is no unconditional list of local rewrites that preserves boundedness, liveness, reachability, and reversibility all at once.

Extensions change the contract #

Plain weighted P/T arcs inspect and update token counts only through fixed nonnegative integer Pre and Post weights. The following variants add distinct semantics:

Adding one of these features can change expressiveness, analysis algorithms, and decidability boundaries. Always put the variant in the model's name and restate its enabling and firing rules before reusing a property or theorem.

Diagnostic workflow #

When a net or an analysis result looks wrong, work from semantics outward:

1. Name the exact net class. Record whether weights, capacities, read/inhibitor/reset arcs, priorities, colors, time, or stochastic rules are present.
2. Type the structure. Check $P\cap T=\varnothing$, arc endpoints, nonnegative integer weights, and the direction of Pre and Post.
3. Write the initial marking and place order. Every vector and matrix must use the same declared order.
4. Recompute enabling before firing. Verify $M\geq\mathop{\mathrm{Pre}}_t$ componentwise; then apply the complete atomic equation.
5. Separate choice from concurrency. For co-enabled transitions, test the combined inequality $M\geq\mathop{\mathrm{Pre}}_t+\mathop{\mathrm{Pre}}_u$ and then test whether one firing disables the other.
6. Find a short exact trace. A concrete sequence often exposes a reversed arc, missing token, or illegal extension faster than global analysis.
7. Use algebra as a filter. Compute $C$, check the state equation, and solve for P/T-invariants. Treat a failed necessary condition as a proof of impossibility; do not treat a passed condition as proof of reachability.
8. Choose exact or covering analysis deliberately. Build the reachability graph only when boundedness makes it finite or exploration limits are explicit. Use Karp–Miller-style coverability acceleration for coverability and unboundedness, never as an exact-marking oracle.
9. State the property's quantifiers. “No deadlock found,” “each transition fired once,” and “live from every reachable marking” are three different claims.
10. Validate any reduction against its theorem. List the property being preserved and every side condition before changing the net.

The central discipline is simple: keep the enabling relation, the token-update equation, and the question being asked distinct. Most incorrect Petri-net arguments collapse at least two of those layers.