Petri Nets

In 1962, a German mathematician named Carl Adam Petri invented a formalism to describe processes where many things happen at the same time. His idea was elegantly simple: draw circles (called places) to represent conditions or resources, draw rectangles (called transitions) to represent events or actions, connect them with arrows, and drop small black dots called tokens into the places.

A token sitting in a place means that condition is currently true. A transition fires whenever every input place has at least one token — it consumes a token from each input and deposits a token into each output. Watch a handful of transitions fire in sequence and you have just simulated a concurrent program, a manufacturing pipeline, a network protocol, or a biological pathway.

The appeal is twofold: Petri nets are visual (you can draw them on a whiteboard and reason about them at a glance) and mathematical (every firing step is a precise algebraic operation on a vector of token counts). That combination made them the dominant tool for reasoning about concurrent systems for decades.

The central question is reachability: given an initial distribution of tokens (the initial marking), can the net ever reach a specific target marking? Answering it turns out to be surprisingly hard — and the story of how hard is one of the great sagas of theoretical computer science.

Below is a small Petri net with four places (circles) and three transitions (rectangles). Tokens appear as filled dots inside the places. A transition lights up when all its input places have at least one token — click it to fire.

<!-- {{c_html_intro}} -->
<div class="layout">
  <canvas id="net" width="420" height="280"></canvas>
  <div class="panel">
    <div class="goal-box">
      <div class="goal-label">{{goal_label}}</div>
      <canvas id="goal" width="120" height="120"></canvas>
    </div>
    <div id="status" class="status">{{status_initial}}</div>
    <div class="btn-row">
      <button id="reset">{{btn_reset}}</button>
    </div>
    <div class="legend">
      <span class="leg-en">{{legend_enabled}}</span>
      <span class="leg-dis">{{legend_disabled}}</span>
    </div>
  </div>
</div>

/* {{c_css_intro}} */
* { box-sizing: border-box; margin: 0; padding: 0; }
body { font-family: system-ui, sans-serif; background: #f7f9fb; color: #222; }
.layout { display: flex; gap: 12px; align-items: flex-start; flex-wrap: wrap; padding: 8px; }
canvas#net { border: 1px solid #d0d8e4; border-radius: 10px; background: #fff;
             cursor: pointer; touch-action: none; }
.panel { display: flex; flex-direction: column; gap: 10px; min-width: 140px; }
.goal-box { border: 1px solid #c8d5e3; border-radius: 8px; padding: 6px 8px; background: #fff; }
.goal-label { font-size: .78rem; font-weight: 600; color: #5a7088; margin-bottom: 4px; }
canvas#goal { border-radius: 6px; }
.status { font-size: .9rem; font-weight: 600; min-height: 1.5em; color: #333; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c0392b; }
.btn-row { display: flex; gap: 6px; }
button { font: 600 13px system-ui; padding: .38rem .8rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 7px; cursor: pointer; }
.legend { font-size: .74rem; color: #666; display: flex; flex-direction: column; gap: 3px; }
.leg-en::before { content: "■ "; color: #2ecc71; }
.leg-dis::before { content: "■ "; color: #aaa; }

// Code not found

Notice that firing a transition is irreversible: once tokens move, earlier states may become unreachable. Try to reach the goal marking shown in the panel — all tokens in place $P_4$. If you get stuck, press Reset and try a different order. The fact that you must search over possible firing sequences is exactly the reachability problem.

How hard is it to decide whether a Petri net can reach a given marking?

• Easy to check a path: if someone hands you a firing sequence, you can verify it leads to the target in linear time — just simulate each step.
• Hard to find one: the space of reachable markings can be enormous. Even with a small net, the reachable states can number in the billions before you hit the target — or discover it is impossible.
• Decidable, but barely. For decades, reachability was one of the great open problems. Ernst Mayr proved it decidable in 1981, and S. Rao Kosaraju gave a cleaner proof in 1982. The algorithm's complexity, however, is non-elementary — it cannot be bounded by any fixed tower of exponentials $2^{2^{2^{\cdots}}}$.
• EXPSPACE-hard. Later work by Lipton (1976) showed the problem is at least EXPSPACE-hard — harder than NP, harder than PSPACE. The exact complexity class was only settled in 2021 when Czerwinski and Orlikowski proved reachability is Ackermann-complete, placing it among the hardest decidable problems known.

This means: unlike the halting problem, which is flat-out undecidable, Petri net reachability can always be answered — but the algorithm may need space and time that towers beyond any fixed exponential. For large industrial nets, heuristic tools and clever abstractions are the only practical recourse.

Any system where multiple things happen simultaneously — and where those things can interact or compete — is a candidate for a Petri net model:

• Hardware and protocol verification: CPU pipelines, cache coherence protocols, and communication protocols are modeled as Petri nets so that deadlocks and race conditions can be detected before silicon is cut.
• Business process management: workflow engines (including the BPMN standard) translate business processes into Petri-net-like graphs to check that a process can always complete and never get stuck.
• Biological networks: metabolic pathways and gene regulatory networks are naturally token-passing systems; Petri nets let biologists ask whether a cell can transition from a healthy state to a diseased one.
• Distributed computing: message-passing protocols and concurrent data structures can be verified by encoding them as Petri nets and checking safety properties.

Extensions — colored Petri nets (tokens carry data), timed Petri nets (transitions have durations), stochastic Petri nets (firing rates are random) — widen the reach while preserving the core token-flow intuition. Tools like model checking algorithms then search the state space for violations.

Petri nets are deceptively simple: a handful of circles, rectangles, arrows, and dots. Yet from that simplicity emerges a model powerful enough to capture any concurrent process — and a reachability question hard enough to resist complete classification for 60 years.

The 2021 result of Czerwinski and Orlikowski placed reachability in the Ackermann complexity class — decidable, but requiring time and space that towers beyond any fixed exponential. It is a reminder that even problems we can in principle solve may be practically intractable for large instances.

Next time you debug a race condition or wonder whether a workflow can ever deadlock, you are asking a Petri net reachability question in disguise. The tools that answer it stand on one of the longest-running proof marathons in the history of theoretical computer science.