Publication details

Saarland University Computer Science

Two-Way Automata in Coq

Christian Doczkal, Gert Smolka

Interactive Theorem Proving (ITP 2016), Vol. 9807 of LNCS, pp. 151-166, 2016

We formally verify translations from two-way automata to one-way automata based on results from the literature. Following Vardi, we obtain a simple reduction from nondeterministic two-way automata to one-way automata that leads to a doubly-exponential increase in the number of states. By adapting the work of Shepherdson and Vardi, we obtain a singly-exponential translation from nondeterministic two-way automata to DFAs. The translation employs a constructive variant of the Myhill-Nerode theorem. Shepherdson's original bound for the translation from deterministic two-way automata to DFAs is obtained as a corollary. The development is formalized in Coq/Ssreflect without axioms and makes extensive use of countable and finite types.

Coq Development

Download PDF        Show BibTeX        Download slides (PDF)       


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009