Publications

The paper behind MoAT, together with the tools it builds on and the tools it was evaluated against.

2026

Verifying LTL for Infinite State Systems via Termination Analysis

Nils Lommen, Moritz Leven Rosarius, and Jürgen Giesl
International Workshop on Termination, WST 2026

We show that existing tools for termination analysis are extremely well suited for LTL model checking of infinite state systems. To this end, we present a framework MoAT which uses the well-known automata-based approach and reduces the LTL model checking problem to fair termination. To prove or disprove fair termination, it then calls the termination tools KoAT and LoAT in the backend. 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.

Tools MoAT builds on

MoAT is a framework: the heavy lifting is done by established tools, each with its own publications and project page.

KoAT

Proves fair termination in MoAT's backend.

A tool to automatically infer complexity bounds for (probabilistic) integer programs, based on an alternating modular inference of upper runtime and size bounds for program parts.

koat.verify.rwth-aachen.de

LoAT

Disproves fair termination in MoAT's backend.

Proves non-termination and lower runtime bounds for integer programs, searching for reachable non-terminating cycles via an acceleration driven clause learning calculus.

loat-developers.github.io/LoAT

Spot

Generates the Büchi automata used by MoAT.

A library for LTL and ω-automata manipulation, producing optimized transition-based accepting Büchi automata.

spot.lre.epita.fr
MoAT

LTL model checking of infinite state systems via fair termination, using the termination tools KoAT and LoAT in the backend.