Partially Ordered Two-way B\"uchi Automata

TL;DR

This paper introduces partially ordered two-way B"uchi automata, characterizes their expressive power in relation to FO<>, and explores their determinism, closure properties, and computational complexity.

Contribution

It defines a new automaton model, establishes its expressive equivalences with FO<>, and analyzes its closure properties and complexity results.

Findings

Deterministic partially ordered two-way B"uchi automata are complete for FO<>.

They are effectively closed under Boolean operations.

The emptiness and inclusion problems are coNP-complete.

Abstract

We introduce partially ordered two-way B\"uchi automata and characterize their expressive power in terms of fragments of first-order logic FO[<]. Partially ordered two-way B\"uchi automata are B\"uchi automata which can change the direction in which the input is processed with the constraint that whenever a state is left, it is never re-entered again. Nondeterministic partially ordered two-way B\"uchi automata coincide with the first-order fragment Sigma2. Our main contribution is that deterministic partially ordered two-way B\"uchi automata are expressively complete for the first-order fragment Delta2. As an intermediate step, we show that deterministic partially ordered two-way B\"uchi automata are effectively closed under Boolean operations. A small model property yields coNP-completeness of the emptiness problem and the inclusion problem for deterministic partially ordered two-way B\"uchi automata.