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

DOI10.1016/J.IC.2006.08.007MaRDI QIDQ876043zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

tree automataterm rewriting systemsterminationforward closuresrewrite labellings

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 3729436 (Why is no real title available?)
• scientific article; zbMATH DE number 3615891 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• Approximations for strategies and termination
• Decidability for left-linear growing term rewriting systems.
• Deleting string rewriting systems preserve regularity
• FINDING FINITE AUTOMATA THAT CERTIFY TERMINATION OF STRING REWRITING SYSTEMS
• Match-bounded string rewriting systems
• Reachability analysis over term rewriting systems
• Term Rewriting and Applications
• Term Rewriting and Applications
• Termination of context-sensitive rewriting
• Termination of string rewriting proved automatically
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(20)

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

Describes a project that uses

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)