Document Open Access Logo

Sparse Tiling Through Overlap Closures for Termination of String Rewriting

Authors Alfons Geser, Dieter Hofbauer, Johannes Waldmann

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.21.pdf
  • Filesize: 0.61 MB
  • 21 pages

Document Identifiers

Author Details

Alfons Geser
  • HTWK Leipzig, Germany
Dieter Hofbauer
  • ASW - Berufsakademie Saarland, Germany
Johannes Waldmann
  • HTWK Leipzig, Germany

Cite AsGet BibTex

Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Sparse Tiling Through Overlap Closures for Termination of String Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.21

Abstract

A strictly locally testable language is characterized by its set of admissible factors, prefixes and suffixes, called tiles. We over-approximate reachability sets in string rewriting by languages defined by sparse sets of tiles, containing only those that are reachable in derivations. Using the partial algebra defined by a tiling for semantic labeling, we obtain a transformational method for proving local termination. These algebras can be represented efficiently as finite automata of a certain shape. Using a known result on forward closures, and a new characterisation of overlap closures, we can automatically prove termination and relative termination, respectively. We report on experiments showing the strength of the method.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • relative termination
  • semantic labeling
  • locally testable language
  • overlap closure

Metrics

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

References

  1. Ronald V. Book and Friedrich Otto. String-rewriting systems. Texts and Monographs in Computer Science. Springer, New York, 1993. Google Scholar
  2. Nachum Dershowitz. Termination of Linear Rewriting Systems. In Shimon Even and Oded Kariv, editors, Automata, Languages and Programming, 8th Colloquium, Acre (Akko), Israel, July 13-17, 1981, Proceedings, volume 115 of LNCS, pages 448-458. Springer, 1981. URL: http://dx.doi.org/10.1007/3-540-10843-2_36.
  3. Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann. Local Termination: theory and practice. Logical Methods in Computer Science, 6(3), 2010. URL: http://arxiv.org/abs/1006.4955.
  4. Bertram Felgenhauer and René Thiemann. Reachability, confluence, and termination analysis with state-compatible automata. Inf. Comput., 253:467-483, 2017. URL: http://dx.doi.org/10.1016/j.ic.2016.06.011.
  5. Thomas Genet. Decidable Approximations of Sets of Descendants and Sets of Normal Forms. In Tobias Nipkow, editor, Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings, volume 1379 of LNCS, pages 151-165. Springer, 1998. URL: http://dx.doi.org/10.1007/BFb0052368.
  6. Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Match-Bounded String Rewriting Systems. Appl. Algebra Eng. Commun. Comput., 15(3-4):149-171, 2004. URL: http://dx.doi.org/10.1007/s00200-004-0162-8.
  7. Alfons Geser and Hans Zantema. Non-looping string rewriting. ITA, 33(3):279-302, 1999. URL: http://dx.doi.org/10.1051/ita:1999118.
  8. Dora Giammaresi and Antonio Restivo. Two-Dimensional Languages. In Arto Salomaa and Grzegorz Rozenberg, editors, Handbook of Formal Languages, volume 3, pages 215-267. Springer, 1997. Google Scholar
  9. Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reasoning, 58(1):3-31, 2017. URL: http://dx.doi.org/10.1007/s10817-016-9388-y.
  10. John V. Guttag, Deepak Kapur, and David R. Musser. On Proving Uniform Termination and Restricted Termination of Rewriting Systems. SIAM J. Comput., 12(1):189-214, 1983. URL: http://dx.doi.org/10.1137/0212012.
  11. Miki Hermann. Divergence des systèmes de réécriture et schématisation des ensembles infinis de termes. Habilitation, Université de Nancy, France, March 1994. Google Scholar
  12. Dieter Hofbauer. System description: MultumNonMulta. In A. Middeldorp and R. Thiemann, editors, 15th Intl. Workshop on Termination, WST 2016, Obergurgl, Austria, 2016, Proceedings, page 90, 2016. Google Scholar
  13. Dieter Hofbauer. MultumNonMulta at TermComp 2018. In S. Lucas, editor, 16th Intl. Workshop on Termination, WST 2016, Oxford, U. K., 2018, Proceedings, page 80, 2018. Google Scholar
  14. Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool 2. In Ralf Treinen, editor, Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, volume 5595 of LNCS, pages 295-304. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02348-4_21.
  15. Dallas S. Lankford and D. R. Musser. A finite termination criterion. Technical report, Information Sciences Institute, Univ. of Southern California, Marina-del-Rey, CA, 1978. Google Scholar
  16. Robert McNaughton and Seymour Papert. Counter-Free Automata. MIT Press, 1971. Google Scholar
  17. Aart Middeldorp, Hitoshi Ohsaki, and Hans Zantema. Transforming Termination by Self-Labelling. In Michael A. McRobbie and John K. Slaney, editors, Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, volume 1104 of LNCS, pages 373-387. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-61511-3_101.
  18. Jacques Sakarovitch. Éléments the théorie des automates. Vuibert Informatique, 2003. Google Scholar
  19. Christian Sternagel and Aart Middeldorp. Root-Labeling. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of LNCS, pages 336-350. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70590-1_23.
  20. Christian Sternagel and René Thiemann. Modular and Certified Semantic Labeling and Unlabeling. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs, pages 329-344. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2011.329.
  21. Vincent van Oostrom. Bowls and Beans. CWI puzzle, http://www.phil.uu.nl/~oostrom/publication/misc.html, accessible via https://web.archive.org/, 2004.
  22. Johannes Waldmann. Efficient Completion of Weighted Automata. In Andrea Corradini and Hans Zantema, editors, Proceedings 9th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2016, Eindhoven, The Netherlands, April 8, 2016., volume 225 of EPTCS, pages 55-62, 2016. URL: http://dx.doi.org/10.4204/EPTCS.225.8.
  23. Yechezkel Zalcstein. Locally testable languages. Journal of Computer and System Sciences, 6(2):151-167, 1972. URL: http://dx.doi.org/10.1016/S0022-0000(72)80020-5.
  24. Hans Zantema. Termination of Term Rewriting by Semantic Labelling. Fundam. Inform., 24(1/2):89-105, 1995. URL: http://dx.doi.org/10.3233/FI-1995-24124.
  25. Hans Zantema. Termination. In Terese, editor, Term Rewriting Systems, pages 181-259. Cambrigde Univ. Press, 2003. Google Scholar
  26. Hans Zantema. Termination of String Rewriting Proved Automatically. J. Autom. Reasoning, 34(2):105-139, 2005. URL: http://dx.doi.org/10.1007/s10817-005-6545-0.
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 Imprint Privacy Contact