Petri nets and large finite sets
An upper bound is given for the complexity of the Karp-Miller decision procedure for the Finite Containment Problem for pairs of Petri nets; the procedure is shown to primitive recursive in the Ackermann function. Bounds for the lengths of the searches involved are obtained in terms of large finite sets in the sense of Paris-Harrington and of Ketonen- Solovay.
complexity of the Karp-Miller decision procedure
Finite Containment Problem for pairs of Petri nets
scientific article; zbMATH DE number 3909749