A twoway finite automaton is a tuple
$M=(S,\varSigma,\delta,q_0,F)$
of a finite nonempty set of states $S$, a finite nonempty input alphabet $\varSigma$, a designated start state
$q_0\in S$, a set of designated accepting states $F\subseteq S$, and a transition function $\delta$ which
associates
pairs from $S\times(\varSigma\cup\{{\vdash},{\dashv}\})$
with pairs in $S\times\{{\scriptstyle\text L},{\scriptstyle\text R}\}$,
where $\vdash$ and $\dashv$ are two special endmarking symbols, and $\scriptstyle\text L$
and $\scriptstyle\text R$ denote the left and right directions on the tape. We assume that no pair of the
form $(\,\cdot\,,{\vdash})$ is associated with a pair of the form $(\,\cdot\,,{\scriptstyle\text L})$, and that a
pair of the form $(\,\cdot\,,{\dashv})$ is associated with a pair of the form $(q,{\scriptstyle\text R})$ only
if $q\in F$.
An input $w\in\varSigma^\ast$ is presented on the tape surrounded by the endmarkers, as ${\vdash}\,w\,{\dashv}$. The
computation starts with the control at state $q_0$ and with the head positioned on $\vdash$. At every step, the
possibilities for the next state and position are derived from the $\delta$associations of the current state and symbol. In
the resulting computation tree, each branch can eventually either continue forever, and we call it looping; or reach
a state and a symbol with no possible next state and position, and we call it hanging; or fall off $\dashv$
into an accepting state, and we call it accepting. (By our assumptions for the behavior of $\delta$ on the
endmarkers, we know that no other possibility exists.)
