Verification

Because Petri nets are a mathematical formalism with decades of theory behind them, they admit a level of formal analysis that ad-hoc workflow diagrams and flowcharts simply don't. They are an object whose state space, reachable markings, and structural invariants can be reasoned about — and, in many cases, decided — by automated tools.

This page sketches what that means in practice for users of Petrinaut.

What can be verified

For classical (untyped) Petri nets, a well-developed body of techniques can decide or approximate a number of properties of interest:

• Reachability: given a starting marking, is some target marking reachable? Useful for asking "can the system ever end up in this bad state?" or "is the goal state reachable at all?"
• Boundedness: do token counts in any place grow without bound as the net runs? Unboundedness usually signals a missing back-pressure mechanism, an unbounded queue, or a runaway feedback loop.
• Deadlock-freedom: is there always at least one enabled transition? A deadlocked net is one where progress has halted because no transition's input conditions are met.
• Liveness: can every transition eventually fire from any reachable marking? Dead transitions are typically modeling mistakes — they represent steps the system can never actually take.
• Place and transition invariants: linear-algebraic conservation laws over markings (place invariants) or firing counts (transition invariants). These capture properties like "the total number of tokens of resource X is conserved" or "every job that starts must eventually finish."

In Petrinaut's setting, these analyses are most directly applicable to the structural skeleton of a net — the places, transitions, arcs, arc weights, and inhibitor arcs — independent of any user-authored code on top.

When symbolic analysis runs out of road

Adding SDCPN's expressive features — colored tokens with numeric attributes, continuous dynamics, stochastic firing rates — buys you modeling power, but often takes you out of the regime where symbolic verification is tractable. An infinite or unbounded attribute space, or a transition that fires according to a probability distribution rather than a guard, can defeat the state-enumeration techniques that decide reachability on classical nets.

The trade-off between expressiveness and decidability here is the subject of active research, including in ARIA's Safeguarded AI programme.

Monte Carlo simulation

Today, Petrinaut leans on Monte Carlo simulation: run the net many times under the same configuration, with different random seeds, and aggregate the results into statistical distributions over quantities of interest.

The headless createMonteCarloSimulator and createMonteCarloExperiment APIs in petrinaut-core run many independent simulations with bounded per-run memory, and aggregate user-defined metrics across them. This won't give you "the probability of deadlock is exactly 0.04" — but it will give you tight empirical confidence intervals on questions like "how often does this supply chain breach its target stockout rate?" or "what's the 95th-percentile time to recover from a disruption?"

See the Simulation page for details on running these experiments and authoring the metrics they aggregate.

A symbolic substrate for AI

Petri nets are interesting not just as a modeling tool in their own right, but as a natural fit for the "symbolic" half of neuro-symbolic AI. They are explicit, inspectable structures: an LLM can propose a Petri net, and a formal toolchain can then check it — for reachability, for safety properties, for invariants — before any of it actually runs.

That separation matters when AI systems are doing real work in safety-critical domains. The neural component is allowed to be creative and fluent; the symbolic component decides whether the result is something we're willing to execute. Petri nets give you a target formalism rich enough to capture real processes, yet structured enough to admit machine-checkable guarantees: the gap neuro-symbolic approaches aim to close.