Fuer explizites und auf Buechiautomatne basierendes LTL-Model-Checking werden Algorithmen eingesetzt, die akzeptierende Zyklen im Produktautomat des Systems und des Buechiautomaten der Negation einer LTL-Formel suchen. Es werden mehrere Algorithmen untersucht und implementiert, die Model Checking on-the-fly unterstuetzen. Die Algorithmen lassen sich in zwei Klassen einteilen, auf verschachtelter Tiefensuche basierende und solche, deren Funktionsprinzip auf dem Finden von starken Zusammenhangskomponenten beruht. Die Algorithmen werden mithilfe von Testmodellen u.a. in Bezug auf Geschwindigkeit und Speicherverbrauch verglichen, und es werden strukturelle Eigenschaften der Produktautomaten aufgezeigt, die für die unterschiedliche Performanz der Algorithmen verantwortlich sind.