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}_{ε_0}$-complete. Here $\mathbf{F}_{ε_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}_{Ω_k}$-complete where $Ω_k$ is the tower of height $k$ of the $ω$ 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, $π$-calculus, logic and parameterized verification. Furthermore, using our completeness results for $k$-NRCS, we also prove $\mathbf{F}_{Ω_k}$-completeness of the considered problems from the realms of parameterized verification and logic, for all $k$.

翻译：嵌套计数器系统（NCS）是将计数器系统推广为高阶计数器的一种系统。其中，高阶计数器不仅可包含数值，还可包含其他（低阶）计数器作为元素。此类系统可视为在树上运行，树的高度自然对应于系统所处理的最高阶计数器。已知NCS的可覆盖性问题（即判断给定初始树能否覆盖给定最终树）是$\mathbf{F}_{ε_0}$-完备的，其中$\mathbf{F}_{ε_0}$是复杂度类快速增长层级中的一个类。本文考虑NCS的一种扩展——嵌套重置计数器系统（NRCS），该扩展在NCS中引入了重置操作。我们证明，对于$k$阶计数器的NRCS，可覆盖性是$\mathbf{F}_{Ω_k}$-完备的，其中$Ω_k$是高度为$k$的$ω$序数塔。这为所有这些类中的自然完备问题提供了首个层级结构。此外，为证明上界，我们还为有限集上多重集运算的任意固定次数应用建立了长度函数定理。作为结果的应用，我们改进了XML处理、图变换系统、$π$-演算、逻辑以及参数化验证等领域中若干问题的现有上界。同时，利用$k$-NRCS的完备性结果，我们证明了参数化验证与逻辑领域中所考虑问题对任意$k$均为$\mathbf{F}_{Ω_k}$-完备的。