Sparse Tiling through Overlap Closures for Termination of String Rewriting

03/03/2020
by   Alfons Geser, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset