The Complexity of Nested Reset Counter Systems

TL;DR

This paper explores the computational complexity of nested reset counter systems (NRCS), extending known results to a hierarchy of complexity classes and applying findings to various verification problems.

Contribution

It establishes the first natural hierarchy of complete problems for classes in the fast-growing hierarchy related to NRCS with resets.

Findings

Coverability for NRCS over order-k counters is $ extbf{F}_{oldsymbol{ ext{ extOmega}}_k}$-complete.

Develops length function theorems for multiset operations on finite sets.

Improves upper bounds for problems in XML processing, graph transformation, $oldsymbol{ ext{ extpi}}$-calculus, logic, and parameterized verification.

Abstract

Nested counter systems (NCS) are a generalization of counter systems to higher-order counters. Here, a higher-order counter is allowed to have other (lower-order) counters as elements, instead of just a number. Such systems can be viewed as working on trees, where the height of the tree naturally corresponds to the highest order counter that the system is working with. It is known that the coverability problem for NCS, which asks if a given final tree can be covered from a given initial tree, is $\mathbf{F}_{\epsilon_0}$-complete. Here $\mathbf{F}_{\epsilon_0}$ is a class in the fast-growing hierarchy of complexity classes. In this paper, we consider an extension of NCS called nested reset counter systems (NRCS) that extends NCS with resets. We show that coverability for NRCS over order-$k$ counters is $\mathbf{F}_{\Omega_k}$-complete where $\Omega_k$ is the tower of height $k$ of the $\omega$ ordinal. This gives the first natural hierarchy of complete problems for all of these classes. Furthermore, to prove our upper bounds, we also develop length function theorems for any fixed amount of applications of the multiset operation on finite sets. As an application of our results, we improve existing upper bounds for various problems from XML processing, graph transformation systems, $\pi$-calculus, logic and parameterized verification. Furthermore, using our completeness results for $k$-NRCS, we also prove $\mathbf{F}_{\Omega_k}$-completeness of the considered problems from the realms of parameterized verification and logic, for all $k$.