Decision method of reachability based on rewrite rule overlapping

Kentaro Shimanuki, Takahito Aoto, Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review


Tree automata completion is a popular method for reachability analysis over term rewriting systems, which has many applications such as confluence analysis and normalizing strategy analysis. The point of this method is to ensure termination of the completion procedure, and it is known that the completion procedure terminates for the classes of growing term rewriting systems and finite path overlapping term rewriting systems. In this paper, we propose a new class of term rewriting systems, named non-left-right-overlapping term rewriting systems, which is incompatible with the classes of growing systems and finite path overlapping systems. Analyzing the overlapping relation between the left-hand side and the right-hand side of the rewrite rules, we give a sufficient condition for termination of the tree automata completion procedure for non-left-right-overlapping term rewriting systems. The reachability problem is decidable for the class of term rewriting systems satisfying this sufficient condition.

Original languageEnglish
Pages (from-to)93-107
Number of pages15
JournalComputer Software
Issue number3
Publication statusPublished - 2016 Jan 1

ASJC Scopus subject areas

  • Software

Cite this