Konferenzbeitrag
Zertifikate und Zeugen im Probabilistischen Model Checking
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Text/Conference Paper
Zusatzinformation
Datum
2023
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
Model Checking ist eine Methode der formalen Verifikation, deren Ziel es ist, vollautomatisiert zu prüfen, ob ein System eine gegebene Eigenschaft erfüllt. Zertifikate, Zeugen und Gegenbeispiele können zusätzliche, über eine reine Ja/Nein-Antwort hinausgehende, Informationen über das Ergebnis eines Model Checkers geben. Dadurch ermöglichen sie höheres Vertrauen in die Antwort von Model Checkern, und können außerdem erklären, warum eine Eigenschaft (nicht) erfüllt ist. Die vorgestellte Dissertation führt neue Methoden zur Zertifizierung und Bezeugung für die Analyse von probabilistischen Systemen ein. Insbesondere wird eine neue Klasse von Zertifikaten, genannt Farkas Zertifikate, für das probabilistische Model Checking definiert. Ein Zusammenhang zwischen diesen Zertifikaten und so gennanten bezeugenden Subsystemen wird hergestellt, welcher in neuen Algorithmen zu Berechnung von bezeugenden Subsystemen mündet. Schließlich wird gezeigt, dass die Komplexität der Berechnung von minimalen Zeugen schon für stark eingeschränkte Klassen von probabilistischen Systemen NP-vollständig ist.