Verifying LTL for Infinite State Systems via Termination Analysis

arXiv (Cornell University)

Abstract

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.

Authors 3

1. Nils Lommen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

2. Moritz Leven Rosarius
3. Jürgen Giesl Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany