Student Thesis STUD-2096

BibliographyGaiser, Andreas: Vergleich von Algorithmen für den Leerheitstest von Büchiautomaten.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Student Thesis No. 2096 (2007).
48 pages, german.
CR-SchemaD.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
G.2.2 (Discrete Mathematics Graph Theory)
KeywordsModel Checking; Büchiautomat; Leerheitstest; Tarjan-Algorithmus; LTL; depth-first search
Abstract

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.

Full text and
other links
PDF (669049 Bytes)
Access to students' publications restricted to the faculty due to current privacy regulations
Contactgaiseras@studi.informatik.uni-stuttgart.de
Department(s)University of Stuttgart, Institute of Formal Methods in Computer Science, Software Reliability and Security
Entry dateNovember 18, 2007
   Publ. Computer Science