MTT
5 Benchmarks
The diagram with the transformations (on the right) is key for understanding the transformations being used.
Terminating problems are in green, non-terminating ones in red, and problem whose termination cannot be proof in orange.
The timeout is set to 10 minutes for all the proofs.
The benchmark includes functional modules (MEL theories, like MTT-BOOL, MTT-NAT, MTT-LIST, etc.) and system modules (RW theories, like JOSEPHUS, BLACKBOARD, DIE-HARD, etc.), some are context sensitive (LAZY-LIST-UTILITIES and LAZY-NAT-LIST), others have A (JOSEPHUS-GENERALIZED) or AC (BLACKBOARD, MTT-MAP, DATA-AGENTS, and DINING-PHILOSOPHERS) operators, and some are non-terminating (INF and DIE-HARD).
In most cases, there are several alternative valid transformations. We give here some of them just for illustrating purposes.
![[check the technical report for the available transformations]](TransfTerminationRWL.jpg "Available transformation diagram. Details available at [...].")