Hack 1976: Formal P/T-Net Semantics and Complete Coverability Trees

Michel Henri Théodore Hack submitted this MIT dissertation in December 1975; MIT issued it as technical report MIT-LCS-TR-161 in June 1976. The official scan contains 196 physical pages: 194 pages of the work and two scan-control pages. It has no text layer, so all pages were rendered, OCRed as reading aids, read sequentially, and visually inspected. The archived PDF is byte-identical to the official object.

Formal model #

Definition 2.1 on printed page 29 gives finite disjoint sets of places and transitions, nonnegative integer input/output multiplicities, and an initial marking. Hack calls this weighted model a “Generalized Petri Net” and reserves “Ordinary Petri Net” for unit nonzero arc weights. In current notation, his consuming function $F$ maps to Pre, while his producing function $B$ maps to Post.

Definition 2.2 on page 31 states the componentwise enabling condition and the atomic update

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

Definitions 2.3–2.4 on pages 31–33 build interleaving firing sequences and the exact reachability set. Definitions 2.6–2.8 on page 35 separate exact reachability, domination-based coverability, and boundedness. Definitions 2.11–2.12 on pages 36–38 give strong liveness and persistence, including the subtle interpretation of self-loops when tokens are removed before being returned.

Complete coverability-tree result #

Hack warns on page 55 that a simple historical account of Karp–Miller acceleration misses sequences with a large enabling hurdle and small net change. His own Definition 3.2 and subsequent results construct a complete tree: Lemma 3.6 on page 67 proves it finite and effectively constructible; Theorem 3.2 on pages 69–70 characterizes coverability by domination from a tree label; Theorem 3.3 on page 70 identifies unbounded coordinates through $\omega$ and gives the exact finite maximum when a place is bounded; Theorem 3.4 on page 71 makes coverability and place boundedness decidable.

The symbolic $\omega$ is therefore an unboundedness summary, not a reachable token count. Hack's full construction also should not be collapsed into an informal one-pass ancestor rule or attributed verbatim to the unread 1969 Karp–Miller body.

Boundaries #

The report uses interleaving sequences and does not formally define multiset steps, transition independence, effective conflict, confusion, or free-choice structure. It also does not define the signed incidence matrix, Parikh-vector state equation, P-invariants, or T-invariants. Those parts of a modern chapter need a separate source or an explicit derivation from the firing equation.

The report repeatedly describes general reachability decidability as open. That is correct historical context for 1975–1976 and obsolete as current status after Mayr's later result. The report remains primary authority for its formal definitions and its own complete-tree theorems, not for present-day research status or standards terminology.