2026-07-21T20:32:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10528 2024-03-06T10:46:08Z ddc:004 open_access

Sparse Tiling Through Overlap Closures for Termination of String Rewriting Geser, Alfons Hofbauer, Dieter Waldmann, Johannes relative termination semantic labeling locally testable language overlap closure 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alfons Geser and Dieter Hofbauer and Johannes Waldmann 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.21 urn:nbn:de:0030-drops-105282 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.21 eng https://creativecommons.org/licenses/by/3.0/legalcode