PaperlayerView exact revision on arXiv

Source-linked AI summary

The Reachability Problem for Petri Nets is Not Primitive Recursive

Jérôme Leroux

arXiv:2104.12695v4cs.LO

TL;DR

Checking-program reachability, equivalent to Petri-net reachability, has an Ackermannian upper bound but had lacked a matching lower bound. The paper proves an Ackermannian lower bound and establishes F_d-hardness in dimension 2d+4, implying non-elementary complexity in dimension 10.

  • Problem

    Checking-program reachability, equivalent to Petri-net reachability, had an Ackermannian upper bound but no matching lower bound, leaving its exact complexity unresolved.

    Source: §1 · p. 1

  • Method

    The paper develops gadgets that establish lower bounds for checking-program reachability, including in fixed dimensions.

    Source: §1 · p. 2

  • Results

    Reachability is F_d-hard in dimension 2d+4 for d ≥ 3, and therefore is not elementary in dimension 10.

    Source: §9 · p. 18

  • Takeaways & Limitations

    The paper proves checking-program reachability Ackermannian-complete, resolving the long-standing complexity gap.

    Source: §1 · p. 1, §10 · p. 19

    The loop-at-most lemmas assume the test-free program M does not use counters c or c′.

    Source: §6 · p. 9

Abstract

from arXiv · show

We provide an Ackermannian complexity lower bound for the reachability problem for checking programs, a model equivalent to Petri nets. Moreover in fixed dimension $2d+4$, we show that the problem is $\mathbb{F}_d$-hard. As a direct corollary, the reachability problem in dimension 10 is not elementary.

1 Introduction

The paper studies reachability for checking programs, equivalent to Petri-net reachability, whose Ackermannian upper bound had lacked a matching lower bound. It proves an Ackermannian lower bound and an F_d-hardness result in dimension 2d+4, including non-elementary complexity in dimension 10.

1 Introduction

  • Reachability is equivalent to Petri-net reachability, and the paper describes checking programs as a model for analyzing parallel processes.Checking programs use increment, decrement, and end-of-execution test commands.Source: §1 · p. 1
  • The paper proves an Ackermannian lower bound for checking-program reachability, matching the known Ackermannian upper bound and closing a long-standing open problem.Checking-program reachability is equivalent to Petri-net reachability.Source: §1 · pp. 1–2
  • For every d ≥ 3, reachability in dimension 2d+4 is F_d-hard; consequently, dimension 10 is not elementary.The paper notes that this fixed-dimension lower bound is not known to be optimal against the F_d+4 upper bound in dimension d.Source: §1 · p. 2
  • The paper identifies its lower bound as the final piece toward exact complexity and notes that lower bounds for natural extensions remain open.The best known lower bounds for those extensions come from checking programs; finding gadgets that exploit their additional power remains open.Source: §1 · p. 2

2 Fast Growing Functions

This section defines fast-growing functions F_d and a reduction rule evalF_d that computes them by preserving function values while decreasing a lexicographic measure.

Fast-growing functions

  • The functions are built by composing F_1 through F_d according to vector v, with F_0(n)=n+1.The section defines F_d recursively and introduces F_v for vectors v in N^d.Source: §2 · p. 2
  • F_ω is defined as F_{n+1}(n) at input n, behaves like the classical Ackermann function for complexity purposes, and is not primitive recursive.Each finite-level F_d is primitive recursive; F_3 behaves like a tower of n exponentials and is not elementary.Source: §2 · pp. 2–3

Computing F_d

  • evalF_d reduces a nonzero vector by its least positive coordinate, adjusting n according to whether that coordinate is first or later.For p=1 it maps (v,n) to (v−1_{d,p},2n+1); for p>1 it maps to (v−1_{d,p}+(n+1)1_{d,p−1},n).Source: §2 · p. 3
  • Each evalF_d step preserves F_v(n), and iteration terminates because the vector strictly decreases in lexicographic order.The section defines evalF_d^max by iterating until the vector reaches zero.Source: §2 · p. 3

Properties

  • Starting from ((n+1)1_{d,d},n), maximal iteration reaches (0_d,F_{d+1}(n)); a supporting bound is F_v(n) ≥ 2|v|n+|v|.Here |v| is the sum of the vector coordinates.Source: §2 · p. 3

3 General Programs

