Web Services and Interoperability for the Maude Termination Tool

This paper presents the Maude Termination Tool (MTT) version 1.5. MTT takes Maude programs as inputs and tries to prove them terminating by applying different transformation techniques and by using existing termination tools as back-ends. MTT can use as back-end tool any termination tool supporting the TPDB syntax, either locally if it follows the rules for the Termination Competition, or remotely as web services. This allows us to interact with the different tools in a uniform way, and not restricting ourselves to a specific set of tools. Thus, tools that have participated in the competition, like AProVE, MU-TERM, TTT, etc., or others that accommodate to the syntax and form of interaction, can be used as back-ends of MTT. In the MTT environment, Maude specifications can be proved terminating by using (any of these) distinct formal tools, allowing the user to choose the most appropriate one for each particular case, a combination of them, or trying different alternatives in the case of a particular tool cannot find a proof.