| Reasoning about Term Rewriting in Kleene Categories with Converse (2008) | |||||||||||||||
Abstract | |||||||||||||||
| 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. In our framework, we can analyze some properties of term rewriting systems by computing rewrite descendants of tree languages. As an application, we consider an infinite state model-checking problem given by a term rewriting system and an LTL formula. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||