License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.21
URN: urn:nbn:de:0030-drops-105282
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10528/
Go to the corresponding LIPIcs Volume Portal

Geser, Alfons ; Hofbauer, Dieter ; Waldmann, Johannes

Sparse Tiling Through Overlap Closures for Termination of String Rewriting

pdf-format:
LIPIcs-FSCD-2019-21.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{geser_et_al:LIPIcs:2019:10528,
  author =	{Alfons Geser and Dieter Hofbauer and Johannes Waldmann},
  title =	{{Sparse Tiling Through Overlap Closures for Termination of String Rewriting}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10528},
  URN =		{urn:nbn:de:0030-drops-105282},
  doi =		{10.4230/LIPIcs.FSCD.2019.21},
  annote =	{Keywords: relative termination, semantic labeling, locally testable language, overlap closure}
}

Keywords: relative termination, semantic labeling, locally testable language, overlap closure
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI