<p><strong>Lemma 1.</strong> <em><span class="math-container">$H_{\textsf{2nfa}}$</span> is decidable.</em></p>

<p><em>Proof.</em>  Decide it as follows.  Given as input a two-way non-deterministic finite automaton <span class="math-container">$M_{\textsf{2nfa}}$</span>:</p>

<ol>
<li><p>Convert <span class="math-container">$M_{\textsf{2nfa}}$</span> into a <a href="https://en.wikipedia.org/wiki/Two-way_finite_automaton#Two-way_alternating_finite_automaton" rel="nofollow noreferrer">two-way alternating finite automaton</a> <span class="math-container">$M_{\textsf{2wafa}}$</span> such that the language of <span class="math-container">$M_{\textsf{2wafa}}$</span> is
<span class="math-container">$$L(M_{\textsf{2wafa}}) = \{x \in \Sigma^* : \text{ all execution paths of $M_{\textsf{2nfa}}$ on input $x$ halt }\},$$</span>
that is, the set of inputs <span class="math-container">$x$</span> to <span class="math-container">$M_{\textsf{2nfa}}$</span> such that all execution paths of <span class="math-container">$M_{\textsf{2nfa}}$</span> on <span class="math-container">$x$</span> halt.  (An <a href="https://en.wikipedia.org/wiki/Alternating_finite_automaton" rel="nofollow noreferrer">alternating finite automata</a> has <span class="math-container">$\exists$</span>-transitions and <span class="math-container">$\forall$</span>-transitions.  Here we make every (non-deterministic) transition of <span class="math-container">$M_{\textsf{2nfa}}$</span> into a <span class="math-container">$\forall$</span>-transition in <span class="math-container">$M_{\textsf{2wafa}}$</span>, we don't use <span class="math-container">$\exists$</span>-transitions, and we make the accept states of <span class="math-container">$M_{\textsf{2wafa}}$</span> be the halting states of <span class="math-container">$M_{\textsf{2nfa}}$</span>.)</p></li>
<li><p>Convert <span class="math-container">$M_{\textsf{2wafa}}$</span> into an equivalent one-way NFA <span class="math-container">$M_{\textsf{nfa}}$</span>. (See e.g. <a href="https://doi.org/10.1007/978-3-662-44522-8_25" rel="nofollow noreferrer">here</a>.  <em><s>I assume but have not verified that this conversion is computable.</s> It appears to be computable, see the proof of Lemma 1, p. 296.)</em></p></li>
<li><p>Convert <span class="math-container">$M_{\textsf{nfa}}$</span> into an equivalent DFA <span class="math-container">$M_{\textsf{dfa}}$</span>, and check whether <span class="math-container">$L(M_{\textsf{dfa}}) = \Sigma^*$</span> (all using standard techniques). Accept if so.  <span class="math-container">$~~\Box$</span></p></li>
</ol>

CC BY-SA 4.0
2020-06-08T21:37:16.517Z
The issue of possibly unbounded run times of a 2-way NFA appears to be dealt with in a more direct way in [Complement for two-way alternating automata](https://doi.org/10.1007/s00236-020-00373-8) by 
Geffert et al.
Neal Young
CC BY-SA 4.0
2020-06-20T22:58:40.430Z
I have been keeping this tab open, for the day I'll finally have time to verify that the conversion at Stage 2 is computable myself. I couldn't do it in a short glimpse, unfortunately, and it has already been 2 weeks since you've helped me. I am accepting the answer now, but I promise to comment with my approval later on!
Utkan Gezer
CC BY-SA 4.0
2020-06-08T21:05:51.050Z
2020-06-11T11:45:01.613Z
2020-06-11T11:45:01.613Z
Neal Young
<p>A 2nfa is a nondeterministic finite automaton that can move its head left or right on the input tape, or not.  Is the following language known to be decidable?
<span class="math-container">$$
\textit{H}_{\mathsf{2nfa}} = \{ \langle M \rangle \mid M \textit{ is a } \mathsf{2nfa} \textit{ that halts on every input and on every branch} \}
$$</span></p>
<blockquote>
<h3><em>Note:</em></h3>
<p><em>This is <strong>not</strong> the same as the halting problem on 2nfa's:</em>
<span class="math-container">$$ \mathit{HALT}_{\mathsf{2nfa}} = \{ \langle M, x \rangle \mid M \textit{ is a } \mathsf{2nfa} \textit{ that halts on every branch, running on } x \} $$</span>
<em>Albeit the two are related, and as follows:</em>
<span class="math-container">$$ \langle M \rangle \in \textit{H}_{\mathsf{2nfa}} \iff \forall x, \langle M, x \rangle \in \textit{HALT}_{\mathsf{2nfa}} $$</span></p>
</blockquote>
<p>I have attempted to write an algorithm deciding <span class="math-container">$\textit{H}_{\mathsf{2nfa}}$</span>.  It looks for the sequence of transitions of <span class="math-container">$M$</span>, that start and end at the same state and the overall displacement of the head along the sequence is <span class="math-container">$0$</span>.  If there is such a loop, and some further details are satisfied, the algorithm decides that <span class="math-container">$M$</span> is not halting.</p>
<p>The problem is that I could not establish any bound on the length of the sequences to look for.  I guess that looking for sequences of length up to some function of <span class="math-container">$M$</span>'s number of states should be enough.</p>
<p>Is there perhaps another, more elegant way? Even better, a known result to refer?</p>

CC BY-SA 4.0
2020-06-08T09:07:49.380Z
The "global" state of the 2NFA on input $x$ at step $t$ is the pair $(q_t,p_t)$, where $q_t$ is the current state, and $p_t$ is head position on the input. Clearly if you don't allow the head to move off the input we have $1 \leq p_t \leq |x|$; so you must simply record every pair, if you find a repeated one then there is an infinite loop on a branch. There are at most $|Q| \times |x|$ distinct pairs. If you allow the head to move off the input, then you can consider the input $0^{|Q|} \,x\, 0^{|Q|}$ with the head at the beginning of $x$. If it moves off, then there is an infinite loop.
Marzio De Biasi
CC BY-SA 4.0
2020-06-08T10:48:39.807Z
@MarzioDeBiasi This explains that the *halting problem* on 2NFA's is decidable, right? I was asking something else; whether a 2NFA halts on every branch running on **any input x**, not a particular one. I have just added that clarification to the question. I do not see a clear reduction from my problem to the halting problem.
Utkan Gezer
CC BY-SA 4.0
2020-06-08T10:55:01.073Z
ok, is the head allowed to move "off" the input ?
Marzio De Biasi
CC BY-SA 4.0
2020-06-08T12:27:27.287Z
@MarzioDeBiasi Sorry, I had to think this through. The input is delimited with end markers on both ends. Let's say that the 2nfa pays attention to not cross those markers. (My guess is that this shouldn't matter; i.e. if the problem is decidable for 2nfa's that pay attention to stay within limits, then it would also be decidable for 2nfa's that do not pay attention.)
Utkan Gezer
<decidability><nfa>
Deciding whether a 2nfa halts on every input on every branch
Utkan Gezer
# Deciding whether a 2nfa halts on every input on every branch

(Asked by: username_0 on 2020-06-08)

A 2nfa is a nondeterministic finite automaton that can move its head left or right on the input tape, or not. Is the following language known to be decidable?
$$
\textit{H}\_{\mathsf{2nfa}} = \{ \langle M \rangle \mid M \textit{ is a } \mathsf{2nfa} \textit{ that halts on every input and on every branch} \}
$$

> ### *Note:*
>
> *This is **not** the same as the halting problem on 2nfa's:*
> $$ \mathit{HALT}\_{\mathsf{2nfa}} = \{ \langle M, x \rangle \mid M \textit{ is a } \mathsf{2nfa} \textit{ that halts on every branch, running on } x \} $$
> *Albeit the two are related, and as follows:*
> $$ \langle M \rangle \in \textit{H}\_{\mathsf{2nfa}} \iff \forall x, \langle M, x \rangle \in \textit{HALT}\_{\mathsf{2nfa}} $$

I have attempted to write an algorithm deciding $\textit{H}\_{\mathsf{2nfa}}$. It looks for the sequence of transitions of $M$, that start and end at the same state and the overall displacement of the head along the sequence is $0$. If there is such a loop, and some further details are satisfied, the algorithm decides that $M$ is not halting.

The problem is that I could not establish any bound on the length of the sequences to look for. I guess that looking for sequences of length up to some function of $M$'s number of states should be enough.

Is there perhaps another, more elegant way? Even better, a known result to refer?

**Tags:** decidability, nfa

> **Comments:**
> **username_1**: The "global" state of the 2NFA on input $x$ at step $t$ is the pair $(q_t,p_t)$, where $q_t$ is the current state, and $p_t$ is head position on the input. Clearly if you don't allow the head to move off the input we have $1 \leq p_t \leq |x|$; so you must simply record every pair, if you find a repeated one then there is an infinite loop on a branch. There are at most $|Q| \times |x|$ distinct pairs. If you allow the head to move off the input, then you can consider the input $0^{|Q|} \,x\, 0^{|Q|}$ with the head at the beginning of $x$. If it moves off, then there is an infinite loop.  
> **username_0**: @MarzioDeBiasi This explains that the *halting problem* on 2NFA's is decidable, right? I was asking something else; whether a 2NFA halts on every branch running on **any input x**, not a particular one. I have just added that clarification to the question. I do not see a clear reduction from my problem to the halting problem.  
> **username_1**: ok, is the head allowed to move "off" the input ?  
> **username_0**: @MarzioDeBiasi Sorry, I had to think this through. The input is delimited with end markers on both ends. Let's say that the 2nfa pays attention to not cross those markers. (My guess is that this shouldn't matter; i.e. if the problem is decidable for 2nfa's that pay attention to stay within limits, then it would also be decidable for 2nfa's that do not pay attention.)  

