Two-Way One-Counter Nets Revisited

Two-way automata have received much attention since their introduction for finite automata in [30]. 2-PDAs were studied in [24, 14, 4, 27], focusing mainly on closure properties and languages recognizable by 2-PDAs. As noted in [4], languages not expressible by 2-PDA can be derived from the complexity results obtained in [14] (specifically, 2-PDA languages are in linear space and polynomial time, and the time/space hierarchy theorems offer languages outside of these classes). No automata-based, combinatorial techniques are known to the authors to show that some languages is not expressible with a 2-PDA, and most questions about 2-PDA, including whether the deterministic variant can recognize all context-free languages, are open [13].

In the world of counter machines, [12] shows that DFAs with a “blind tape” (a form of a nonnegative counter that cannot be 0-tested) are less expressive than 2-DPDAs. A significant body of work by Ibarra et al. studies reversal bounded counters [19, 21, 18, 10, 20], i.e., counters that cannot increase and decrease unboundedly many times. The heavy reliance on reversal-boundedness makes these works orthogonal to ours. Atig and Ganty [5] study a VASS-CFG hybrid, and use also make use of reductions to VASS with 0-tests, but with significant technical differences.

Closer to our setting are two-way one-counter automata (2-OCAs), that allow explicit zero tests. In [29] certain languages computing squaring or exponentiation are shown not to be 2-DOCA recognizable (the deterministic variant), whereas [11] exhibit nonsemilinear 2-OCA languages. Ibarra and Su [21] note that 1-sweep 2-DOCA have an undecidable emptiness problem; in contrast, we show that this problem is decidable for sweeping 2-OCN. They also note that, over bounded languages, emptiness of 2-DOCA is decidable provided that the counter reaches zero only a constant number of times; in contrast, we show that this emptiness over bounded languages is decidable for any 2-OCN.

A nearly identical model to 2-OCN has been introduced in [26] and further studied in [7]. In their model, the counter updates are $\pm 1$, which essentially amounts to encoding counters in unary. In [26], the focus is on 2-DOCN recognizable languages. It is shown that this class is closed under intersection, but not under complementation nor union. Further, over bounded languages, 2-DOCN can be made sweeping¹¹1The proof in [26] is actually missing significant details, but those can be reconstructed., and the Parikh images of their languages are semilinear. An example is also given to show that 2-DOCN are less expressive than 2-OCN.

The algorithmic contribution in [7] is that the emptiness problem for 2-DOCN is undecidable. Additionally, it is shown that if a 2-OCN accepts a word of length $n$, then it accepts it with a run of polynomial length in $n$. The latter result no longer holds for our model, due to the binary encoding of the counters.

In this work we provide a modern view of 2-OCNs and some of its interesting and decidable fragments, namely bounded-language 2-OCNs and sweeping 2-OCNs. In Section 3.1 we give a counter-machine based proof of the undecidability of 2-DOCN emptiness. In Section 3.2, we consider 2-OCNs whose languages are bounded, i.e., of the form $L\subseteq a_1^{\ast }{a}_2^{\ast }\mathrm{\cdots }{a}_k^{\ast }$. We show that under this restriction, emptiness becomes decidable. In Section 3.3, we consider sweeping 2-OCNs, i.e., 2-OCNs whose head-movement direction only changes at the end-markers. We show that here too emptiness becomes decidable and we give precise complexity bounds, using recent results regarding VASS reachability. In Section 4, we investigate the relationship between semilinear languages and 2-OCN languages. We show that for bounded languages, the set of lengths of words in the language of a 2-OCN is semilinear, and derive explicit languages that are not 2-OCN-recognizable. We also show that a bounded language is semilinear if and only if it is recognizable by a sweeping 2-OCN. In Section 5, we show an elaborate pumping lemma for 2-DOCNs. Apart from its independent usefulness for understanding 2-DOCNs, this enables us to demonstrate a 1-OCN whose language is not 2-DOCN recognizable, establishing a new separation result. We conclude in Section 6 with some open problems.

We encourage the reader to initially skip the proofs and garner a bird’s eye view of our results. Thereafter, we note that Sections 3.2, 17, 14, and 15 have the most interesting proofs. Detailed proofs appear in the appendix or in the full version.

For an alphabet set $\mathrm{\Sigma }$, we denote ${\mathrm{\Sigma }}_{⊢⊣}=\mathrm{\Sigma }\cup \{⊢,⊣\}$ where $⊢,⊣$ are two symbols not appearing in $\mathrm{\Sigma }$, called left end-marker and right end-marker, respectively. A Two-Way One-Counter Net (2-OCN) is a tuple $𝒜=⟨Q,\mathrm{\Sigma },\mathrm{\Delta },q_{\mathrm{init}},q_{\mathrm{acc}}⟩$ where $Q$ is a finite set of states, $\mathrm{\Sigma }$ is a finite alphabet, $\mathrm{\Delta }\subseteq Q\times {\mathrm{\Sigma }}_{⊢⊣}\times \mathbb{Z}\times \{-1,+1\}\times Q$ is a finite set of transitions, $q_{\mathrm{init}},q_{\mathrm{acc}}\in Q$ are the initial and accepting states, respectively. Intuitively, a transition $\tau =(q,\sigma ,e,h,q^{\prime })$ dictates that from state $q$, when reading letter $\sigma$, we add $e$ to the counter value, move the position of the head on the tape by $h$, and reach state $q^{\prime }$. We call $e$ the effect and $h$ the head shift of the transition. Unless explicitly stated otherwise, we assume that the effect $e$ is encoded in binary. We require that if $(q,⊢,e,h,q^{\prime })\in \mathrm{\Delta }$ then $h=1$ and if $(q,⊣,e,h,q^{\prime })\in \mathrm{\Delta }$ then $h=-1$. That is, upon reaching the end-markers, the head cannot proceed beyond them.

We say that $𝒜$ is deterministic (denoted 2-DOCN) if for every $q\in Q,\sigma \in {\mathrm{\Sigma }}_{⊢,⊣}$ there is at most one $q^{\prime }\in Q$ and $e,h$ such that $(q,\sigma ,e,h,q^{\prime })$. We say that $𝒜$ is one way (denoted 1-OCN) if every transition moves the head to the right (i.e., the head shift is 1).

A configuration of $𝒜$ is $(q,c,p)\in Q\times \mathbb{N}\times \mathbb{N}$ representing the current state $q$, counter value $c$, and head position $p$. Note that we do not consider configurations with negative counter values, thus enforcing the semantics of Counter Nets. Consider a word $w={\sigma }_1\mathrm{\cdots }{\sigma }_m\in {\mathrm{\Sigma }}^{\ast }$, we augment it to $⊢w⊣$ by setting ${\sigma }_0=⊢$ and ${\sigma }_{m+1}=⊣$. A run of $𝒜$ on $w$ is a finite sequence of configurations $\rho =(q_1,c_1,p_1),(q_2,c_2,p_2),\mathrm{\dots },(q_n,c_n,p_n)$ such that $0\le p_i\le m+1$ for all $i$, and for every we have $(q_i,{\sigma }_{p_i},c_{i+1}-c_i,p_{i+1}-p_i,q_{i+1})\in \mathrm{\Delta }$. That is, each configuration follows from the previous one by the transition relation. A run is initial if $q_1=q_{\mathrm{init}}$ and $p_1=c_1=0$. A run is accepting if $q_n=q_{\mathrm{acc}}$. We tacitly assume that runs do not continue after the accepting state. The word $w$ is accepted by $𝒜$ if $𝒜$ has an initial and accepting run on it. We define $L(𝒜)=\{w\in {\mathrm{\Sigma }}^{\ast }\mid 𝒜\text{ accepts }w\}$. Note that, just like OCNs, 2-OCNs are monotone, i.e., every word accepted from initial configuration $(q,c,p)$ is also accepted from $(q,c^{\prime },p)$ for every $c^{\prime }>c$. We sometimes consider sequences of pseudo-configurations where the counter value becomes negative. In such cases, we say that the run is cut short by a counter violation, and we mean that the sequence of configurations is a run up to a prefix in which the counter becomes negative.

