On tree automata that certify termination of left-linear term rewriting systems

DOI10.1016/J.IC.2006.08.007zbMATH Open1112.68077OpenAlexW2111433946MaRDI QIDQ876043FDOQ876043

Authors: Alfons Geser, Dieter Hofbauer, Johannes Waldmann, Hans Zantema 

Publication date: 16 April 2007

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2006.08.007

Recommendations

• Term Rewriting and Applications
• Max/Plus tree automata for termination of term rewriting
• Match-bounds revisited
• Implementation and Application of Automata
• FINDING FINITE AUTOMATA THAT CERTIFY TERMINATION OF STRING REWRITING SYSTEMS

zbMATH Keywords

tree automataterm rewriting systemsterminationforward closuresrewrite labellings

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Termination of context-sensitive rewriting
• Reachability analysis over term rewriting systems
• Term Rewriting and Applications
• Deleting string rewriting systems preserve regularity
• Decidability for left-linear growing term rewriting systems.
• Title not available (Why is that?)
• Term Rewriting and Applications
• Match-bounded string rewriting systems
• Termination of string rewriting proved automatically
• FINDING FINITE AUTOMATA THAT CERTIFY TERMINATION OF STRING REWRITING SYSTEMS
• Approximations for strategies and termination

Cited In (20)

• Match-bounds revisited
• Increasing Interpretations
• Automatic Termination
• FINDING FINITE AUTOMATA THAT CERTIFY TERMINATION OF STRING REWRITING SYSTEMS
• Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
• Beyond Dependency Graphs
• Complexity of conditional term rewriting
• Term Rewriting and Applications
• Proving non-termination by finite automata
• Joint spectral radius theory for automated complexity analysis of rewrite systems
• A dependency pair framework for innermost complexity analysis of term rewrite systems
• Proving Quadratic Derivational Complexities Using Context Dependent Interpretations
• Max/Plus tree automata for termination of term rewriting
• Analyzing innermost runtime complexity of term rewriting by dependency pairs
• Increasing interpretations
• Symbol different term rewrite systems
• Automated Complexity Analysis Based on the Dependency Pair Method
• From Outermost Termination to Innermost Termination
• Title not available (Why is that?)
• Reachability, confluence, and termination analysis with state-compatible automata

Uses Software

• Timbuk
• Chaff
• Tyrolean
• AProVE
• CiME
• TPDB
• Matchbox
• TORPA

This page was built for publication: On tree automata that certify termination of left-linear term rewriting systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q876043)