Skip to main content
SpringerLink
Log in
Book cover

International Conference on Interactive Theorem Proving

ITP 2016: Interactive Theorem Proving pp 151–166Cite as

Two-Way Automata in Coq

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9807))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    www.ps.uni-saarland.de/extras/itp16-2FA.

  2. 2.

    That the transitive closure of a decidable relation is decidable is established in the Ssreflect libraries using depth-first search.

References

  1. Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.): TPHOLs 2009. LNCS, vol. 5674. Springer, Heidelberg (2009)

    Google Scholar 

  2. Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer et al. [1], pp. 147–163

    Google Scholar 

  3. Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Log. Meth. Comp. Sci. 8(1:16), 1–42 (2012)

    MathSciNet  MATH  Google Scholar 

  4. Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.C.: Constructively formalizing automata theory. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, pp. 213–238. The MIT Press, Cambridge (2000)

    Google Scholar 

  5. Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 119–134. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Doczkal, C., Kaiser, J.-O., Smolka, G.: A constructive theory of regular languages in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 82–97. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  7. Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer et al. [1], pp. 327–342

    Google Scholar 

  8. Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A modular formalisation of finite group theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 86–101. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2008)

    Google Scholar 

  10. Hedberg, M.: A coherence theorem for Martin-Löf’s type theory. J. Funct. Program. 8(4), 413–436 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  11. Kozen, D.: Automata and Computability. Undergraduate Texts in Computer Science. Springer, New York (1997)

    Book  MATH  Google Scholar 

  12. Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 450–466. Springer, Heidelberg (2014)

    Google Scholar 

  13. Paulson, L.C.: A formalisation of finite automata using hereditarily finite sets. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS(LNAI), vol. 9195, pp. 231–245. Springer, Heidelberg (2015)

    Google Scholar 

  14. Pighizzini, G.: Two-way finite automata: old and recent results. Fundam. Inform. 126(2–3), 225–246 (2013)

    MathSciNet  MATH  Google Scholar 

  15. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959)

    Article  MathSciNet  MATH  Google Scholar 

  16. Sakoda, W.J., Sipser, M.: Nondeterminism and the size of two way finite automata. In: Lipton, R.J., Burkhard, W.A., Savitch, W.J., Friedman, E.P., Aho, A.V. (eds.) Proceedings of the 10th Annual ACM Symposium on Theory of Computing, pp. 275–286. ACM (1978)

    Google Scholar 

  17. Shepherdson, J.: The reduction of two-way automata to one-way automata. IBM J. Res. Develp. 3, 198–200 (1959)

    Article  MathSciNet  MATH  Google Scholar 

  18. The Coq Development Team. http://coq.inria.fr

  19. Traytel, D., Nipkow, T.: Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25, e18 (30 pages) (2015)

    Google Scholar 

  20. Vardi, M.Y.: A note on the reduction of two-way automata to one-way automata. Inf. Process. Lett. 30(5), 261–264 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  21. Vardi, M.Y.: Endmarkers can make a difference. Inf. Process. Lett. 35(3), 145–148 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  22. Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions. J. Autom. Reasoning 52(4), 451–480 (2014)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

We thank Jan-Oliver Kaiser, who was involved in our previous work on one-way automata and also in some of the early experiments with two-way automata. We also thank one of the anonymous referees for his helpful comments.

Author information

Authors and Affiliations

  1. Saarland University, Saarbrücken, Germany

    Christian Doczkal & Gert Smolka

Authors
  1. Christian Doczkal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gert Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Christian Doczkal or Gert Smolka .

Editor information

Editors and Affiliations

  1. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Jasmin Christian Blanchette

  2. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Stephan Merz

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Doczkal, C., Smolka, G. (2016). Two-Way Automata in Coq. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-43144-4_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-43143-7

  • Online ISBN: 978-3-319-43144-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation