Web Interface

Submit an integer transition system and an LTL formula, and let MoAT decide whether the formula holds.
Examples
seconds

Choose a property, or keep the default termination check.

Atomic propositions are polynomial inequations like 'x > 0' or locations like 'AT(l0)', always in single quotes. All operators have the same precedence and associate to the left, so parenthesise where the grouping matters. Programs are written in the ARI format.

The property to check

The order in which the formula's variables map onto the program's.

Optional constraint on the initial state.

Operators — temporal X, F, G, U, and R; boolean &&, ||, ->, <->, and NOT.

The same run locally

The web interface passes no options of its own beyond the timeout, so a local MoAT gives the same answer for the same input:

See Getting Started for what MoAT takes as input and what its answers mean.
MoAT
LTL model checking of infinite state systems via fair termination, using the termination tools KoAT and LoAT in the backend.
MoAT
Related
© 2026 MoAT
LuFG Informatik 2, RWTH Aachen University