Sparse Tiling through Overlap Closures for Termination of String Rewriting
Logic in Computer Science
2020-03-04 v1
Abstract
We over-approximate reachability sets in string rewriting by languages defined by admissible factors, called tiles. A sparse set of tiles contains only those that are reachable in derivations, and is constructed by completing an automaton. Using the partial algebra defined by a sparse tiling for semantic labelling, we obtain a transformational method for proving local termination. With a known result on forward closures, and a new characterisation of overlap closures, we obtain methods for proving termination and relative termination, respectively. We report on experiments showing the strength of these methods.
Cite
@article{arxiv.2003.01696,
title = {Sparse Tiling through Overlap Closures for Termination of String Rewriting},
author = {Alfons Geser and Dieter Hofbauer and Johannes Waldmann},
journal= {arXiv preprint arXiv:2003.01696},
year = {2020}
}