Two-way finite automaton

Definition

Let $\Sigma$ be an alphabet and let $\vdash, \dashv$ be two symbols not in $\Sigma$, the left and right end markers. A two-way deterministic finite automaton (2DFA) is a tuple $A = (Q, \Sigma, \delta, s, t, r)$ where:

1. $Q$ is a finite set of states, and $s, t, r \in Q$ are the start, accept and reject states, with $t \ne r$;
2. $\delta \colon Q \times (\Sigma \cup \set{\vdash, \dashv}) \to Q \times \set{L, R}$ is the transition function;
3. for every state $q$, $\delta(q, \vdash)$ has the form $(q', R)$ and $\delta(q, \dashv)$ has the form $(q', L)$, so the head never leaves the marked input.

On an input string $w = a_1 \cdots a_n$, the tape holds $a_0 a_1 \cdots a_n a_{n+1}$ with $a_0 = {\vdash}$ and $a_{n+1} = {\dashv}$. A configuration is a pair $(q, i)$ with $q \in Q$ and $0 \le i \le n + 1$; it starts at $(s, 0)$. If $q \notin \set{t, r}$ and $\delta(q, a_i) = (q', D)$, the next configuration is $(q', i - 1)$ when $D = L$ and $(q', i + 1)$ when $D = R$. The computation stops when it enters $t$ or $r$. The 2DFA accepts $w$ when the computation enters $t$; it rejects $w$ when it enters $r$ or never stops.