A two-way $k$-head automaton over a vocabulary $L$ has a finite set of control states with an initial state and accepting states, a finite family of tests, each a quantifier-free formula over $L \cup \{\le\}$ in the $k$ head positions, and a transition table: for each state and each outcome of the tests, a finite list of transitions, each a new state together with one move per head. A move leaves the head where it is, sends it to the least or to the greatest element, to the position of another head, or to the immediate successor or predecessor of the position of another head; the last two are disabled at the ends of the order. There is no work tape.

On a linearly ordered $L$-structure $A$, a configuration is a state and a $k$-tuple of elements; a step applies one of the transitions listed for the current state and the truth values of the tests at the current positions. The automaton accepts $A$ when a configuration in an accepting state is reachable from an initial configuration, in the initial state with every head on the least element. It is deterministic when every entry of its transition table lists at most one transition.