Document Open Access Logo

Proving non-termination by finite automata

Authors Jörg Endrullis, Hans Zantema

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.160.pdf
  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Author Details

Jörg Endrullis
Hans Zantema

Cite As Get BibTex

Jörg Endrullis and Hans Zantema. Proving non-termination by finite automata. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 160-176, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.160

Abstract

A new technique is presented to prove non-termination of term rewriting. The basic idea is to find a non-empty regular language of terms that is closed under rewriting and does not contain normal forms. It is automated by representing the language by a tree automaton with a fixed number of states, and expressing the mentioned requirements in a SAT formula. Satisfiability of this formula implies non-termination. Our approach succeeds for many examples where all earlier techniques fail, for instance for the S-rule from combinatory logic.

Subject Classification

Keywords
  • non-termination
  • finite automata
  • regular languages

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Homepage of AProVE, 2015. URL: http://aprove.informatik.rwth-aachen.de.
  2. Homepage of TTT2, 2015. URL: http://cl-informatik.uibk.ac.at/software/ttt2/.
  3. H.P. Barendregt, J. Endrullis, J.W. Klop, and J. Waldmann. Dance of the Starlings. 2015. To be published on arXiv.org. Google Scholar
  4. H.P. Barendregt, J. Endrullis, J.W. Klop, and J. Waldmann. Songs of the Starling and the Owl. 2015. To be published on arXiv.org. Google Scholar
  5. B. Cook. Priciples of program termination. URL: http://research.microsoft.com/en-us/um/cambridge/projects/terminator/principles.pdf.
  6. N. Eén and A. Biere. Effective Preprocessing in SAT through Variable and Clause Elimination. In Proc. Conf. on Theory and Applications of Satisfiability Testing (SAT '05), volume 3569 of LNCS, pages 61-75. Springer, 2005. Google Scholar
  7. F. Emmes, T. Enger, and J. Giesl. Proving Non-looping Non-termination Automatically. In International Joint Conference on Automated Reasoning (IJCAR 2012), volume 7364 of LNCS, pages 225-240. Springer, 2012. Google Scholar
  8. J. Endrullis, R. C. de Vrijer, and J. Waldmann. Local Termination. In Proc. Conf. on Rewriting Techniques and Applications (RTA), volume 5595 of LNCS, pages 270-284. Springer, 2009. Google Scholar
  9. J. Endrullis, R.C. de Vrijer, and J. Waldmann. Local Termination: Theory and Practice. Logical Methods in Computer Science, 6(3), 2010. Google Scholar
  10. J. Endrullis, H. Geuvers, J. G. Simonsen, and H. Zantema. Levels of Undecidability in Rewriting. Information and Computation, 209(2):227-245, 2011. Google Scholar
  11. J. Endrullis, H. Geuvers, and H. Zantema. Degrees of Undecidability in Term Rewriting. In Proc. Int. Workshop on Computer Science Logic (CSL 2009), volume 5771 of LNCS, pages 255-270. Springer, 2009. Google Scholar
  12. J. Endrullis, C. Grabmayer, D. Hendriks, J.W. Klop, and R.C. de Vrijer. Proving Infinitary Normalization. In Postproc. Int. Workshop on Types for Proofs and Programs (TYPES 2008), volume 5497 of LNCS, pages 64-82. Springer, 2009. Google Scholar
  13. J. Endrullis, C. Grabmayer, J.W. Klop, and V. van Oostrom. On Equal μ-Terms. Theoretical Computer Science, 412(28):3175-3202, 2011. Google Scholar
  14. J. Endrullis, H. Hvid Hansen, D. Hendriks, A. Polonsky, and A. Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics. Schloss Dagstuhl, 2015. Google Scholar
  15. J. Endrullis and D. Hendriks. Transforming Outermost into Context-Sensitive Rewriting. Logical Methods in Computer Science, 6(2), 2010. Google Scholar
  16. J. Endrullis and D. Hendriks. Lazy Productivity via Termination. Theoretical Computer Science, 412(28):3203-3225, 2011. Google Scholar
  17. J. Endrullis, D. Hendriks, and R. Bakhshi. On the Complexity of Equivalence of Specifications of Infinite Objects. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2012), pages 153-164. ACM, 2012. Google Scholar
  18. J. Endrullis, D. Hendriks, R. Bakhshi, and G. Roşu. On the complexity of stream equality. Journal of Functional Programming, 24(2-3):166-217, 2014. Google Scholar
  19. J. Endrullis, D. Hendriks, and M. Bodin. Circular Coinduction in Coq Using Bisimulation-Up-To Techniques. In Proc. Conf. on Interactive Theorem Proving (ITP), volume 7998 of LNCS, pages 354-369. Springer, 2013. Google Scholar
  20. J. Endrullis, D. Hendriks, and J.W. Klop. Highlights in Infinitary Rewriting and Lambda Calculus. Theoretical Computer Science, 464:48-71, 2012. Google Scholar
  21. J. Endrullis, D. Hofbauer, and J. Waldmann. Decomposing Terminating Rewrite Relations. In Proc. Workshop on Termination (WST '06), pages 39-43, 2006. Google Scholar
  22. J. Endrullis and A. Polonsky. Infinitary Rewriting Coinductively. In Proc. Types for Proofs and Programs (TYPES 2012), volume 19 of Leibniz International Proceedings in Informatics, pages 16-27. Schloss Dagstuhl, 2013. Google Scholar
  23. B. Felgenhauer and R. Thiemann. Reachability Analysis with State-Compatible Automata. In LATA, volume 8370 of LNCS, pages 347-359. Springer, 2014. Google Scholar
  24. T. Genet. Decidable Approximations of Sets of Descendants and Sets of Normal Forms. In Proc. Conf. on Rewriting Techniques and Applications (RTA '98), volume 1379 of LNCS, pages 151-165. Springer, 1998. Google Scholar
  25. A. Geser, D. Hofbauer, J. Waldmann, and H. Zantema. On tree automata that certify termination of left-linear term rewriting systems. Information and Computation, 205(4):512-534, 2007. Google Scholar
  26. A. Geser and H. Zantema. Non-looping String Rewriting. RAIRO Theoretical Informatics and Applications, 33(3):279-302, 1999. Google Scholar
  27. M. Korp and A. Middeldorp. Match-bounds revisited. Information and Computation, 207(11):1259-1283, 2009. Google Scholar
  28. M. Mousazadeh, B. T. Ladani, and H. Zantema. Liveness verification in trss using tree automata and termination analysis. Computing and Informatics, 29(3):407-426, 2010. Google Scholar
  29. M. Oppelt. Automatische Erkennung von Ableitungsmustern in nichtterminierenden Wortersetzungssystemen. Technical report, HTWK Leipzig, Germany, 2008. Diploma Thesis. Google Scholar
  30. Helmut Seidl. Deciding equivalence of finite tree automata. In STACS 89, volume 349 of LNCS, pages 480-492. Springer, 1989. Google Scholar
  31. J. Waldmann. The Combinator S. Information and Computation, 159(1-2):2-21, 2000. Google Scholar
  32. J. Waldmann. Matchbox: A Tool for Match-Bounded String Rewriting. In Proc. Conf. on Rewriting Techniques and Applications (RTA '04), volume 3091 of LNCS, pages 85-94. Springer, 2004. Google Scholar
  33. J. Waldmann. Compressed loops (draft), 2012. Google Scholar
  34. H. Zankl and A. Middeldorp. Nontermination of String Rewriting using SAT, 2007. Google Scholar
  35. H. Zankl, C. Sternagel, D. Hofbauer, and A. Middeldorp. Finding and certifying loops. In Proc. Conf. on Theory and Practice of Computer Science (SOFSEM 2010), volume 5901 of LNCS, pages 755-766. Springer, 2010. Google Scholar
  36. H. Zankl, C. Sternagel, D. Hofbauer, and A. Middeldorp. Finding and certifying loops. In SOFSEM 2010: Theory and Practice of Computer Science, volume 5901 of LNCS, pages 755-766. Springer, 2010. Google Scholar
  37. H. Zantema and J. Endrullis. Proving Equality of Streams Automatically. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2011), pages 393-408, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact