Petri Nets: Properties, Analysis and Applications
A complete source map of Tadao Murata's 1989 survey of classical weighted place/transition nets, covering firing semantics, concurrency and conflict, reachability and coverability, behavioral properties, structural subclasses, invariants, and extension boundaries.
Murata's invited survey is a broad, carefully connected account of classical place/transition nets. Its strongest contribution to GTK is the map between operational semantics, behavior-dependent properties, algebraic necessary conditions, structural subclasses, and model extensions. It is an authoritative peer-reviewed survey, not a primary specification or a current complexity survey, so its definitions and theorem scopes are retained with explicit boundaries.
The archived object is a 40-page scan of Proceedings of the IEEE 77(4), printed pages 541–580. It was read and visually inspected in full, including Tables 1–7, Figures 1–59, the bibliography, and the final biography page. The PDF has SHA-256 7f68218a74bcebc6c4d32126b1b4bac0aba713de4be390a5ad9f45568537d7a8; its embedded OCR is useful for navigation but unreliable for formulas, subscripts, inequalities, and small graph labels, which were checked against 144 dpi page renders.
Source map #
| Printed pages | Material | GTK use |
|---|---|---|
| 541–546 | Motivation, typed weighted P/T structure, firing, conflict, concurrency, confusion, applications, inhibitor arcs | Foundation and model-boundary map |
| 547–549 | Reachability, boundedness, safeness, liveness, reversibility, home states, coverability, persistence | Quantified property definitions |
| 550–553 | Omega-accelerated coverability tree, information loss, incidence matrix, state equation, reductions | Analysis mechanisms and their failure boundaries |
| 554–565 | State-machine, marked-graph, free-choice, extended-free-choice, and asymmetric-choice subclasses; siphons, traps, subclass theorems and synthesis | Structural taxonomy; theorem hypotheses must remain local |
| 566–569 | Structural boundedness, conservativeness, repetitiveness, consistency, S/P- and T-invariants | Algebraic certificates and terminology crosswalk |
| 570–573 | Timed, stochastic, generalized stochastic, and high-level/colored extensions | Topic discovery and separation from ordinary P/T semantics |
| 574–580 | References and author biography | Primary-source routing and document completeness |
Claims retained with scope #
- A weighted P/T net has finite disjoint place and transition sets, nonnegative integer markings, and input/output arc weights; enabling checks every input requirement before an atomic firing changes the marking.
- Structural conflict, marking-dependent enabled conflict, causal concurrency, confusion, and persistence are related but distinct notions.
- Reachability is exact, while coverability asks for componentwise domination by a reachable marking.
- The omega-accelerated coverability construction summarizes unbounded growth but loses exact-count and ordering information. Murata explicitly shows that it cannot alone settle general reachability or liveness.
- The cumulative state equation is necessary for reachability in general, not sufficient. A nonnegative solution need not be orderable into an enabled firing sequence.
- Murata's place-side S-invariant is commonly called a P-invariant today. A positive place invariant can yield token bounds; a T-invariant records zero net change but is not automatically executable.
- Siphon and trap consequences follow from their preset/postset inclusions: an emptied siphon stays empty, while a marked trap stays marked.
- Inhibitor, timed, stochastic, and colored nets change the base model. Their expressiveness and analysis results must not be attributed to ordinary P/T nets.
Source claims audit #
| Source framing | Verdict | GTK treatment |
|---|---|---|
| Omega-tree nodes can summarize unbounded components | current with abstraction qualification | Explain omega as a coverability summary, never an exact marking |
| The coverability tree decides general reachability or liveness | explicitly rejected by the source | Preserve the information-loss counterexample and use exact reachability separately |
| The state equation characterizes general reachability | explicitly rejected by the source | Teach it as a necessary filter and show a spurious algebraic solution |
| The 1989 reachability resource bound is current | outdated | Omit it; use current primary research for modern complexity claims |
| Free-choice and other subclass theorems hold for arbitrary nets | false generalization | Keep every ordinary/pure/live/safe/connected hypothesis attached to its theorem |
| Inhibitor-net Turing power belongs to ordinary P/T nets | model-category error | Place zero testing behind an explicit extension boundary |
Visual audit #
Every numbered table and figure was inspected. None is copied into GTK. The scan's small labels and OCR damage make direct reuse weaker than independently authored diagrams, and several advanced figures depend on theorem-specific side conditions. GTK preserves two load-bearing visual roles with original, recomputed SVGs: a weighted before/after firing diagram, and a comparison between an exact bounded reachability graph and lossy omega acceleration.