Variations of Checking Stack Automata: Obtaining Unexpected Decidability Properties
Oscar H. Ibarra, Ian McQuillan

TL;DR
This paper explores various models of checking stack automata, revealing unexpected decidability properties and differences between deterministic and nondeterministic versions, including the first one-way model with certain decidability characteristics.
Contribution
It introduces new variants of checking stack automata with unique decidability properties, including the first one-way model exhibiting specific decidability and undecidability behaviors.
Findings
Deterministic checking stack automata have decidable membership but undecidable emptiness.
Nondeterministic models can have both undecidable membership and emptiness.
Two-way deterministic machines with multiple stacks and counters have decidable membership.
Abstract
We introduce a model of one-way language acceptors (a variant of a checking stack automaton) and show the following decidability properties: (1) The deterministic version has a decidable membership problem but has an undecidable emptiness problem. (2) The nondeterministic version has an undecidable membership problem and emptiness problem. There are many models of accepting devices for which there is no difference with these problems between deterministic and nondeterministic versions, and the same holds for the emptiness problem. As far as we know, the model we introduce above is the first one-way model to exhibit properties (1) and (2). We define another family of one-way acceptors where the nondeterministic version has an undecidable emptiness problem, but the deterministic version has a decidable emptiness problem. We also know of no other model with this property in the literature.…
| nondeterministic class | membership | emptiness | deterministic class | membership | emptiness |
|---|---|---|---|---|---|
| \DCSACM(1) | |||||
| Prop 12 | Prop 12 | Prop 7 | Prop 12 | ||
| Prop 9 | Prop 9 | Prop 7 | Cor 10 | ||
| -head -stack | -head -stack | ||||
| Prop 9 | Prop 9 | Cor 30 | Cor 10 | ||
| no-read/no-decrease | no-read/no-decrease | ||||
| pg 3 | pg 3 | Prop 7 | Cor 14 | ||
| no-read/no-counter | no-read/no-counter | ||||
| Prop 18 | Prop 18 | Prop 7 | Cor 17 |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Variations of Checking Stack Automata: Obtaining Unexpected Decidability Properties
111A preliminary version of this paper has appeared in the Springer LNCS Proceedings of the 21st International Conference on Developments in Language Theory (DLT 2017), pp. 235–246.222©2018. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http://creativecommons.org/licenses/by-nc-nd/4.0/
Oscar H. Ibarra333Supported, in part, by NSF Grant CCF-1117708 (Oscar H. Ibarra).
Department of Computer Science
University of California, Santa Barbara, CA 93106, USA
Ian McQuillan444Supported, in part, by Natural Sciences and Engineering Research Council of Canada Grant 2016-06172 (Ian McQuillan).
Department of Computer Science, University of Saskatchewan
Saskatoon, SK S7N 5A9, Canada
Abstract
We introduce a model of one-way language acceptors (a variant of a checking stack automaton) and show the following decidability properties:
The deterministic version has a decidable membership problem but has an undecidable emptiness problem. 2. 2.
The nondeterministic version has an undecidable membership problem and emptiness problem.
There are many models of accepting devices for which there is no difference with these problems between deterministic and nondeterministic versions, i.e., the membership problem for both versions are either decidable or undecidable, and the same holds for the emptiness problem. As far as we know, the model we introduce above is the first one-way model to exhibit properties (1) and (2). We define another family of one-way acceptors where the nondeterministic version has an undecidable emptiness problem, but the deterministic version has a decidable emptiness problem. We also know of no other model with this property in the literature. We also investigate decidability properties of other variations of checking stack automata (e.g., allowing multiple stacks, two-way input, etc.). Surprisingly, two-way deterministic machines with multiple checking stacks and multiple reversal-bounded counters are shown to have a decidable membership problem, a very general model with this property.
keywords:
checking stack automata , pushdown automata , decidability , reversal-bounded counters
††journal: Theoretical Computer Science
\newclass\COMSLIP
COM-SLIP \newclass\COMSLIPCUPCOM-SLIP^∪ \newclass\DCMDCM \newclass\eDCMeDCM \newclass\eNPDAeNPDA \newclass\DPDADPDA \newclass\RDPDARDPDA \newclass\PDAPDA \newclass\DCMNEDCM_NE \newclass\TwoDCM2DCM \newclass\NCMNCM \newclass\eNCMeNCM \newclass\eNQAeNQA \newclass\eNSAeNSA \newclass\eNPCMeNPCM \newclass\eNQCMeNQCM \newclass\eNSCMeNSCM \newclass\DPCMDPCM \newclass\NPCMNPCM \newclass\NQCMNQCM \newclass\NSCMNSCM \newclass\NPDANPDA \newclass\TRETRE \newclass\NFANFA \newclass\DFADFA \newclass\NCANCA \newclass\DCADCA \newclass\DTMDTM \newclass\NTMNTM \newclass\NTMCMNTMCM \newclass\DLOGDLOG \newclass\CFGCFG \newclass\ETOLET0L \newclass\EDTOLEDT0L \newclass\CFPCFP \newclass\ORDERO \newclass\MATRIXM \newclass\BDBD \newclass\LBLB \newclass\ALLALL \newclass\decLBDdecLBD \newclass\StLBStLB \newclass\SBDSBD \newclass\TCATCA \newclass\LLL \newclass\CSACSA \newclass\DCSADCSA \newclass\NCSANCSA \newclass\GSMGSM \newclass\RDCSARDCSA \newclass\RNCSARNCSA \newclass\DCSACMDCSACM \newclass\NCSACMNCSACM
label1][email protected]
label2][email protected]
1 Introduction
The deterministic and nondeterministic versions of most known models of language acceptors exhibit the same decidability properties for each of the membership and emptiness problems. In fact, it is possible to define machine models in a general fashion by varying the allowed store types, such as with Abstract Families of Acceptors (AFAs) from [1], or a similar type of machine model with abstract store types used in [2] and in this paper. Studying machine models defined in such a general fashion is advantageous as certain decidability problems are equivalently decidable for arbitrary machine models defined using such a framework, and therefore it is possible to see which problems could conceivably differ in terms of decidability. For arbitrary one-way machine models defined in the way used here, the emptiness problem for the nondeterministic machines of this class, the membership problem for nondeterministic machines of this class, and the emptiness problem for the deterministic machines in this class, must all be either decidable or undecidable. Membership for deterministic machines could conceivably differ from the other three decidability problems. However, as far as we know, no one-way model has been shown to exhibit different decidability properties for deterministic and nondeterministic versions. The question arises of whether there is a model where membership for deterministic machines is decidable while it is undecidable for nondeterministic machines?
A second topic of interest here is that of studying decidability properties of different classes of machines when adding additional data stores. In [3], it was shown that for any one-way machine model (defined using another method used there), if the languages accepted by these machines are all semilinear555See [4] for the formal definition. Equivalently, a language is semilinear if it has the same commutative closure as some regular language., then augmenting these machines with additional reversal-bounded counters666A counter stores a non-negative integer that can be tested for zero, and it is reversal-bounded if there is a bound on the number of changes between non-decreasing and non-increasing. produces only semilinear languages. And, if semilinearity is effective with the original model, then it is also effective after adding counters, and therefore the emptiness problem is decidable. However, it is unknown what can occur when augmenting a class of machines that accepts non-semilinear languages with reversal-bounded counters. Can adding such counters change decidability properties?
These two topics are both simultaneously studied in this paper. Of primary importance is the one-way checking stack automaton [5], which is similar to a pushdown automaton that cannot erase its stack, but can enter and read the stack in two-way read-only mode, but once this mode is entered, the stack cannot change. This model accepts non-semilinear languages, but has decidable emptiness and membership problems. Here, we introduce a new model of one-way language acceptors by augmenting a checking stack automaton with reversal-bounded counters, and the deterministic and nondeterministic versions are denoted by and , respectively. The models with two-way input (with end-markers) are called and . These are generalized further to models with checking stacks: -stack and -stack . These models can be defined within the general machine model framework mentioned above.
We show the following results concerning membership and emptiness:
The membership and emptiness problems for s are undecidable, even when there are only two reversal-bounded counters. 2. 2.
The emptiness problem for is decidable when there is only one reversal-bounded counter but undecidable when there are two reversal-bounded counters. 3. 3.
The membership problem for -stack s is decidable for any .
Therefore, this machine model provides the first known model where membership is decidable for deterministic machines, while the other decidability properties are undecidable, which is the only property that can conceivably differ. It also shows one possible scenario that can occur when augmenting a machine model accepting non-semilinear languages with reversal-bounded counters: it can change the emptiness problem for both nondeterministic and deterministic machines to be undecidable, as with the membership problem for nondeterministic machines, but membership for deterministic machines can remain decidable (and therefore, all such languages accepted by deterministic machines are recursive).
In addition, we define another family of one-way acceptors where the deterministic version has a decidable emptiness problem, but the nondeterministic version has an undecidable emptiness problem. This model must necessarily not be defined using the general machine model framework, as emptiness for deterministic and nondeterministic machine models are always equivalently decidable. But the model is still natural and demonstrates what must occur to obtain unusual decidable properties. Further, we introduce a new family with decidable emptiness, containment, and equivalence problems, which is one of the most powerful families to have these properties (one-way deterministic machines with one reversal-bounded counter and a checking stack that can only read from the stack at the end of the input). We also investigate the decidability properties of other variations of checking stack automata (e.g., allowing multiple stacks, two-way input, etc.).
2 Preliminaries
This paper requires basic knowledge of automata and formal languages, including finite automata, pushdown automata, and Turing machines [6]. An alphabet is a (usually finite unless stated otherwise) set of symbols. The set is the set of all words over , which contains the empty word . A language is any set . Given a word , is the length of . A language is bounded if there exists words such that , and is letter-bounded if are letters.
We use a variety of machine models here, mostly built on top of the checking stack. It is possible to define each machine model directly. As discussed in Section 1, an alternate approach is to define “store types” first, which describes just the behavior of the store, including instructions that can change the store, and the manner in which the store can be read. This can capture standard types of stores studied in the literature, such as a pushdown, or a counter. Defined generally enough, it can also define a checking stack, or a reversal-bounded counter. Then, machines using one or more store types can be defined, in a standard fashion. A -machine is a machine with stores, where describes each store. This is the approach taken here, in a similar fashion to the one taken in [7] or [1] to define these same types of automata. This generality will also help in illustrating what is required to obtain certain decidability properties; see e.g. Lemma 1 and Proposition 2 which are proven generally for arbitrary store types. Furthermore, these two results are used many times within other proofs rather than having many ad hoc proofs. Hence, this generality in defining machines serves several purposes for this work.
First, store types, and machines using store types are defined formally using the same framework used by the authors in [2]. A store type is a tuple , where is the store alphabet (potentially infinite available to all machines using this type of store), is the set of allowable instructions, is the initial configuration which is a word in , and is the instruction language (over possibly an infinite alphabet) of allowable sequences of instructions, is the read function, a partial function from to , and is the write function, a partial function from to .
We will study a few examples of store types. First, a pushdown store type is a tuple , where is an infinite set of store symbols available to pushdowns, where special symbol is the bottom-of-stack marker, and , is the set of instructions of the pushdown, where the first set are called the push instructions, and the second set contains the pop and stay instruction, , , with , and is defined as:
- •
for ,
- •
, for ,
- •
, for .
A counter store tape can be obtained by restricting the pushdown store type to only having a single symbol (plus the bottom-of-stack marker). The instruction language in the definition of restricts the allowable sequences of instructions available to the store type (that is, a computation can only accept if its sequence of instructions is in the instruction language). This restriction does not exist in the definition of AFAs, but can be used to define many classically studied machine models, while still preserving many useful properties. For example, an -reversal-bounded counter store type is a counter store type with equal to the alternating concatenation of and with applications of concatenation (this is more classically stated as, there are at most alternations between non-decreasing and non-increasing).
Next, the more complicated stack store type is a tuple , where
- •
is an infinite set of store symbols available to stacks, where special symbols are the position of the read/write head in the stack, is the bottom-of-stack marker, and is the top-of-stack marker, with ,
- •
is the set of instructions of the stack, where the first set are called the push instructions, the second set is the pop and stay instruction, and the third set are the move instructions (down, stay, or up),
- •
, , with ,
- •
and is defined as:
- –
for ,
- –
, for ,
- –
, for ,
- –
, for , with ,
- –
, for ,
- –
, for .
That is, a stack is just like a pushdown with the additional ability to read from the “inside” of the stack (but not change the inside) in two-way read-only mode. Also, the checking stack store type is a restriction of stack store type above where is restricted to be in . That is, a checking stack has two phases, a “writing phase”, where it can push or stay (no pop), and then a “reading phase”, where it enters the stack in read-only mode. But once it starts reading, it cannot change the stack again.
Given store types , with , a two-way -head -tape -machine is a tuple where is the finite set of states, is the initial state, is the set of final states, is the finite input alphabet, is a finite subset of the store alphabets of , is the finite transition relation from to .
An instantaneous description (ID) is a tuple , where is the current state, is the current input word (surrounded by left input end-marker and right input end-marker), is the current position of tape head (this can be thought of as [math] scanning , and scanning ), for , and is the current word in the store, for . Then is deterministic if is a partial function (i.e. it only maps each element to at most one element).
Then , (two IDs) if there exists a transition , where is character of ( is added since is the letter at position [math]), and , for , , and for . Instead of , we can also write to show the instructions applied to each store on the transition. We let be the reflexive and transitive closure of , and let , where is the sequence of instructions applied to store , , in the sequence of transitions applied, and . The language accepted by , , is equal to
[TABLE]
Thus, the sequence of instructions applied to each store must satisfy its instruction language, and they must each be of the same length.
The different machine modes are combinations of either one-way or two-way, deterministic or nondeterministic, and -head for some . For example, one-way, -head, deterministic, is a machine mode. Given a sequence of store types and a machine mode, one can study the set of all -machines with this mode. The set of all such machines with a mode is said to be complete. Any strict subset is said to be incomplete. Given a set of (complete or incomplete) machines of this type, the family of languages accepted by these machines is denoted . For example, the set of all one-way deterministic pushdown automata is complete as it contains all one-way deterministic machines that use the pushdown store. But consider the set of all one-way deterministic pushdown automata that can only decrease the size of the stack when scanning the right end-marker. This is a strict subset of all one-way deterministic machines that use the pushdown store, since the instructions available to such machines depend on the location of the input (whether it has reached the end of the input or not). Therefore, this is an incomplete set of machines. The instruction language of a store does allow a complete class of machines to restrict the allowable sequences of instructions, but it has to apply to all machines using the store. Later in the paper, we will consider variations of checking stack automata such as one called no-read, which means that they do not read from the inside of the checking stack before hitting the right input end-marker. This is similarly an incomplete set of automata since the instructions allowed differs depending on the input position.
The class of one-way deterministic (resp. nondeterministic) checking stack automata is denoted by (resp., ) [5]. The class of deterministic (resp. nondeterministic), finite automata is denoted by (resp., [6]. For , the class of one-way deterministic (resp. nondeterministic) -reversal-bounded -counter machines is denoted by (resp. ). If only one integer is used, e.g. , this class contains all -reversal-bounded counter machines, for some , and if the integers is omitted, e.g., and , they contain all -reversal-bounded counter machines, for some . Note that a counter that makes reversals can be simulated by 1-reversal-bounded counters [8]. Closure and decidable properties of various machines augmented with reversal-bounded counters have been studied in the literature (see, e.g., [3, 8]). For example, it is known that the membership and emptiness problems are decidable for [8].
Also, here we will study the following new classes of machines that have not been studied in the literature: one-way deterministic (resp. nondeterministic) machines defined by stores consisting of one checking stack and -reversal-bounded counters, denoted by (resp. ), those with -reversal-bounded counters, denoted by (resp. ), and those with some number of reversal-bounded counters, denoted by (resp. ).
All models above also have two-way versions of the machines defined, denoted by preceding them with 2, e.g. , etc. We will also define models with checking stacks for some , which we will precede with the phrase “-stack”, e.g. -stack , -stack , -stack , -stack , etc. When , then this corresponds with omitting the phrase “-stack”.
3 A Checking Stack with Reversal-Bounded Counters
Before studying the new types of stores and machine models, we determine several properties that are equivalent for any complete set of machines. This helps to demonstrate what is required to potentially have a machine model where the deterministic version has a decidable membership problem with an undecidable emptiness problem, while both problems are undecidable for the nondeterministic version.
First, we examine a machine’s behavior on one word.
Lemma 1
Let be a one- or two-way, -head, for some , -machine, and let . We can effectively construct another -machine that is one-way and -head which accepts if and only if accepts . Furthermore, is deterministic if is deterministic.
Proof 1
The input is encoded in the state of , and on input , simulates the computation of and accepts if and only if accepts . This uses a subset of the sequence of transitions used by (and thereby would satisfy the instruction language of each store). Since is only on input, two-way input is not needed in , and the -heads are simulated completely in the finite control. \qed
Then, for all machines with the same store types, the following decidability problems are equivalent:
Proposition 2
Consider store types . The following problems are equivalently decidable, for the stated complete sets of automata:
the emptiness problem for one-way deterministic -machines, 2. 2.
the emptiness problem for one-way nondeterministic -machines, 3. 3.
the membership problem for one-way nondeterministic -machines, 4. 4.
acceptance of , for one-way nondeterministic -machines, 5. 5.
the membership problem for two-way -head (for ) nondeterministic -machines.
Proof 2
The equivalence of 1) and 2) can be seen by taking a nondeterministic machine . Let be labels in bijective correspondence with the transitions of . Then construct which operates over alphabet . Then reads each input symbol and simulates of on the store, while always moving right on the input. However, if it is a stay transition on the input of , then also checks that the next input symbol read (if any), , is defined on the same letter of in . Then is deterministic, and changes its stores identically in sequence to (thereby still satisfying the same instruction language), and is therefore empty if and only if is empty.
It is immediate that 5) implies 4), and it follows that 4) implies 5) from Lemma 1. Similarly, 3) implies 4), and 4) implies 3) from Lemma 1.
To show that 4) implies 2), notice that any complete set of nondeterministic one-way automata are closed under homomorphisms where , for all letters . Considering the homomorphism that erases all letters, the resulting language is empty if and only if is accepted by the original machine.
To see that 2) implies 4), take a one-way nondeterministic machine and make a new one that cannot accept if there is an input letter. This new machine is non-empty if and only if is accepted in the original machine. \qed
It is important to note that this proposition is not necessarily true for incomplete sets of automata, as the machines constructed in the proof need to be present in the set. We will see some natural restrictions later where this is not the case, such as sets of machines where there is a restriction on what instructions can be performed on the store based on the position of the input. And indeed, to prove the equivalence of 1) and 2) above, the deterministic machine created reads a letter for every transition of the nondeterministic machine applied. Hence, consider a set of machines that is only allowed to apply a strict subset of store instructions before the end-marker. Let be a nondeterministic machine of this type, and say that applies some instruction on the end-marker that is not available to the machine before the end-marker. But the deterministic machine created from in Proposition 2 reads an input letter when every instruction is applied, even including those applied on the end-marker of . But since is reading an input letter during this operation, it would violate the instructions allowed by before the end-marker.
The above proposition indicates that for every complete set of one-way machines, membership for nondeterminism, emptiness for nondeterminism, and emptiness for determinism are equivalent. Thus, the only problem that can potentially differ is membership for deterministic machines. Yet we know of no existing model where it differs from the other three properties. We examine one next.
We will study s and s, which are s and s (nondeterministic and deterministic checking stack automata) respectively, augmented by reversal-bounded counters. First, two examples will be shown, demonstrating a language that can be accepted by a .
Example 1
Consider the language . A with one 1-reversal-bounded counter can accept as follows: when given an input (we may assume that the input is of the form for some and for , since the finite control can check this), copies the first segment to the stack while also storing number in the counter. Then goes up and down the stack comparing to the rest of the input to check that while decrementing the counter by 1 for each segment it processes. Clearly, and makes only 1 reversal on the counter. We will show in Proposition 3 that cannot be accepted by an (or an ).
Example 2
Let . We can construct a to accept as follows. reads and stores in the stack. Then it reads and increments the counter by . Finally, reads while moving up and down the stack containing and decrementing the counter by 1 every time the stack has moved cells, to verify that is divisible by and . Then accepts , and needs only one 1-reversal counter. We will see in Proposition 27 that cannot be accepted by a .
The following shows that, in general, s and s are computationally more powerful than s and s, respectively.
Proposition 3
There are languages in . Hence, , and .
Proof 3
Consider the language from Example 1. cannot be accepted by an ; otherwise, can also be accepted by an (since languages are closed under homomorphism), but it was shown in [5] that cannot be accepted by any . However, Example 1 showed that can be accepted by a . Furthermore, is not semilinear, but only accepts semilinear languages [8]. \qed
We now proceed to show that the membership problem for s is decidable. In view of Lemma 1, our problem reduces to deciding, given a , whether it accepts . For acceptance of , the next lemma provides a normal form.
Lemma 4
Let be a . We can effectively construct a such that:
- •
all counters of are -reversal-bounded and each must return to zero before accepting,
- •
* always writes on the stack at each step during the writing phase,*
- •
the stack head returns to the left end of the stack before accepting,
whereby accepts if and only if accepts .
Proof 4
It is evident that all counters can be assumed to be -reversal-bounded as with [8], and that each counter can be forced to return to zero before accepting. Similarly, the checking stack can be forced to return to the left end before accepting. We introduce a dummy symbol \$$ to the stack alphabet so that if in a step, MM^{\prime}$M^{\prime}M^{\prime}M$M^{\prime}\lambdaM\lambda$. \qed
In view of Lemma 4, we may assume that a writes a symbol at the end of the stack at each step during the writing phase. This is important for deciding the following problem.
Lemma 5
Let be a satisfying the assumptions of Lemma 4. We can effectively decide whether or not , on input, has an infinite writing phase (i.e., will keep on writing).
Proof 5
Let be the number of states of . We construct an which, when given an input over the stack alphabet of , does the following: simulates the computation of on ‘stay’ transitions while checking that could be written by on the stack at some point during the computation of the writing phase of , while also verifying that there is a subword of of length such that was written by without:
incrementing a counter that has so far been at zero, and 2. 2.
decrementing a non-zero counter.
If so, accepts . Next, it will be argued that is not empty if and only if has an infinite writing phase on , and indeed this is decidable since emptiness for is decidable [8].
If is not empty, then there is a sequence of transitions during the writing phase where no counter during this sequence is increased from zero, and no counter is decreased. Thus, there must be some state hit twice by the pigeonhole principle, and the sequence of transitions between and itself must repeat indefinitely in . Thus, has an infinite writing phase on input.
Conversely, assume has an infinite writing phase. Then there must be a sequence of transitions where no counter is decreased, and no counter is increased from zero. Thus, must be non-empty. \qed
From this, decidability of acceptance of is straightforward.
Lemma 6
It is decidable, given a satisfying the assumptions of Lemma 4, whether or not accepts .
Proof 6
From Lemma 5, we can decide if has an infinite writing phase. If so, will not accept (as the stack must return to the bottom before accepting).
If does not have an infinite writing phase, the (final) word written in the stack is unique and hence has a unique length . In this case, we can simulate faithfully the computation of (on input) and determine .
We then construct a DCM , which on input, encodes the stack in the state and simulates . Thus, needs a buffer of size to simulate the operation of the stack, and accepts if and only if accepts. The result follows, since the membership problem for is decidable [8]. \qed
Proposition 7
For , the membership problem for -head is decidable.
We now give some undecidability results. The proofs will use the following result in [8]:
Proposition 8
[8]** It is undecidable, given a over a letter-bounded language, whether is empty.
Proposition 9
The membership problem for is undecidable.
Proof 7
Let be a machine over a letter-bounded language. Construct from an which, on input (i.e. the input is fixed), guesses an input to and writes it on its stack. Then simulates the computation of by using the stack and two reversal-bounded counters and accepts if and only if accepts. Clearly, accepts if and only if is not empty which is undecidable by Proposition 8. \qed
By Propositions 2 and 9, the following is true:
Corollary 10
The emptiness problem for is undecidable.
Combining together the results thus far demonstrates that is a model where,
- •
the deterministic version has a decidable membership problem,
- •
the deterministic version has an undecidable emptiness problem,
- •
the nondeterministic version has an undecidable membership problem,
- •
the nondeterministic version has an undecidable emptiness problem.
Moreover, this is the first (to our knowledge) model where these properties hold.
The next restriction serves to contrast this undecidability result. Consider an where during the reading phase, the stack head crosses the boundary of any two adjacent cells on the stack at most times for some given . Call this machine a -crossing . Then we have:
Proposition 11
It is decidable, given a -crossing , whether or not .
Proof 8
Define a -crossing to be an nondeterministic Turing machine with a one-way read-only input tape and a -crossing read/write worktape (i.e., the worktape head crosses the boundary between any two adjacent worktape cells at most times) augmented with reversal-bounded counters. Note that a -crossing can be simulated by a -crossing . It was shown in [3] that it is decidable, given a -crossing , whether . The proposition follows. \qed
Although we have been unable to resolve the open problem as to whether the emptiness problem is decidable for both and with one reversal-bounded counter, as with membership for the nondeterministic version, we show they are all equivalent to an open problem in the literature.
Proposition 12
The following are equivalent:
the emptiness problem is decidable for , 2. 2.
the emptiness problem is decidable for , 3. 3.
the emptiness problem is decidable for , 4. 4.
the membership problem is decidable for -head , 5. 5.
it is decidable if is accepted by a .
Proof 9
The last four properties are equivalent by Proposition 2.
It can be seen that 2) implies 1) because a machine can simulate a machine by taking the input, copying it to the stack, then simulating the machine with the two-way stack instead of the two-way input.
Furthermore, it can be seen that 1) implies 5) as follows: given a machine , assume without loss of generality, that immediately and nondeterministically sets the stack and returns to the bottom of the stack in read-only mode in some special state before changing any counter (as it can verify that would have pushed the stack contents). Then, build a machine that on some input over the stack alphabet, simulates the stack using the input, and the counter using the counter starting at state . Then is non-empty if and only if is accepted by . \qed
It is indeed a longstanding open problem as to whether the emptiness problem for is decidable [8].
Now consider the following three restricted models, with counters: For , a (or a ) machine is said to be:
- •
no-read/no-counter if it does not read the checking stack nor use any counter before hitting the right input end-marker,
- •
no-read/no-decrease if it does not read the checking stack nor decrease any counter before hitting the right input end-marker,
- •
no-read if it does not read the checking stack before hitting the right input end-marker.
We will consider the families of () machines satisfying each of these three conditions.
Proposition 13
For any , every machine can be effectively converted to an equivalent no-read/no-decrease machine, and vice-versa.
Proof 10
First, a machine can be simulated by a no-read/no-decrease machine that first copies the input to the stack, and simulates the input of using the checking stack, while simulating the counters faithfully. Indeed, the checking stack is not read and counters are not decreased until reads the entire input.
Next we will prove the converse. Let be a no-read/no-decrease machine with input alphabet and stack alphabet .
A two-way deterministic gsm, , is a deterministic generalized sequential machine with a two-way input (surrounded by end-markers), accepting states, and output. It is known that if is a language accepted by a two-way -head deterministic machine augmented with some storage/memory structure (such as a pushdown, checking stack, checking stacks, etc.), then is also accepted by the same type of machine [7].
Let be which, on input , first outputs . Then it moves to the left end-marker and on the second sweep of input , simulates and outputs the string written on the stack during the writing phase of . Note that can successfully do this as generates the checking stack contents from left-to-right, and does not read the contents during the writing phase; and because the counters of are not decreased during the writing phase of , the counters can never empty during the writing phase, thereby affecting the checking stack contents created. When reaches its right end-marker, it outputs the state of at that time, and then enters an accepting state. Thus, .
Now construct a which when given a string , reads , and while doing so, simulates the writing phase of on by only changing the counters as would do. Then, moves to the right and stores the state in the finite control. Then simulates the reading phase of on string (which only happens after the end of the input has been reached), starting in state and the current counter contents, and accepts if and only if accepts.
It is straightforward to see that , which can therefore be accepted by a machine. \qed
From this, the following is immediate, since emptiness for is known to be decidable [9].
Corollary 14
The emptiness problem for no-read/no-decrease is decidable.
In the first part of the proof of Proposition 13, the machine created from a machine was also no-read/no-counter. Therefore, the following is immediate:
Corollary 15
For , the family of languages accepted by the following three sets of machines coincide:
- •
all no-read/no-decrease machines,
- •
all no-read/no-counter machines,
- •
.
One particularly interesting corollary of this result is the following:
Corollary 16
The family of languages accepted by no-read/no-decrease (respectively no-read/no-counter) is effectively closed under union, intersection, and complementation. 2. 2.
Containment and equivalence are decidable for languages accepted by no-read/no-decrease machines.
This follows since this family is equal to , and these results hold for [9]. Something particularly noteworthy about closure of languages accepted by no-read/no-decrease under intersection, is that, the proof does not follow the usual approach for one-way machines. Indeed, it would be usual to simulate two machines in parallel, each requiring its own counter (and checking stack). But here, only one counter is needed to establish intersection, by using a result on two-way machines. Later, we will show that Corollary 16, part 2 also holds for no-read .
Also, since emptiness is undecidable for , even over letter-bounded languages [8], the following is true:
Corollary 17
The emptiness problem for languages accepted by no-read/no-counter is undecidable, even over letter-bounded languages.
Turning now to the nondeterministic versions, from the first part of Proposition 13, it is immediate that for any , every can be effectively converted to an equivalent no-read/no-decrease . But, the converse is not true combining together the following two facts:
Proposition 18
For every , the emptiness problem for languages accepted by over a unary alphabet is decidable. 2. 2.
The emptiness problem for languages accepted by no-read/no-counter (also for no-read/no-decrease) over a unary alphabet is undecidable.
Proof 11
The first part was shown in [9]. For the second part, it is known that the emptiness problem for (even over a letter-bounded language) is undecidable by Proposition 8. We construct a no-read/no-counter which, on a unary input, nondeterministically writes some string on the stack. Then simulates using . The result follows since if and only if . \qed
In contrast to part 2 of Proposition 18:
Proposition 19
For any , the emptiness problem for languages accepted by no-read/no-decrease machines over a unary alphabet, is decidable.
Proof 12
If is a no-read/no-decrease over a unary alphabet, we can effectively construct an equivalent (over a unary language) from Proposition 13. The result follows since the emptiness problem for over unary languages is decidable [9]. \qed
Combining these two results yields the following somewhat strange contrast:
Corollary 20
Over a unary input alphabet and for all , the emptiness problem for no-read/no-counter is undecidable, but decidable for no-read/no-counter .
As far as we know, this demonstrates the first known example of a family of one-way acceptors where the nondeterministic version has an undecidable emptiness problem, but the deterministic version has a decidable emptiness problem. This presents an interesting contrast to Proposition 2, where it was shown that for complete sets of automata for any store types, the emptiness problem of the deterministic version is decidable if and only if it is decidable for the nondeterministic version. However, the set of unary no-read/no-counter machines can be seen to not be a complete set of machines, as a complete set of machines contains every possible machine involving a store type. This includes those machines that read input letters while performing read instructions on the checking stack. And indeed, to prove the equivalence of 1) and 2) in Proposition 2, the deterministic machine created reads a letter for every transition applied, which can produce machines that are not of the restriction no-read/no-counter.
With only one counter, decidability of the emptiness problem for no-read/no-decrease , and for no-read/no-counter can be shown to be equivalent to all problems listed in Proposition 12. This is because 2) of Proposition 12 implies each immediately, and each implies 1) of Proposition 12, as a machine can be converted to a no-read/no-decrease, or no-read/no-counter machine where the input is copied to the stack, and then the machine simulated.
Therefore, it is open as to whether the emptiness problem for no-read/no-decrease (or no-read/no-counter) is decidable, as this is equivalent to the emptiness problem for . One might again suspect that decidability of emptiness for no-read/no-decrease implies decidability of emptiness for no-read/no-decrease by Proposition 2. However, it is again important to note that Proposition 2 only applies to complete sets of machines, including those machines that read input letters while performing read instructions on the checking stack, again violating the ‘no-read/no-decrease’ condition.
Even though it is open as to whether the emptiness problem is decidable for no-read/no-decrease , we have the following result, which contrasts Corollary 16, part 2:
Proposition 21
The universe problem is undecidable for no-read/no-counter s. (Thus, containment and equivalence are undecidable.)
Proof 13
It is known that the universe problem for a one-way nondeterministic 1-reversal-bounded one-counter automaton is undecidable [10]. Clearly, we can construct a no-read/no-counter to simulate . \qed
In the definition of a no-read/no-decrease , we imposed the condition that the counters can only decrement when the input head reaches the end-marker. Consider the weaker condition no-read, i.e., the only requirement is that the machine can only enter the stack when the input head reaches the end-marker, but there is no constraint on the reversal-bounded counters. It is an interesting open question about whether no-read languages are also equivalent to a (we conjecture that they are equivalent). However, the following stronger version of Corollary 14 can be proven.
Proposition 22
The emptiness problem is decidable for no-read s.
Proof 14
Let be a no-read . Let be symbols in bijective correspondence with transitions of that can occur in the writing phase. Then, build a machine that, on input over , reads while changing states as does, and changing the counter as the transitions do. Let be the state where the last transition symbol ends. Then, at the end of the input, simulates the reading phase of starting in by scanning , and interpreting a letter of as being the stack letter written by in (while always skipping over a letter if does not write to the stack in ). Then is empty if and only if is empty. \qed
We can further strengthen Proposition 22 somewhat. Define a restricted no-read to be a no-read which is only nondeterministic during the writing phase. Then the proof of Proposition 22 applies to the following, as the sequence of transition symbols used in the proof can be simulated deterministically:
Corollary 23
The emptiness problem is decidable for languages accepted by restricted no-read machines.
While we are unable to show that the intersection of two no-read languages is a no-read language, we can prove:
Proposition 24
It is decidable, given two no-read s and , whether .
Proof 15
Let and be no-read over input alphabet . Let be symbols in bijective correspondence with transitions of that can occur in the writing phase, for each . Let be the set of all pairs of symbols , where is a transition of , is a transition of , and where both and read the same input letter of . Let be all those symbols (r,\)rM_{1}T^{\prime\prime\prime}($,s)sM_{2}$ that stays on the input.
Build a machine operating over alphabet . On input , verifies that the first component changes states as does (skipping over any M_{1}qM^{\prime}M_{1}qwt\neq$wtM$tM^{\prime}M_{2}M_{1}a\in\SigmaM_{2}a\in\SigmaM_{1}M_{2}w=(s_{1},r_{1})(s_{2},$)(s_{3},$)($,r_{2})(s_{4},r_{3})s_{1}M_{1}r_{1}M_{2}s_{4}r_{3}s_{2}s_{3}M_{1}r_{2}M_{2}L(M^{\prime})L(M_{1})\cap L(M_{2})$ is empty. \qed
One can show that no-read languages are effectively closed under complementation. Thus, from Proposition 24:
Corollary 25
The containment and equivalence problems are decidable for no-read s.
No-read is indeed quite a large family for which emptiness, equality, and containment are decidable. The proof of Proposition 24 also applies to the following:
Proposition 26
It is decidable, given two restricted no-read s and , whether .
Finally, consider the general model (i.e., unrestricted). While it is open whether no-read is equivalent to , we can prove:
Proposition 27
.
Proof 16
It is obvious that any can be simulated by a (in fact by a no-read/no-counter ). Now let . We can construct a to accept by Example 2. However, it was shown in [11] that cannot be accepted by a by a proof that shows that if can be accepted by a , then one can use the decidability of the emptiness problem for s to show that Hilbert’s Tenth Problem is decidable. \qed
4 Multiple Checking-Stacks with Reversal-Bounded Counters
In this section, we will study deterministic and nondeterministic -checking-stack machines. These are defined by using multiple checking stack stores. Implied from this definition is that each stack has a “writing phase” followed by a “reading phase”, but these phases are independent of each letter for each stack.
A -stack ( respectively) is the deterministic (nondeterministic) version of this type of machine. The two-way versions (with input end-markers) are called -stack and -stack , respectively. These -stack models can also be augmented with reversal-bounded counters and are called -stack , -stack , -stack , and -stack .
Consider a -stack . By Lemma 1, for the membership problem, we need only investigate whether is accepted. Also, as in Lemma 4, we may assume that each stack pushes a symbol at each move during its writing phase, and that all counters are -reversal-bounded.
We say that has an infinite writing phase (on input) if no stack enters a reading phase. Thus, all stacks will keep on writing a symbol at each step. If has a finite writing phase, then directly before a first such stack enters its reading phase, all the stacks would have written strings of the same length.
Lemma 28
Let and be a -stack satisfying the assumption of Lemma 4.
We can determine if has an infinite writing phase. If so, does not accept . 2. 2.
If has a finite writing phase, we can construct a -stack satisfying the assumption of Lemma 4 such that accepts if and only if accepts .
Proof 17
Let have states and stack alphabets for the stacks. Let . By assumption, each stack of writes a symbol during its writing phase.
We can determine if has a finite writing phase as follows: As in Lemma 5, we construct an which, when given an input , does the following: simulates the computation of on ‘stay’ transitions such that the input was written by (in a component-wise fashion on each checking stack) and there is a subword of of length such that the subword was written by without:
incrementing a counter that has so far been at zero, and 2. 2.
decrementing a non-zero counter.
If so, accepts . So we need only check if is not empty, which is decidable since emptiness is decidable for [8]. Then, does not accept if and only if has an infinite writing phase, and if and only if is not empty, which is decidable.
If is empty, we then simulate faithfully to determine the unique word and its length just before the reading phase of at least one of the stacks, say , is entered. Note that by construction, no stack entered its stack earlier.
We then construct a -stack which, on input, encodes the operation of stack in the state and simulates (also converted into satisfying the assumptions of Lemma 4). Thus, needs a buffer of size to simulate the operation of stack . accepts if and only if accepts, and has one less stack than . \qed
Notice that has fewer stacks than . Then, from Proposition 7 (the result for a single stack) and using Lemma 28 recursively:
Proposition 29
The membership problem for -stack s is decidable.
Then, by Lemma 1:
Corollary 30
The membership problem for -head -stack is decidable.
This is one of the most general machine models known with a decidable membership problem. Although space complexity classes of Turing machines are also very general, the membership problem for both deterministic and nondeterministic Turing machines satisfying some space complexity function are both decidable. However, for s, membership is undecidable but is decidable for deterministic machines. Moreover, unlike space-bounded Turing machines, -head -stack s do not have a space restriction on their stacks.
5 Conclusions
We introduced several variants of checking stack automata and showed the difference between the deterministic and nondeterministic models with respect to the decidability of the membership and emptiness problems. The main decision problems are summarized in Table 1. We believe the contrasting results obtained are the first of its kind. An interesting open question is the status of the emptiness problem for nondeterministic checking stack automata augmented with one reversal-bounded counter which can only read the stack and decrease the counter at the end of the input. As shown in the paper, this problem is equivalent to a long-standing open problem of whether emptiness for two-way nondeterministic finite automata augmented with one reversal-bounded counter is decidable. Furthermore, we investigated possible scenarios that can occur when augmenting a machine model accepting non-semilinear languages with reversal-bounded counters. This contrasts known results on models accepting only semilinear languages.
Acknowledgements
We thank the Editor and the referees for their expeditious handling of our paper and, in particular, the referees for their comments that improved the presentation of our results.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] S. Ginsburg, Algebraic and Automata-Theoretic Properties of Formal Languages, North-Holland Publishing Company, Amsterdam, 1975.
- 2[2] O. Ibarra, I. Mc Quillan, On store languages of language acceptors, submitted. A preprint appears in https://arxiv.org/abs/1702.07388 (2017).
- 3[3] T. Harju, O. Ibarra, J. Karhumäki, A. Salomaa, Some decision problems concerning semilinearity and commutation, Journal of Computer and System Sciences 65 (2) (2002) 278–294.
- 4[4] M. Harrison, Introduction to Formal Language Theory, Addison-Wesley series in computer science, Addison-Wesley Pub. Co., 1978.
- 5[5] S. Greibach, Checking automata and one-way stack languages, Journal of Computer and System Sciences 3 (2) (1969) 196–217.
- 6[6] J. E. Hopcroft, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, MA, 1979.
- 7[7] J. Engelfriet, The power of two-way deterministic checking stack automata, Information and Computation 80 (2) (1989) 114–120.
- 8[8] O. H. Ibarra, Reversal-bounded multicounter machines and their decision problems, Journal of the ACM 25 (1) (1978) 116–133.
