Efficient symbolic and explicit model checking approaches have been developed for the verification of linear time temporal logic (LTL) properties. Nowadays, several attempts have been made to combine on-the-fly search with symbolic encoding. Model checking LTL properties usually pose two challenges: one must compute the product between the state space of the system and the automaton model of the desired property, then look for counterexamples that is reduced to searching for fair loops or strongly connected components (SCCs) in state space of the product. In case of concurrent systems, the so-called saturation algorithm proved to be an efficient symbolic state space generation approach.
This thesis proposes a new approach that leverages the saturation algorithm both as an iteration strategy used to compute the product directly, as well as in a new incremental fixed-point computation algorithm to compute strongly connected components on-the-fly. Complementing the search for SCCs, explicit techniques and abstraction will be used to prove the absence of counterexamples. The result is an on-the-fly, incremental LTL model checking algorithm that proved to scale well with the size of models, as evaluation on models of the Model Checking Contest suggests.