MoAT

Existing tools for termination analysis are extremely well suited for LTL model checking of infinite state systems. MoAT (Model Checking Analysis Tool) is a framework which builds on this observation: it uses the well-known automata-based approach and reduces the LTL model checking problem to fair termination.

Linear temporal logic is widely used to express properties of software — local or global invariants, but also properties like termination. While there is a wealth of work on deciding LTL properties for finite state systems, the abstraction step from general programs to finite state systems naturally results in a loss of precision. MoAT therefore targets infinite state systems directly, modeled as integer transition systems (ITSs).

To decide the resulting fair termination problem, MoAT calls the termination tools KoAT and LoAT in the backend. While fair termination is undecidable in general, MoAT benefits from integrating these tools, which can often prove or refute the property for a wide range of practical programs.

Our experiments show that in this way, MoAT is on par with existing state-of-the-art tools for LTL model checking of infinite state systems. This demonstrates that state-of-the-art tools for termination analysis are also very suitable for applications in other areas.