Finally, we sometimes discuss classical Boolean automata (NFA, DFA, 2-NFA and 2-DFA). For our purposes, they can be thought of as 2-OCN where all the counter updates are $0$, and are therefore omitted.

A Vector Addition System with States (VASS) is a tuple $𝒱=⟨S,T⟩$ where $S$ is a finite set of states and $T\subseteq S\times {\mathbb{Z}}^d\times S$ is the transition relation. A configuration of $T$ is $(s,𝒗)$ where $s\in S$ and $𝒗\in {\mathbb{N}}^d$ (note that this is a vector of nonnegative integers). We say that configuration $(s_2,𝒚)$ is reachable from configuration $(s_1,𝒙)$ if there is a finite sequence of configurations $(p_1,{𝒗}_{\mathrm{𝟏}}),\mathrm{\dots },(p_m,{𝒗}_{𝒎})$ such that $(p_1,{𝒗}_{\mathrm{𝟏}})=(s_2,𝒚),(p_m,{𝒗}_{𝒎})=(s_2,𝒚)$ and for every we have $(p_i,{𝒗}_{𝒊\mathbf{+}\mathrm{𝟏}}-{𝒗}_{𝒊},p_{i+1})\in T$. Intuitively, a VASS runs by repeatedly adding vectors to the configuration, as long as all the counters (i.e., the entries of the vector) remain nonnegative. The reachability problem for VASS asks whether $(s_2,𝒚)$ is reachable from $(s_1,𝒙)$ and is known to be decidable [9].

While VASS do not allow explicit 0-tests, it is possible to simulate a fixed number of 0-tests within the context of reachability [8, 9]. That is, we can extend the transition relation so that $T\subseteq S\times {\mathbb{Z}}^d\times {\{=0,\ge 0\}}^d\times S$, and a transition can be taken only when the counters that have $=0$ tests are 0. As long as there is a constant $B$ such that there are no more than $B$ 0-tests along every run of the VASS, then reachability remains decidable. The simplest approach to achieve this is to increase the dimension by $d\cdot B$, keeping $B$ copies of every counter, and whenever a counter needs to be tested for 0, a copy of it is “frozen” (i.e., never changes again) and the reachability target has $0$ on all frozen entries. Note that we can mark which entries are frozen in the states of the VASS, since there are at most $B$ of them. We remark that more elaborate approaches can keep the number of added counters small [8, 9]. We call such machines VASS with bounded 0-tests.

Emptiness decidability has been historically intimately tied to semilinearity. A set $E\subseteq {\mathbb{N}}^d$ is semilinear if it is expressible in first-order logic with addition (there are many equivalent definitions and we will not need a specific one). The Parikh image of a language $L$ over an alphabet $\{a_1,\mathrm{\dots },a_k\}$ is the set of vectors $(n_1,\mathrm{\dots },n_k)$ such that there is a word in $L$ with precisely $n_i$ letters $a_i$ (in any order), for all $i$. In other words, the Parikh image counts the number ${|w|}_{\mathrm{\ell }}$ of times each letter $\mathrm{\ell }$ appears in a word $w\in L$, resulting in a set of vectors in ${\mathbb{N}}^{|\mathrm{\Sigma }|}$. A class of languages is semilinear if for any language $L$ in that class, the Parikh image of $L$ is semilinear. In that case, if there is an algorithmic way to obtain a representation of that semilinear set from a representation of $L$, then one can check whether $L=\mathrm{\varnothing }$, since satisfiability is decidable for first-order logic with addition [6].

