MTT: The Maude Termination Tool

Authors

Francisco Durán, Salvador Lucas and José Meseguer

Abstract

In this paper we describe MTT, a tool for automatically proving termination of Maude programs. It makes use of a transformational methodology which makes possible that advanced Maude features like conditional rules and equations, sorts, subsorts, memberships, reasoning modulo axioms like associativity and commutativity, programmable strategies for controlling the execution, and so on, are transformed into proofs of termination of context-sensitive (unconditional) term rewriting systems whose termination can be analyzed by means of already available tools. Another interesting aspect of MTT, which is not usual in termination tools, is its ability to integrate as 'plug-ins' other subsidiary tools which can be used as servers of termination proofs (e.g., termination of context-sensitive rewriting). In this way, termination proofs returned by these subsidiary tools fill in the remaining proof obligations of the termination proof for the original Maude program. The TPDB format is used as an intermediate language to specify proof obligations regarding termination problems which should be solved by the external tool (e.g., AProVE, CiME, MU-TERM, ...). Also, the tool can be easily integrated as part of a formal tool environment for the verification of Maude programs, so that other Maude tools (for example the inductive theorem prover, the Church-Rosser checker, and the sufficient complenteness checker) can use the termination proofs for other analysis, verification or certification purposes.

Keywords

Maude, program analysis, rewriting logic, termination.