This section formalizes programs over natural-number counters and distinguishes general, test-free, and checking programs, connecting their reachability problems to undecidability and Petri-net problems.

Counters and commands

  • Counters range over natural numbers, and increment, decrement, and test commands respectively add one, subtract one, or require the counter to be zero.Configurations are finite-support valuations of counters.Source: §3 · p. 4

Program model

  • A program can be a command, a loop, a sequential composition, or a nondeterministic choice, with size and dimension defined from its structure and used counters.Loops take reflexive-transitive closure, composition chains relations, and choice unions relations.Source: §3 · p. 4

Program subclasses

  • Test-free programs use no tests, while checking programs consist of a test-free program followed by tests on selected counters.Series composition and nondeterministic choice are associative, and the notation extends to repeated programs and counter lists.Source: §3 · p. 4

Reachability

  • General-program reachability is undecidable, whereas test-free reachability is inter-reducible with Petri-net coverability and checking-program reachability with Petri-net reachability.General reachability asks whether some execution from the zero configuration reaches a configuration.Source: §3 · p. 4

4 Simulating Test Commands

The section simulates tests using a test-free program that encodes whether prior simulations were correct in the relation y ≥ Kx, where K is the total of a finite counter set.

Simulation invariant

  • To simulate test(c), the construction uses auxiliary counters x and y and sets K to the sum of counters in B, maintaining y ≥ Kx as a correctness invariant.Equality y=Kx represents correct prior test simulations; strict inequality records at least one incorrect simulation.Source: §4 · p. 5

Test-free simulation

  • The test-free simulation transfers counter contents along an enumeration of B and back, decrementing y during both passes and decrementing x by two.Because the sum of B is invariant, y can decrease by at most 2K; achieving that full decrease requires c initially zero and maximal transfers, which restore B's counters.Source: §4 · p. 5

Simulation proof

  • The construction executes its transfer loops for the source counters' full values when y initially has at least 2K and x at least 2.The proof establishes an execution with both loop passes transferring each counter's full content.Source: §4 · pp. 5–6

Simulation properties

  • If y ≥ Kx holds initially, it still holds after the simulation; if equality holds afterward, then c was zero initially and the counters in B are restored.The formal lemma states that the total of counters in B is preserved and characterizes the equality case.Source: §4 · p. 6

5 Bounded Semantics and Preamplifiers

The section defines executions bounded by the total counter sum and introduces K-preamplifiers to simulate them with checking programs. This construction preserves reachability while controlling the resulting program’s dimension.

5 Bounded Semantics and Preamplifiers

  • K-bounded semantics restricts every configuration visited during an execution, including its endpoints, to have total counter sum at most K.It is the semantics used for general programs in the simulation.Source: §5 · p. 7
  • A K-preamplifier produces counters x, y, b with y ≥ bx, and equality y = bx forces b = K; it can realize equality for every x = ℓ ≥ 1.The remaining counters are zero in the described configurations.Source: §5 · p. 7
  • A K-preamplifier simulates K-bounded executions of general programs with a checking program, preserving the reached configuration.The construction has size size(A) + O(d size(M)) and dimension u + max(s, d), where u and s count unsafe and safe preamplifier counters.Source: §5 · pp. 7–8
  • The simulation offsets increments and decrements with changes to b and replaces each test with simtestx,B,y(c), then postpones the preamplifier’s tests until the end.This arrangement makes the checking program’s execution correspond to a K-bounded execution of the general program.Source: §5 · pp. 7–8
  • Small K-preamplifiers therefore yield small checking programs that simulate the K-bounded semantics of general programs.The section identifies preamplifiers as the means for this simulation.Source: §5 · pp. 7–8

6 Loop at Most

The section introduces a test-free program that repeats another program a counter-value-dependent number of times. Its iteration bounds and resulting counter values are constrained by the starting values of the two counters.

6 Loop at Most

  • The loop-at-most construction iterates a test-free program M using the values of two distinct counters c and c′.The section describes the iteration count as depending on counter valuations and assumes M does not use c or c′.Source: §6 · pp. 8–9
  • For the stated loop variant, the number of iterations ℓ is at most α(c) + α(c′), and equality forces β(c) = α(c) + α(c′) and β(c′) = 0.The cited result also gives β(c) ≤ α(c) + α(c′).Source: §6 · p. 9
  • In another stated variant, ℓ is at most α(c) + α(c′), β(c) is at most twice that sum, and equality in either bound forces ℓ to equal the sum.Under equality, β(c) = 2(α(c) + α(c′)) and β(c′) = 0.Source: §6 · p. 9
  • An execution decomposes into n iterations of the first loop and ℓ of the second, with n ≤ α(c) and ℓ ≤ n + α(c′).The proof tracks the resulting counter values after these loops.Source: §6 · p. 10

