Bibliography | Gaiser, 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-Schema | D.2.4 (Software Engineering Software/Program Verification) F.3.1 (Specifying and Verifying and Reasoning about Programs) G.2.2 (Discrete Mathematics Graph Theory)
|
Keywords | Model 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 |
Contact | gaiseras@studi.informatik.uni-stuttgart.de |
Department(s) | University of Stuttgart, Institute of Formal Methods in Computer Science, Software Reliability and Security
|
Entry date | November 18, 2007 |
---|