Two-Way Automata in Coq

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9807
• 期：1
• 页码：151-166
• 全文大小：242 KB
• 参考文献：1.Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.): TPHOLs 2009. LNCS, vol. 5674. Springer, Heidelberg (2009)
  2.Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer et al. [1], pp. 147–163
  3.Braibant, T., Pous, D.: Deciding Kleene algebras in Coq. Log. Meth. Comp. Sci. 8(1:16), 1–42 (2012)MathSciNet MATH
  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)
  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)CrossRef
  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)CrossRef
  7.Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer et al. [1], pp. 327–342
  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)CrossRef
  9.Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2008)
  10.Hedberg, M.: A coherence theorem for Martin-Löf’s type theory. J. Funct. Program. 8(4), 413–436 (1998)MathSciNet CrossRef MATH
  11.Kozen, D.: Automata and Computability. Undergraduate Texts in Computer Science. Springer, New York (1997)CrossRef MATH
  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)
  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)
  14.Pighizzini, G.: Two-way finite automata: old and recent results. Fundam. Inform. 126(2–3), 225–246 (2013)MathSciNet MATH
  15.Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959)MathSciNet CrossRef MATH
  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)
  17.Shepherdson, J.: The reduction of two-way automata to one-way automata. IBM J. Res. Develp. 3, 198–200 (1959)MathSciNet CrossRef MATH
  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)
  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)MathSciNet CrossRef MATH
  21.Vardi, M.Y.: Endmarkers can make a difference. Inf. Process. Lett. 35(3), 145–148 (1990)MathSciNet CrossRef MATH
  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)MathSciNet CrossRef MATH
  
• 作者单位：Christian Doczkal (15)
  Gert Smolka (15)
  
  15. Saarland University, Saarbrücken, Germany
  
• 丛书名：Interactive Theorem Proving
• ISBN：978-3-319-43144-4
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9807

文摘

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.