Petri Nets

Introduction

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.

Try It

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.

<!-- Petri net demo: canvas-rendered net with clickable transitions -->
<div class="layout">
  <canvas id="net" width="420" height="280"></canvas>
  <div class="panel">
    <div class="goal-box">
      <div class="goal-label">Goal marking</div>
      <canvas id="goal" width="120" height="120"></canvas>
    </div>
    <div id="status" class="status">Click an enabled transition (green) to fire it.</div>
    <div class="btn-row">
      <button id="reset">Reset</button>
    </div>
    <div class="legend">
      <span class="leg-en">Enabled transition</span>
      <span class="leg-dis">Disabled transition</span>
    </div>
  </div>
</div>

/* Layout and styling for the Petri net canvas demo */
* { 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; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Petri net model: 4 places (P0-P3), 3 transitions (T0-T2)
// Goal: move all tokens to P3 by firing transitions in the right order
//
// Place coordinates on the 420x280 canvas
//   P0: (55,  60)  P1: (200,  60)
//   P2: (55, 200)  P3: (340, 130)
//
// Transition definitions with their input/output places
//   T0: P0,P2 -> P1   (merge two tokens into one)
//   T1: P1   -> P2,P3 (split one token into two)
//   T2: P1,P3 -> P3   (consume P1, loop P3)  ... wait, redesign:
//
// Net topology (firing rule: consume 1 token per input, produce 1 per output)
//   T0: [P0]      -> [P1]       (move token from P0 to P1)
//   T1: [P1]      -> [P2, P1b]  (split: P1 to P2 and internal)
//   T2: [P2, P1b] -> [P3]       (join: both inputs to P3)

const PLACES = [
  { id: 'P0', x: 70,  y: 70,  label: 'P₀' },
  { id: 'P1', x: 200, y: 70,  label: 'P₁' },
  { id: 'P2', x: 130, y: 195, label: 'P₂' },
  { id: 'P3', x: 340, y: 130, label: 'P₃' }
];

// Each transition: position + input/output place IDs
const TRANSITIONS = [
  { id: 'T0', x: 135, y: 70,  inputs: ['P0'], outputs: ['P1'] },
  { id: 'T1', x: 270, y: 70,  inputs: ['P1'], outputs: ['P2', 'P3'] },
  { id: 'T2', x: 200, y: 195, inputs: ['P2', 'P3'], outputs: ['P3'] }
];

// Initial marking: 1 token in P0, none elsewhere
const INIT = { P0: 1, P1: 0, P2: 0, P3: 0 };
// Goal marking: 1 token in P3, all others empty
const GOAL = { P0: 0, P1: 0, P2: 0, P3: 1 };

let marking = Object.assign({}, INIT);
let fired = 0;
let won = false;

// A transition is enabled when every input place has >= 1 token
function enabled(t) {
  return t.inputs.every(p => (marking[p] || 0) >= 1);
}

// Fire: consume 1 token from each input, produce 1 for each output
function fire(t) {
  if (!enabled(t)) return;
  t.inputs.forEach(p => { marking[p]--; });
  t.outputs.forEach(p => { marking[p] = (marking[p] || 0) + 1; });
  fired++;
}

// Check whether the current marking matches the goal
function atGoal() {
  return Object.keys(GOAL).every(p => (marking[p] || 0) === GOAL[p]);
}

// Drawing helpers for the canvas-rendered Petri net
const R = 20; // visual radius of place circles
const TH = 14, TW = 22; // half-height and half-width of transition rectangles

function drawToken(ctx, cx, cy, n) {
  if (n === 0) return;
  if (n === 1) {
    ctx.beginPath(); ctx.arc(cx, cy, 5, 0, 2 * Math.PI);
    ctx.fillStyle = '#1d3557'; ctx.fill();
  } else if (n === 2) {
    [-6, 6].forEach(dx => {
      ctx.beginPath(); ctx.arc(cx + dx, cy, 4, 0, 2 * Math.PI);
      ctx.fillStyle = '#1d3557'; ctx.fill();
    });
  } else {
    ctx.fillStyle = '#1d3557'; ctx.font = 'bold 12px system-ui';
    ctx.textAlign = 'center'; ctx.textBaseline = 'middle';
    ctx.fillText(String(n), cx, cy);
  }
}

function arrowTo(ctx, x1, y1, x2, y2, col) {
  const dx = x2 - x1, dy = y2 - y1, len = Math.hypot(dx, dy);
  const ux = dx / len, uy = dy / len;
  const hx = x2 - ux * 8, hy = y2 - uy * 8;
  ctx.beginPath(); ctx.moveTo(x1, y1); ctx.lineTo(hx, hy);
  ctx.strokeStyle = col; ctx.lineWidth = 1.4; ctx.stroke();
  const ax = -uy * 5, ay = ux * 5;
  ctx.beginPath(); ctx.moveTo(hx + ax, hy + ay);
  ctx.lineTo(x2, y2); ctx.lineTo(hx - ax, hy - ay);
  ctx.fillStyle = col; ctx.fill();
}

function edgePoints(p, t) {
  // Compute arrow endpoints on the boundary of place and transition
  const dx = t.x - p.x, dy = t.y - p.y, len = Math.hypot(dx, dy);
  const px = p.x + (dx / len) * R, py = p.y + (dy / len) * R;
  const tx = t.x - (dx / len) * TW / 2, ty = t.y - (dy / len) * TH / 2;
  return { px, py, tx, ty };
}

function drawNet(ctx, places, transitions, m, highlight) {
  ctx.clearRect(0, 0, ctx.canvas.width, ctx.canvas.height);
  // Draw arrows between places and transitions
  transitions.forEach(t => {
    const col = '#8899aa';
    t.inputs.forEach(pid => {
      const p = places.find(pl => pl.id === pid);
      const { px, py, tx, ty } = edgePoints(p, t);
      arrowTo(ctx, px, py, tx, ty, col);
    });
    t.outputs.forEach(pid => {
      const p = places.find(pl => pl.id === pid);
      const { px, py, tx, ty } = edgePoints(p, t);
      arrowTo(ctx, tx, ty, px, py, col);
    });
  });
  // Draw places (circles) with token counts
  places.forEach(p => {
    ctx.beginPath(); ctx.arc(p.x, p.y, R, 0, 2 * Math.PI);
    ctx.fillStyle = '#fff'; ctx.fill();
    ctx.strokeStyle = '#2c3e50'; ctx.lineWidth = 1.8; ctx.stroke();
    ctx.fillStyle = '#2c3e50'; ctx.font = '13px system-ui';
    ctx.textAlign = 'center'; ctx.textBaseline = 'top';
    ctx.fillText(p.label, p.x, p.y + R + 3);
    drawToken(ctx, p.x, p.y, m[p.id] || 0);
  });
  // Draw transitions (rectangles), green when enabled
  transitions.forEach((t, i) => {
    const en = enabled(t);
    const isHi = highlight === i;
    ctx.beginPath();
    ctx.rect(t.x - TW, t.y - TH, TW * 2, TH * 2);
    ctx.fillStyle = isHi ? '#27ae60' : (en ? '#2ecc71' : '#bdc3c7');
    ctx.fill();
    ctx.strokeStyle = '#2c3e50'; ctx.lineWidth = 1.4; ctx.stroke();
    ctx.fillStyle = '#fff'; ctx.font = 'bold 11px system-ui';
    ctx.textAlign = 'center'; ctx.textBaseline = 'middle';
    ctx.fillText(t.id, t.x, t.y);
  });
}

// Draw the small goal marking in the side panel
function drawGoal() {
  const gc = document.getElementById('goal');
  const gx = gc.getContext('2d');
  const GPLACES = [
    { id: 'P0', x: 20, y: 25, label: 'P₀' },
    { id: 'P1', x: 60, y: 25, label: 'P₁' },
    { id: 'P2', x: 20, y: 90, label: 'P₂' },
    { id: 'P3', x: 100, y: 60, label: 'P₃' }
  ];
  const R2 = 12;
  gx.clearRect(0, 0, 120, 120);
  GPLACES.forEach(p => {
    gx.beginPath(); gx.arc(p.x, p.y, R2, 0, 2 * Math.PI);
    gx.fillStyle = '#fff'; gx.fill();
    gx.strokeStyle = '#2c3e50'; gx.lineWidth = 1.4; gx.stroke();
    gx.fillStyle = '#2c3e50'; gx.font = '10px system-ui';
    gx.textAlign = 'center'; gx.textBaseline = 'top';
    gx.fillText(p.label, p.x, p.y + R2 + 2);
    const n = GOAL[p.id] || 0;
    if (n > 0) {
      gx.beginPath(); gx.arc(p.x, p.y, 4, 0, 2 * Math.PI);
      gx.fillStyle = '#e74c3c'; gx.fill();
    }
  });
}

const canvas = document.getElementById('net');
const ctx = canvas.getContext('2d');
let hoverTrans = -1;

function getTransAt(x, y) {
  for (let i = 0; i < TRANSITIONS.length; i++) {
    const t = TRANSITIONS[i];
    if (x >= t.x - TW - 4 && x <= t.x + TW + 4 && y >= t.y - TH - 4 && y <= t.y + TH + 4)
      return i;
  }
  return -1;
}

function updateStatus() {
  const el = document.getElementById('status');
  if (won) {
    el.textContent = i18nFmt('Goal reached in %n% firings!', { n: fired });
    el.className = 'status ok';
  } else {
    const anyEnabled = TRANSITIONS.some(enabled);
    if (!anyEnabled) {
      el.textContent = 'Deadlock — no enabled transitions. Press Reset.';
      el.className = 'status bad';
    } else {
      el.textContent = i18nFmt('Transitions fired: %n%. Keep going!', { n: fired });
      el.className = 'status';
    }
  }
}

canvas.addEventListener('click', e => {
  if (won) return;
  const rect = canvas.getBoundingClientRect();
  const sx = canvas.width / rect.width;
  const sy = canvas.height / rect.height;
  const x = (e.clientX - rect.left) * sx;
  const y = (e.clientY - rect.top) * sy;
  const ti = getTransAt(x, y);
  if (ti >= 0 && enabled(TRANSITIONS[ti])) {
    fire(TRANSITIONS[ti]);
    if (atGoal()) { won = true; }
    updateStatus();
    drawNet(ctx, PLACES, TRANSITIONS, marking, -1);
  }
});

canvas.addEventListener('mousemove', e => {
  const rect = canvas.getBoundingClientRect();
  const sx = canvas.width / rect.width;
  const sy = canvas.height / rect.height;
  const x = (e.clientX - rect.left) * sx;
  const y = (e.clientY - rect.top) * sy;
  const ti = getTransAt(x, y);
  if (ti !== hoverTrans) {
    hoverTrans = ti;
    drawNet(ctx, PLACES, TRANSITIONS, marking, ti >= 0 && enabled(TRANSITIONS[ti]) ? ti : -1);
  }
});

document.getElementById('reset').addEventListener('click', () => {
  marking = Object.assign({}, INIT);
  fired = 0;
  won = false;
  hoverTrans = -1;
  updateStatus();
  drawNet(ctx, PLACES, TRANSITIONS, marking, -1);
});

drawGoal();
drawNet(ctx, PLACES, TRANSITIONS, marking, -1);
updateStatus();

<!-- Petri net demo: canvas-rendered net with clickable transitions -->
<div class="layout">
  <canvas id="net" width="420" height="280"></canvas>
  <div class="panel">
    <div class="goal-box">
      <div class="goal-label">Goal marking</div>
      <canvas id="goal" width="120" height="120"></canvas>
    </div>
    <div id="status" class="status">Click an enabled transition (green) to fire it.</div>
    <div class="btn-row">
      <button id="reset">Reset</button>
    </div>
    <div class="legend">
      <span class="leg-en">Enabled transition</span>
      <span class="leg-dis">Disabled transition</span>
    </div>
  </div>
</div>

/* Layout and styling for the Petri net canvas demo */
* { 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; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Petri net model: 4 places (P0-P3), 3 transitions (T0-T2)
// Goal: move all tokens to P3 by firing transitions in the right order
//
// Place coordinates on the 420x280 canvas
//   P0: (55,  60)  P1: (200,  60)
//   P2: (55, 200)  P3: (340, 130)
//
// Transition definitions with their input/output places
//   T0: P0,P2 -> P1   (merge two tokens into one)
//   T1: P1   -> P2,P3 (split one token into two)
//   T2: P1,P3 -> P3   (consume P1, loop P3)  ... wait, redesign:
//
// Net topology (firing rule: consume 1 token per input, produce 1 per output)
//   T0: [P0]      -> [P1]       (move token from P0 to P1)
//   T1: [P1]      -> [P2, P1b]  (split: P1 to P2 and internal)
//   T2: [P2, P1b] -> [P3]       (join: both inputs to P3)

const PLACES = [
  { id: 'P0', x: 70,  y: 70,  label: 'P₀' },
  { id: 'P1', x: 200, y: 70,  label: 'P₁' },
  { id: 'P2', x: 130, y: 195, label: 'P₂' },
  { id: 'P3', x: 340, y: 130, label: 'P₃' }
];

// Each transition: position + input/output place IDs
const TRANSITIONS = [
  { id: 'T0', x: 135, y: 70,  inputs: ['P0'], outputs: ['P1'] },
  { id: 'T1', x: 270, y: 70,  inputs: ['P1'], outputs: ['P2', 'P3'] },
  { id: 'T2', x: 200, y: 195, inputs: ['P2', 'P3'], outputs: ['P3'] }
];

// Initial marking: 1 token in P0, none elsewhere
const INIT = { P0: 1, P1: 0, P2: 0, P3: 0 };
// Goal marking: 1 token in P3, all others empty
const GOAL = { P0: 0, P1: 0, P2: 0, P3: 1 };

let marking = Object.assign({}, INIT);
let fired = 0;
let won = false;

// A transition is enabled when every input place has >= 1 token
function enabled(t) {
  return t.inputs.every(p => (marking[p] || 0) >= 1);
}

// Fire: consume 1 token from each input, produce 1 for each output
function fire(t) {
  if (!enabled(t)) return;
  t.inputs.forEach(p => { marking[p]--; });
  t.outputs.forEach(p => { marking[p] = (marking[p] || 0) + 1; });
  fired++;
}

// Check whether the current marking matches the goal
function atGoal() {
  return Object.keys(GOAL).every(p => (marking[p] || 0) === GOAL[p]);
}

// Drawing helpers for the canvas-rendered Petri net
const R = 20; // visual radius of place circles
const TH = 14, TW = 22; // half-height and half-width of transition rectangles

function drawToken(ctx, cx, cy, n) {
  if (n === 0) return;
  if (n === 1) {
    ctx.beginPath(); ctx.arc(cx, cy, 5, 0, 2 * Math.PI);
    ctx.fillStyle = '#1d3557'; ctx.fill();
  } else if (n === 2) {
    [-6, 6].forEach(dx => {
      ctx.beginPath(); ctx.arc(cx + dx, cy, 4, 0, 2 * Math.PI);
      ctx.fillStyle = '#1d3557'; ctx.fill();
    });
  } else {
    ctx.fillStyle = '#1d3557'; ctx.font = 'bold 12px system-ui';
    ctx.textAlign = 'center'; ctx.textBaseline = 'middle';
    ctx.fillText(String(n), cx, cy);
  }
}

function arrowTo(ctx, x1, y1, x2, y2, col) {
  const dx = x2 - x1, dy = y2 - y1, len = Math.hypot(dx, dy);
  const ux = dx / len, uy = dy / len;
  const hx = x2 - ux * 8, hy = y2 - uy * 8;
  ctx.beginPath(); ctx.moveTo(x1, y1); ctx.lineTo(hx, hy);
  ctx.strokeStyle = col; ctx.lineWidth = 1.4; ctx.stroke();
  const ax = -uy * 5, ay = ux * 5;
  ctx.beginPath(); ctx.moveTo(hx + ax, hy + ay);
  ctx.lineTo(x2, y2); ctx.lineTo(hx - ax, hy - ay);
  ctx.fillStyle = col; ctx.fill();
}

function edgePoints(p, t) {
  // Compute arrow endpoints on the boundary of place and transition
  const dx = t.x - p.x, dy = t.y - p.y, len = Math.hypot(dx, dy);
  const px = p.x + (dx / len) * R, py = p.y + (dy / len) * R;
  const tx = t.x - (dx / len) * TW / 2, ty = t.y - (dy / len) * TH / 2;
  return { px, py, tx, ty };
}

function drawNet(ctx, places, transitions, m, highlight) {
  ctx.clearRect(0, 0, ctx.canvas.width, ctx.canvas.height);
  // Draw arrows between places and transitions
  transitions.forEach(t => {
    const col = '#8899aa';
    t.inputs.forEach(pid => {
      const p = places.find(pl => pl.id === pid);
      const { px, py, tx, ty } = edgePoints(p, t);
      arrowTo(ctx, px, py, tx, ty, col);
    });
    t.outputs.forEach(pid => {
      const p = places.find(pl => pl.id === pid);
      const { px, py, tx, ty } = edgePoints(p, t);
      arrowTo(ctx, tx, ty, px, py, col);
    });
  });
  // Draw places (circles) with token counts
  places.forEach(p => {
    ctx.beginPath(); ctx.arc(p.x, p.y, R, 0, 2 * Math.PI);
    ctx.fillStyle = '#fff'; ctx.fill();
    ctx.strokeStyle = '#2c3e50'; ctx.lineWidth = 1.8; ctx.stroke();
    ctx.fillStyle = '#2c3e50'; ctx.font = '13px system-ui';
    ctx.textAlign = 'center'; ctx.textBaseline = 'top';
    ctx.fillText(p.label, p.x, p.y + R + 3);
    drawToken(ctx, p.x, p.y, m[p.id] || 0);
  });
  // Draw transitions (rectangles), green when enabled
  transitions.forEach((t, i) => {
    const en = enabled(t);
    const isHi = highlight === i;
    ctx.beginPath();
    ctx.rect(t.x - TW, t.y - TH, TW * 2, TH * 2);
    ctx.fillStyle = isHi ? '#27ae60' : (en ? '#2ecc71' : '#bdc3c7');
    ctx.fill();
    ctx.strokeStyle = '#2c3e50'; ctx.lineWidth = 1.4; ctx.stroke();
    ctx.fillStyle = '#fff'; ctx.font = 'bold 11px system-ui';
    ctx.textAlign = 'center'; ctx.textBaseline = 'middle';
    ctx.fillText(t.id, t.x, t.y);
  });
}

// Draw the small goal marking in the side panel
function drawGoal() {
  const gc = document.getElementById('goal');
  const gx = gc.getContext('2d');
  const GPLACES = [
    { id: 'P0', x: 20, y: 25, label: 'P₀' },
    { id: 'P1', x: 60, y: 25, label: 'P₁' },
    { id: 'P2', x: 20, y: 90, label: 'P₂' },
    { id: 'P3', x: 100, y: 60, label: 'P₃' }
  ];
  const R2 = 12;
  gx.clearRect(0, 0, 120, 120);
  GPLACES.forEach(p => {
    gx.beginPath(); gx.arc(p.x, p.y, R2, 0, 2 * Math.PI);
    gx.fillStyle = '#fff'; gx.fill();
    gx.strokeStyle = '#2c3e50'; gx.lineWidth = 1.4; gx.stroke();
    gx.fillStyle = '#2c3e50'; gx.font = '10px system-ui';
    gx.textAlign = 'center'; gx.textBaseline = 'top';
    gx.fillText(p.label, p.x, p.y + R2 + 2);
    const n = GOAL[p.id] || 0;
    if (n > 0) {
      gx.beginPath(); gx.arc(p.x, p.y, 4, 0, 2 * Math.PI);
      gx.fillStyle = '#e74c3c'; gx.fill();
    }
  });
}

const canvas = document.getElementById('net');
const ctx = canvas.getContext('2d');
let hoverTrans = -1;

function getTransAt(x, y) {
  for (let i = 0; i < TRANSITIONS.length; i++) {
    const t = TRANSITIONS[i];
    if (x >= t.x - TW - 4 && x <= t.x + TW + 4 && y >= t.y - TH - 4 && y <= t.y + TH + 4)
      return i;
  }
  return -1;
}

function updateStatus() {
  const el = document.getElementById('status');
  if (won) {
    el.textContent = i18nFmt('Goal reached in %n% firings!', { n: fired });
    el.className = 'status ok';
  } else {
    const anyEnabled = TRANSITIONS.some(enabled);
    if (!anyEnabled) {
      el.textContent = 'Deadlock — no enabled transitions. Press Reset.';
      el.className = 'status bad';
    } else {
      el.textContent = i18nFmt('Transitions fired: %n%. Keep going!', { n: fired });
      el.className = 'status';
    }
  }
}

canvas.addEventListener('click', e => {
  if (won) return;
  const rect = canvas.getBoundingClientRect();
  const sx = canvas.width / rect.width;
  const sy = canvas.height / rect.height;
  const x = (e.clientX - rect.left) * sx;
  const y = (e.clientY - rect.top) * sy;
  const ti = getTransAt(x, y);
  if (ti >= 0 && enabled(TRANSITIONS[ti])) {
    fire(TRANSITIONS[ti]);
    if (atGoal()) { won = true; }
    updateStatus();
    drawNet(ctx, PLACES, TRANSITIONS, marking, -1);
  }
});

canvas.addEventListener('mousemove', e => {
  const rect = canvas.getBoundingClientRect();
  const sx = canvas.width / rect.width;
  const sy = canvas.height / rect.height;
  const x = (e.clientX - rect.left) * sx;
  const y = (e.clientY - rect.top) * sy;
  const ti = getTransAt(x, y);
  if (ti !== hoverTrans) {
    hoverTrans = ti;
    drawNet(ctx, PLACES, TRANSITIONS, marking, ti >= 0 && enabled(TRANSITIONS[ti]) ? ti : -1);
  }
});

document.getElementById('reset').addEventListener('click', () => {
  marking = Object.assign({}, INIT);
  fired = 0;
  won = false;
  hoverTrans = -1;
  updateStatus();
  drawNet(ctx, PLACES, TRANSITIONS, marking, -1);
});

drawGoal();
drawNet(ctx, PLACES, TRANSITIONS, marking, -1);
updateStatus();

Result

Console

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.

The Real Complexity

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.

Where It Matters

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.

Conclusion

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.

Comments

Loading comments...

https://www.kipuhub.com/en/article/petri-nets/Content licensed under CC BY-NC 4.0.

Cookies & privacy

Tokens, places, and the surprising hardness of reachability