Two-Way Deterministic Finite Automata

Felipe Escallón 📧 and Tobias Nipkow 📧

July 29, 2025

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This theory presents a proof that two-way DFAs are as powerful as DFAs, i.e. they accept exactly the regular languages. The formalization follows Kozen.

License

BSD License

Topics

Session Two_Way_DFA_HF

Depends on

Cite

× 
@article{Two_Way_DFA_HF-AFP,
  author  = {Felipe Escallón and Tobias Nipkow},
  title   = {Two-Way Deterministic Finite Automata},
  journal = {Archive of Formal Proofs},
  month   = {July},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Two_Way_DFA_HF.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download