Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Techniques for Showing the Decidability of the Boundedness Problem of Language Acceptors

Oscar H. Ibarra, Ian McQuillan

TL;DR

The paper tackles the boundedness problem for various language-accepting automata, introducing two core techniques: multi-tape characterizations that reduce complex models to decidable, simpler counterparts, and store-language analysis that captures feasible store contents during computations. By establishing representative transformations (e.g., between finite-turn NTMs and $(t+1)$-tape NFAs/NCMS, and via the history language $H(M)$), it proves decidability (and effective semilinearity) of boundedness for several powerful one-way nondeterministic models, including finite-turn NTMs with pushdowns and counters under restricted use, partially blind counters, and simple matrix grammars. The store-language approach further yields decidability results for finite-flip NPDA and related configurations, broadening the landscape beyond context-free languages. Together, these results extend known decidability of boundedness to a wide range of intermediate-language families and illuminate connections to containment problems and semilinearity, with potential implications for formal language theory and verification tasks.

Abstract

There are many types of automata and grammar models that have been studied in the literature, and for these models, it is common to determine whether certain problems are decidable. One problem that has been difficult to answer throughout the history of automata and formal language theory is to decide whether a given system $M$ accepts a bounded language (whether there exist words $w_1, \ldots,w_k$ such that $L(M) \subseteq w_1 \cdots w_k$?). Decidability of this problem has gone unanswered for the majority of automata/grammar models in the literature. Boundedness was only known to be decidable for regular and context-free languages until recently when it was shown to also be decidable for finite-automata and pushdown automata augmented with reversal-bounded counters, and for vector addition systems with states. In this paper, we develop new techniques to show that the boundedness problem is decidable for larger classes of one-way nondeterministic automata and grammar models, by reducing the problem to the decidability of boundedness for simpler classes of automata. One technique involves characterizing the models in terms of multi-tape automata. We give new characterizations of finite-turn Turing machines, finite-turn Turing machines augmented with various storage structures (like a pushdown, multiple reversal-bounded counters, partially-blind counters, etc.), and simple matrix grammars. The characterizations are then used to show that the boundedness problem for these models is decidable. Another technique uses the concept of the store language of an automaton. This is used to show that the boundedness problem is decidable for pushdown automata that can "flip" their pushdown a bounded number of times, and boundedness remains decidable even if we augment this device with additional stores.

Techniques for Showing the Decidability of the Boundedness Problem of Language Acceptors

TL;DR

The paper tackles the boundedness problem for various language-accepting automata, introducing two core techniques: multi-tape characterizations that reduce complex models to decidable, simpler counterparts, and store-language analysis that captures feasible store contents during computations. By establishing representative transformations (e.g., between finite-turn NTMs and -tape NFAs/NCMS, and via the history language ), it proves decidability (and effective semilinearity) of boundedness for several powerful one-way nondeterministic models, including finite-turn NTMs with pushdowns and counters under restricted use, partially blind counters, and simple matrix grammars. The store-language approach further yields decidability results for finite-flip NPDA and related configurations, broadening the landscape beyond context-free languages. Together, these results extend known decidability of boundedness to a wide range of intermediate-language families and illuminate connections to containment problems and semilinearity, with potential implications for formal language theory and verification tasks.

Abstract

There are many types of automata and grammar models that have been studied in the literature, and for these models, it is common to determine whether certain problems are decidable. One problem that has been difficult to answer throughout the history of automata and formal language theory is to decide whether a given system accepts a bounded language (whether there exist words such that ?). Decidability of this problem has gone unanswered for the majority of automata/grammar models in the literature. Boundedness was only known to be decidable for regular and context-free languages until recently when it was shown to also be decidable for finite-automata and pushdown automata augmented with reversal-bounded counters, and for vector addition systems with states. In this paper, we develop new techniques to show that the boundedness problem is decidable for larger classes of one-way nondeterministic automata and grammar models, by reducing the problem to the decidability of boundedness for simpler classes of automata. One technique involves characterizing the models in terms of multi-tape automata. We give new characterizations of finite-turn Turing machines, finite-turn Turing machines augmented with various storage structures (like a pushdown, multiple reversal-bounded counters, partially-blind counters, etc.), and simple matrix grammars. The characterizations are then used to show that the boundedness problem for these models is decidable. Another technique uses the concept of the store language of an automaton. This is used to show that the boundedness problem is decidable for pushdown automata that can "flip" their pushdown a bounded number of times, and boundedness remains decidable even if we augment this device with additional stores.
Paper Structure (9 sections, 24 theorems, 9 equations, 1 figure)

This paper contains 9 sections, 24 theorems, 9 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries and Notation
  3. Boundedness Using Multi-Tape Characterizations
  4. Characterizations of Finite-Turn Turing Machines
  5. Finite-Turn $\NTM$ with Pushdown and Counters
  6. Finite-Turn $\NTM$ with Partially Blind Counters
  7. Simple Matrix Grammars
  8. Store Languages for the Boundedness Problem
  9. Conclusions

Key Result

lemma 1

Let $t \ge 0$, and $M$ be a $t$-turn $\NTM$ (resp. $t$-turn $\NTCM$). We can construct a $(t+1)$-tape $\NFA$ (resp. $(t+1)$-tape $\NCM$) $M'$ such that $L(M' )^A = L(M).$

Figures (1)

  • Figure 1: In (a), it shows the counter values of counter $i$ is an original accepting computation of $M'$, where $i_j$ is the value at turn $j$ of the Turing tape. In (b), we see the modified computation of $M$ with each counter simulating in parallel.

Theorems & Definitions (36)

  • lemma 1
  • lemma 2
  • proposition 1
  • lemma 3
  • proof
  • proposition 2
  • proof
  • lemma 4
  • proposition 3
  • proposition 4
  • ...and 26 more