Truly On-The-Fly LTL Model Checking

Moritz Hammer, Alexander Knapp, Stephan Merz

We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized Büchi automaton for the negation of the formula and the empt…