Since the emptiness problem is undecidable for 2-DOCN, it is an unsurprising fact that there are nonsemilinear 2-DOCN languages (e.g., $\{{(a^n\mathrm{\#})}^n\mid n>1\}$). A tantalizing question surging from the study in Section 3.2 is: Are all 2-OCN bounded languages semilinear? For 2-DOCN, it is proved in [26] that this is indeed the case. For 2-OCN, it is likely that a proof of this statement would provide an alternative proof to Theorem 5. We conjecture that, indeed, 2-OCN are in good company with a wealth of computational models whose bounded languages are precisely those with a semilinear Parikh image. We come short of showing this, but prove, using the construction of Section 3.2 and a result of [15], that:

In [15, Corollary 4.3] the following is shown.²²2In [15] the result is phrased for Petri Nets, but the equivalence between Petri Nets and VASS gives a straightforward translation. In [22], a slightly weaker result is presented in the language of VAS. Given a VASS $𝒱=⟨S,T⟩$ of dimension $d$ and two states $s_1,s_2$, consider the set ${ℛ}_{s_1,s_2}\subseteq {\mathbb{N}}^d\times {\mathbb{N}}^d\times {\mathbb{N}}^T$ such that $(𝒑,{𝒑}^{\mathbf{\prime }},𝒕)\in {ℛ}_{s_1,s_2}$ iff $(s_2,{𝒑}^{\mathbf{\prime }})$ is reachable from $(s_1,𝒑)$ via a run $\rho$ that takes transition $\tau$ exactly $𝒕(\tau )$ times. Then the image of every morphism $\pi :{ℛ}_{s_1,s_2}\to \mathbb{N}$ is effectively semilinear.

In our setting, take $𝒱$ to be the VASS obtained in Section 3.2 with the states $s_{\text{init}},s_{\text{fin}}$ and $𝒑={𝒑}^{\mathbf{\prime }}=\mathrm{𝟎}$. Let $\pi$ be the morphism that counts the number of transitions used to initialize $n_i$ for all $a_i\in \mathrm{\Gamma }$, and recall that by the correctness of the construction of $𝒱$, we have that along a run from $(s_{\text{init}},\mathrm{𝟎})$ to $(s_{\text{fin}},\mathrm{𝟎})$, the value of $n_i$ after the Initialization Component corresponds to the length of the $a_i$ segment in an accepted word. Then, [15, Corollary 4.3] readily shows that the set $\{{\sum }_{a_i\in \mathrm{\Gamma }}{n}_i\mid a_1^{n_1}\mathrm{\cdots }{a}_k^{n_k}\in L(𝒜)\}$ is effectively semilinear. $◀$ The previous theorem implies that 2-OCN languages over a singleton alphabet are semilinear. In addition, we have the following:

We note that Theorem 9 also applies to sweeping 2-OCN without the bounded language restriction, with a similar proof.

However, unlike the case of bounded languages, here we can show that the Parikh image of sweeping 2-OCN language are not always semilinear.

Consider the Dyck language over $\{a,b\}$, i.e., well-parenthesized expressions where $a$ corresponds to an opening parenthesis and $b$ to a closing one. Write $P$ for the prefixes of that language. Clearly, $P$ is a 1-DOCN language. Write $P^{\prime }$ for the language $P$ where $a$ and $b$ swap roles. We can construct a sweeping 2-DOCN that recognizes $K=P\cap a^{\ast }{P}^{\prime }$ using the closure of 2-DOCN under intersection [26] (which preserves the sweeping property). In any word $w$ in $K$, if $n$ is the length of the first block of $a$’s, then $0\le {|w|}_a-{|w|}_b\le n$. Finally, using a few more sweeps, we can express:

Indeed, this requires checking that the number of $c$’s is equal to the number of $a$’s in the first block, the number of $b$’s in the last block, and the number of $ab$ infixes.

Now, for a fixed value $n$, the longest word in $L$ that can appear after $c^n\mathrm{\#}$ is ${(a^n{b}^n)}^n$, of length $2n^2$, showing that this language is not semilinear. $◀$

We will show, in Section 5, that there is a 1-OCN language (thus a sweeping 2-OCN language) this is not expressible using a 2-DOCN. Conversely, Proposition 12 provides an easy way to show that:

Consider the language $L$ over the alphabet $\{a,b,c,\mathrm{\#},\underset{¯}{b},x\}$ defined as:

By applying the morphism $h:{\mathrm{\Sigma }}^{\ast }\to {\mathrm{\Sigma }}^{\ast }$ that erases $\underset{¯}{b},\mathrm{\#}$, and $x$, we have $h(L)=\{a^n{b}^m{c}^{nm}\}$, which can be seen as multiplication.

The language $L$ is recognizable by a 2-DOCN $𝒜$ by repeatedly using a similar approach to Example 1:

• $\mathrm{■}$

  Check that the input has the form $a^{\ast }\mathrm{\#}{b}^{\ast }{(x^{\ast }\mathrm{\#}{\underset{¯}{b}}^{\ast })}^{\ast }{c}^{\ast }$,

• $\mathrm{■}$

  Check that the number of $a$’s is the same as the number of $\mathrm{\#}$’s,

• $\mathrm{■}$

  Check that the first sequence of $\underset{¯}{b}$’s is as long as the sequence of $b$’s,

• $\mathrm{■}$

  Check that the lengths of all sequences of $\underset{¯}{b}$’s are equal, by checking that each neighboring sequence $\mathrm{\#}{\underset{¯}{b}}^i{x}^{\ast }\mathrm{\#}{\underset{¯}{b}}^j{x}^{\ast }$ satisfies $i=j$,

• $\mathrm{■}$

  Check for each sequence $x^i\mathrm{\#}{\underset{¯}{b}}^m{x}^j$ that $i+m=j$, and the same for the last segment where $x$ is replaced with $c$.

This 2-DOCN proceeds segment by segment, always making sure that the number of $x$’s increases by exactly $m$. This, together with the initial test that the number of segments is $n$, forces the number of $c$’s to be exactly $nm$.

However, the lengths of words in this language do not form a semilinear set, so by Theorem 11 it cannot be recognized by a sweeping 2-OCN. $◀$

Over bounded languages, the following exact characterization holds:

The fact that any semilinear bounded language can be expressed with a sweeping 2-OCN is easily deduced from the fact that semilinear sets are those expressible with quantifier-free first-order formulas with addition, order, and modulo. Putting such a formula in DNF, we simply need to guess which conjunction is to hold, and the conjunction can be checked by a sweeping 2-DOCN using the closure of 2-DOCN under intersection [26] (which preserves the sweeping property).

We turn to the fact that bounded languages expressed by sweeping 2-OCN are semilinear. We split the proof into two parts.

Let us first assume that the sweeping 2-OCN $𝒜$ executes a constant number of sweeps, say $C$, with $C$ odd, for each input word (we assume here that the machine ends at the right end-marker). With $L(𝒜)\subseteq a_1^{\ast }\mathrm{\cdots }{a}_k^{\ast }$, consider the following transformation that produces a word over the alphabet $\mathrm{\Gamma }=\{a_{i,j}\mid 1\le i\le C\wedge 1\le j\le k\}$:

That is, the input is replicated $C$ times, with every other copy reversed, and each copy on its own alphabet. Let us call $w^{\prime }$ the replica of $w$. Since $𝒜$ makes at most $C$ sweeps, we can build a 1-OCN $ℬ$ that reads the replica of any word $w\in a_1^{\ast }\mathrm{\cdots }{a}_k^{\ast }$ and accepts if and only if $w$ is accepted by the 2-OCN (and the input is of the format $R=a_{1,1}^{\ast }\mathrm{\cdots }{a}_{1,k}^{\ast }\mathrm{\#}{a}_{2,k}^{\ast }\mathrm{\cdots }{a}_{2,1}^{\ast }\mathrm{\#}\mathrm{\cdots }$ $\mathrm{\#}{a}_{C,1}^{\ast }\mathrm{\cdots }{a}_{C,k}^{\ast }$). Naturally, $ℬ$ also accepts words that are not replicas.

We circumvent this problem by using an “external” semilinear set, as follows. Let $E$ be the Parikh image of the language where for all $i$, each $a_{\bullet ,i}$ appears the same number of times; clearly, a word in $R$ is a replica iff its Parikh image is in $E$. Since $ℬ$ is a 1-OCN language (and in particular context-free), the Parikh image $F$ of its language is semilinear by Parikh’s Theorem [28]. It is then easy to check that $E\cap F$ is exactly the set of Parikh images of replicas of words in $L(𝒜)$, showing that the Parikh image of $L(𝒜)$ itself is semilinear (as a projection of the former).

If $𝒜$ is sweeping but does not do a constant number of sweeps for each input, we adapt the recurring idea of Sections 3.2 and 3.3. Let $k$ be the number of states of $𝒜$. After $2k+1$ sweeps, a state is repeated at the left end-marker; if the counter effect between the two repetitions is nonpositive, then that run is not useful for acceptance, and can be disregarded. If the counter increases, then it can be increased arbitrarily, and the behavior of the 2-OCN is the same as a 2-NFA $𝒩$ from that point on. Consider the 1-OCN $ℬ$ constructed above, with $C=2k+1$. We can additionally have $ℬ$ guess the state that repeats, if any, and check that it indeed repeats. Next, $ℬ$ assumes that the counter strictly increases in the repetition, and branches into a DFA for $𝒩$. In order to “kill” the runs of $ℬ$ where this assumption is incorrect, any transition that $ℬ$ takes, in between the first and second appearance of the repeated state, should be followed by input symbols indicating the counter effect, increasing (${\text{+}}^{\ast }$) or decreasing (${\text{-}}^{\ast }$), and by how much. $ℬ$ then verifies that the correct effect is matched to the transition of $𝒜$ it guesses. For instance, $ℬ$ may read the following replica of $aabbbc$ with extra counter information (here the original alphabet is $\{a,b,c\}$ and the replica alphabet has $1,\mathrm{\dots },5$ as indices):

As mentioned, this modified version of $ℬ$ may jump into a DFA for $𝒩$ when it should not. However, we can augment the external semilienar set $E$, checking that the input word is a replica, to also check that the number of + is strictly greater than the number of -. This corresponds to the counter updates between the state repetitions having a strict positive impact, and that $ℬ$ correctly jumps into $𝒩$’s simulation. To conclude, let again $F$ be the (semilinear) Parikh image of the language of $ℬ$. The vectors in $E\cap F$ correspond precisely to the replicas (with possibly explicit counter updates) that are accepted by $𝒜$, hence the language of $𝒜$ is semilinear. $◀$

$L$ is 1-OCN recognizable by guessing whether $\mathrm{\ell }>m$ or $m>n$, and checking by either increasing the counter on $a$ and decreasing on $b$, or increasing on $b$ and decreasing on $c$ (with another decrease at the end to make the inequality strict). Assume by way of contradiction that $L=L({𝒟}_2)$ for a 2-DOCN ${𝒟}_2$. Let $K$ be the constant provided by Lemma 15, then $a^K{b}^K{c}^K\notin L=L({𝒟}_2)$. Then, Lemma 15 guarantees that there exists $K^{\prime }\ne K$ such that $a^K{b}^{K^{\prime }}{c}^K\notin L({𝒟}_2)$, but $a^K{b}^{K^{\prime }}{c}^K\in L$, since either $K>K^{\prime }$ or $K^{\prime }>K$, a contradiction. $◀$ We remark that we can similarly show that $L_2=\{a^n{b}^m\mid n\ne m\}$ is also not 2-DOCN recognizable (but is recognizable by a sweeping 2-OCN), giving an alternative proof to the result in [26].

The classes we consider, 1-OCN, 1-DOCN, 2-OCN, 2-DOCN, sweeping and nonsweeping, over bounded languages or not, are all provably distinct, except for the following: are all bounded 2-OCN languages expressible with a sweeping machine? We conjecture that they are, and leave this question open (this is known for 2-DOCN from [7]).

The examples of languages outside 2-DOCN readily show that the class of languages recognized by 2-DOCN is not closed under union nor complement, but is closed under intersection (also shown in [26]). For 2-OCN, the class is closed under union, but we conjecture that it is closed under neither intersection nor complement. We leave these questions open, together with the same questions for sweeping 2-OCN.

Beyond emptiness, our proofs imply that it is decidable whether the intersection of two (sweeping or bounded) 2-OCN is empty. The next natural question is then the decidability of inclusion. We conjecture that this problem is decidable for sweeping and bounded 2-OCN.