7 Implementing evalFd

The section implements evalFd with a test-free program whose good configurations encode inputs to the reduction rule. Its correctness relies on trapping erroneous computations in bad configurations and permitting a good output only for the proper branch.

7 Implementing evalFd

  • Good configurations encode (v, n) in counters c1 through cd and c0, with auxiliary counters satisfying the stated equalities.The encoding includes b = 2c0, x1 = 2c0x, and xi = 2ci−1xi−1 for i from 2 to d + 1.Source: §7 · p. 11
  • Erroneous computations are represented by bad configurations, and subsequent evalFd steps cannot turn a bad input into a good output.For conform configurations, the index of badness cannot decrease.Source: §7 · pp. 11, 16
  • The program chooses nondeterministically among evalFd,p branches, but a good output is possible only when p is the least index with v[p] > 0.That branch’s good output encodes evalFd(v, n).Source: §7 · p. 11
  • The branch construction transfers values between counters and uses bounded loops to perform its counter updates.The described loops transfer min(x1, …, xd) into y, transfer back from y, double xp during one loop, and iterate other loops according to C0, X, and B.Source: §7 · p. 11
  • From a good configuration encoding (v, n), evalFd can reach a good configuration encoding evalFd(v, n), while preserving xd+1.Conversely, if an evalFd computation ends good, its input was good and encoded a nonzero v with the expected reduction-rule result.Source: §7 · p. 16

8 Ackermannian Preamplifiers

The section constructs an Ackermann-scale K-preamplifier, a checking program whose executions enforce a relation among counters x, y, and b. The construction yields K = 2F_{d+1}(n) using 2d + 6 counters, d of them safe.

8 Ackermannian Preamplifiers

  • Lemma 18 states that the checking program Ackd,n is a K-preamplifier for K = 2Fd+1(n); the cited proof sets up a configuration β for ℓ≥1.It specifies β(x, y, b) = (ℓ, Kℓ, K) and β(c) = 0.Source: §8 · p. 17
  • Iterating evalFd over encoded configurations leads to a maximal configuration whose encoded value is F_{d+1}(n).The proof uses this maximality to establish the required final value K.Source: §8 · p. 17
  • The construction produces a K-preamplifier of size O(nd^4n) in time O(nd^4n), using 2d + 6 counters, d safe.The counter reduction is obtained by unfolding the program n times and removing an additional counter.Source: §8 · p. 18

9 Complexity Classes Beyond Elementary

The section transfers lower bounds for bounded reachability of two-dimensional general programs to checking programs. This proves F_d-hardness in dimension 2d + 4 and F_ω-hardness without a fixed dimension.

9 Complexity Classes Beyond Elementary

  • Reachability for (2d + 4)-dimensional checking programs is F_d-hard for every d ≥ 3, so dimension 10 is not elementary.The reduction maps bounded reachability of a two-dimensional general program to checking-program reachability.Source: §9 · p. 18
  • The fixed-dimension result is nearly optimal: reachability for d-dimensional checking programs is in F_{d+4}.This upper bound is attributed to [13].Source: §9 · p. 18
  • Reachability for checking programs is F_ω-hard, and the paper reports this bound is optimal because the problem is also in F_ω.The hardness follows from a reduction of bounded reachability for two-dimensional general programs.Source: §9 · p. 18

10 Conclusion

The conclusion states that checking-program reachability is Ackermannian-complete while identifying an unresolved gap in fixed-dimension parameterized complexity. It gives two possible research directions for closing that gap.

10 Conclusion

  • The paper proves that checking-program reachability is Ackermannian-complete.This is stated as the paper’s principal complexity conclusion.Source: §10 · p. 19
  • One proposed direction is a primitive-recursive construction of K-preamplifiers with dimension d + O(1).The target is K = F_d(n).Source: §10 · p. 19
  • A second proposed direction is a reachability algorithm with an upper bound in F_{d^2+O(1)}.Source: §10 · p. 19
Loading 2104.12695v4…