Logo des Repositoriums
 

Zertifikate und Zeugen im Probabilistischen Model Checking

dc.contributor.authorJantsch, Simon
dc.contributor.editorReischuk, Rüdiger
dc.date.accessioned2023-11-09T13:38:06Z
dc.date.available2023-11-09T13:38:06Z
dc.date.issued2023
dc.description.abstractModel 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.de
dc.identifier.isbn978-3-88579-981-8
dc.identifier.urihttps://dl.gi.de/handle/20.500.12116/42587
dc.language.isode
dc.publisherGesellschaft für Informatik e.V.
dc.relation.ispartofAusgezeichnete Informatikdissertationen 2022 (Band D23)
dc.titleZertifikate und Zeugen im Probabilistischen Model Checkingde
dc.typeText/Conference Paper
gi.citation.endPage120
gi.citation.publisherPlaceBonn
gi.citation.startPage111
gi.conference.date14.-17.05.2023
gi.conference.locationSchloss Dagstuhl, Deutschland

Dateien

Originalbündel
1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
Jantsch-Simon.pdf
Größe:
962.55 KB
Format:
Adobe Portable Document Format