---

## 1 answers

### Answer by username_2 on 2020-06-08. Score: 3 | Accepted answer

**Lemma 1.** *$H\_{\textsf{2nfa}}$ is decidable.*

*Proof.* Decide it as follows. Given as input a two-way non-deterministic finite automaton $M\_{\textsf{2nfa}}$:

1. Convert $M\_{\textsf{2nfa}}$ into a [two-way alternating finite automaton](https://en.wikipedia.org/wiki/Two-way_finite_automaton#Two-way_alternating_finite_automaton) $M\_{\textsf{2wafa}}$ such that the language of $M\_{\textsf{2wafa}}$ is
   $$L(M\_{\textsf{2wafa}}) = \{x \in \Sigma^\* : \text{ all execution paths of $M\_{\textsf{2nfa}}$ on input $x$ halt }\},$$
   that is, the set of inputs $x$ to $M\_{\textsf{2nfa}}$ such that all execution paths of $M\_{\textsf{2nfa}}$ on $x$ halt. (An [alternating finite automata](https://en.wikipedia.org/wiki/Alternating_finite_automaton) has $\exists$-transitions and $\forall$-transitions. Here we make every (non-deterministic) transition of $M\_{\textsf{2nfa}}$ into a $\forall$-transition in $M\_{\textsf{2wafa}}$, we don't use $\exists$-transitions, and we make the accept states of $M\_{\textsf{2wafa}}$ be the halting states of $M\_{\textsf{2nfa}}$.)
2. Convert $M\_{\textsf{2wafa}}$ into an equivalent one-way NFA $M\_{\textsf{nfa}}$. (See e.g. [here](https://doi.org/10.1007/978-3-662-44522-8_25). *~~I assume but have not verified that this conversion is computable.~~ It appears to be computable, see the proof of Lemma 1, p. 296.)*
3. Convert $M\_{\textsf{nfa}}$ into an equivalent DFA $M\_{\textsf{dfa}}$, and check whether $L(M\_{\textsf{dfa}}) = \Sigma^\*$ (all using standard techniques). Accept if so. $~~\Box$

> **Comments:**
> **username_2**: The issue of possibly unbounded run times of a 2-way NFA appears to be dealt with in a more direct way in [Complement for two-way alternating automata](https://doi.org/10.1007/s00236-020-00373-8) by  Geffert et al.  
> **username_0**: I have been keeping this tab open, for the day I'll finally have time to verify that the conversion at Stage 2 is computable myself. I couldn't do it in a short glimpse, unfortunately, and it has already been 2 weeks since you've helped me. I am accepting the answer now, but I promise to comment with my approval later on!  

---

