# Deciding whether a 2nfa halts on every input on every branch

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?

• 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 Jun 8 '20 at 9:07
• @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 Jun 8 '20 at 10:48
• ok, is the head allowed to move "off" the input ? – Marzio De Biasi Jun 8 '20 at 10:55
• @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 Jun 8 '20 at 12:27

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 $$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 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. 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$$