Reachability analysis over term rewriting systems

DOI10.1007/s10817-004-6246-0zbMath1075.68038OpenAlexW2088129830MaRDI QIDQ556686

Thomas Genet, Valérie Viet Triem Tong, Guillaume Feuillade

Publication date: 22 June 2005

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00071609/file/RR-4970.pdf

zbMATH Keywords

reachability analysisterm rewritingtree automatoncompletion algorithmTimbuk

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42)

Related Items (20)

Unnamed Item ⋮ Controlled Term Rewriting ⋮ Descendants of a recognizable tree language for prefix constrained linear monadic term rewriting with position cutting strategy ⋮ Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies ⋮ Descendants of a recognizable tree language for sets of linear monadic term rewrite rules ⋮ On tree automata that certify termination of left-linear term rewriting systems ⋮ Unnamed Item ⋮ Some decidability results on one-pass reductions ⋮ One-variable context-free hedge automata ⋮ Symbol different term rewrite systems ⋮ Reachability, confluence, and termination analysis with state-compatible automata ⋮ A theoretical limit for safety verification techniques with regular fix-point computations ⋮ Equational approximations for tree automata completion ⋮ Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives ⋮ A note on partially ordered tree automata ⋮ Termination criteria for tree automata completion ⋮ TAGED Approximations for Temporal Properties Model-Checking ⋮ Handling Left-Quadratic Rules When Completing Tree Automata ⋮ Towards an Efficient Implementation of Tree Automata Completion ⋮ Term orderings for non-reachability of (conditional) rewriting

Uses Software

• Isabelle/HOL
• ELAN
• Timbuk
• OCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On sufficient-completeness and related properties of term rewriting systems
• Deterministic tree pushdown automata and monadic tree rewriting systems
• Linear generalized semi-monadic rewrite systems effectively preserve recognizability
• Bottom-up tree pushdown automata: Classification and connection with rewrite systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Reachability Analysis of Term Rewriting Systems with Timbuk
• Term Rewriting and All That
• Reachability in Conditional Term Rewriting Systems
• Tree generating regular systems

This page was built for publication: Reachability analysis over term rewriting systems