Decision Method of Reachability based on Rewrite Rule Overlapping

• SHIMANUKI Kentaro

  Graduate School of Information Sciences, Tohoku University presently with Hitachi Solutions East Japan, Ltd.

• AOTO Takahito

  Faculty of Engineering, Niigata University

• TOYAMA Yoshihito

  RIEC, Tohoku University

Bibliographic Information

Other Title

• 書き換え規則の重なりに基づく到達可能性判定法

Abstract

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.

Journal

• Computer Software

  Computer Software 33 (3), 3_93-3_107, 2016

  Japan Society for Software Science and Technology

Details

• CRID: 1390282679713526912
• NII Article ID: 130005256734
• DOI: 10.11309/jssst.33.3_93
• ISSN: 02896540
• Text Lang: ja
• Data Source:
  • JaLC
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed