Equational Tree Automata: Towards Automated Verification of Network Protocols ⋆ (2008)
Hitoshi Ohsaki, Toshinori Takai
Abstract. An extension of tree automata framework, called equational tree automata, is presented. This theory is useful to deal with unification modulo equational rewriting. In the manuscript, we...
Reasoning about Term Rewriting in Kleene Categories with Converse (2008)
Toshinori Takai, Hitoshi Furusawa, Wolfram Kahl, Toshinori Takai, Hitoshi Furusawa, Wolfram Kahl
Abstract. This paper shows that “root-only ” rewrite relations with respect to term rewriting systems can be expressed using Kleene star operations in a gs-monoidal Kleene category with converse....
A Tree Automata Theory for Unification Modulo Equational Rewriting (2007)
Hitoshi Ohsaki, Toshinori Takai
Abstract. An extension of tree automata framework, called equational tree automata, is presented. This theory is useful to deal with unification modulo equational rewriting. In the manuscript, we...
Layered transducing term rewriting system and its recognizability preserving property (2003)
Takai, Toshinori, Seki, Hiroyuki, Fujinaka, Youhei, Kaji, Yuichi
Recognizing boolean closed A-tree languages with membership conditional mechanism (2003)
Hitoshi Ohsaki, Hiroyuki Seki, Toshinori Takai
Abstract. This paper provides an algorithm to compute the complement of tree languages recognizable with A-TA (tree automata with associativity axioms [16]). Due to this closure property together...
A decidable subclass of term rewriting systems which effectively preserve recognizability (2002)
http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=60902
Decidability and closure properties of equational tree languages (2002)
Hitoshi Ohsaki, Toshinori Takai
Abstract. Equational tree automata provide a powerful tree language framework that facilitates to recognize congruence closures of tree languages. In the paper we show the emptiness problem for...
Layered transducing term rewriting system and its recognizability preserving property (2000)
Toshinori Takai, Hiroyuki Seki, Youhei Fujinaka, Yuichi Kaji
A term rewriting system which effectively preserves recognizability (EPR-TRS) has good mathematical properties. In this paper, a new subclass of TRSs, layered transducing TRSs (LT-TRSs) is defined...
Takai, Toshinori, Kaji, Yuichi, Seki, Hiroyuki
The authors have proposed a procedure for solving an order-sorted unification problem in an equational theory which is defined by a confluent TRS. The procedure requires an instance of the problem to...
Solving an Order-Sorted Unification Problem Using Tree Automata (1998)
http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=20628
A Decidable Subclass of Term Rewriting Systems Which Effectively Preserve Recognizability
Takai, Toshinori, 高井, 利憲, タカイ, トシノリ
奈良先端科学技術大学院大学情報科学研究科博士論文、NAIST-IS-DT9861012、2002年2月5日
A Decidable Subclass of Term Rewriting Systems Which Effectively Preserve Recognizability
Takai, Toshinori, 高井, 利憲, タカイ, トシノリ
奈良先端科学技術大学院大学情報科学研究科博士論文、NAIST-IS-DT9861012、2002年2月5日