@article{oai:nagoya.repo.nii.ac.jp:00019058,
 author = {Kojima, Yoshiharu and Sakai, Masahiko and Nishida, Naoki and Kusakari, Keiichirou and Sakabe, Toshiki},
 issue = {3},
 journal = {情報処理学会論文誌, プログラミング},
 month = {Jul},
 note = {The reachability problem for given an initial term, a goal term, and a term rewriting system (TRS) is to decide whether the initial one is reachable to the goal one by the TRS or not. A term is shallow if each variable in the term occurs at depth 0 or 1. Innermost reduction is a strategy that rewrites innermost redexes, and context-sensitive reduction is a strategy in which rewritable positions are indicated by specifying arguments of function symbols. In this paper, we show that the reachability problem under context-sensitive innermost reduction is decidable for linear right-shallow TRSs. Our approach is based on the tree automata technique that is commonly used for analysis of reachability and its related properties. We show a procedure to construct tree automata accepting the sets of terms reachable from a given term by context-sensitive innermost reduction of a given linear right-shallow TRS.},
 pages = {20--32},
 title = {Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems},
 volume = {2},
 year = {2009}
}