On the finite containment problem for Petri nets (Q1819937)

The finite containment problem (FCP) for vector addition systems (VAS) is to determine, given two VAS with finite reachability sets \(R_ 1\), \(R_ 2\), whether \(R_ 1\subset R_ 2\). The paper shows that FCP is DTIME(Ackermann)-complete, sharpening previous results due to \textit{K. McAloon} [Theor. Comput. Sci. 32, 173-183 (1984; Zbl 0569.68046)] and to \textit{E. W. Mayr} and \textit{A. R. Meyer} [J. Assoc. Comput. Mach. 28, 561- 576 (1981; Zbl 0462.68020)]. The principal technique is to replace an application of the infinite Ramsey theorem by a certain finite Ramsey theorem yielding an upper bound for the height of the Karp-Miller- covering-tree (coinciding with the reachability tree in the case of finite reachability sets).