Reachability in Higher-Order-Counters

الأصل · EN

Higher-order counter automata () can be either seen as a restriction of higher-order pushdown automata () to a unary stack alphabet, or as an extension of counter automata to higher levels. We distinguish two principal kinds of: those that can test whether the topmost counter value is zero and those which cannot. We show that control-state reachability for level k with 0-test is complete for (k-2)-fold exponential space; leaving out the 0-test leads to completeness for (k-2)-fold exponential time. Restricting (without 0-test) to level 2, we prove that global (forward or backward) reachability analysis is -complete. This enhances the known result for pushdown systems which are subsumed by level 2 without 0-test. We transfer our results to the formal language setting. Assuming that EXPTIME, we apply proof ideas of Engelfriet and conclude that the hierarchies of languages of and of form strictly interleaving hierarchies. Interestingly, Engelfriet's constructions also allow to conclude immediately that the hierarchy of collapsible pushdown languages is strict level-by-level due to the existing complexity results for reachability on collapsible pushdown graphs. This answers an open question independently asked by Parys and by Kobayashi.