Symbolische Methoden für die probabilistische Verifikation – Zustandsraumreduktion und Gegenbeispiele

Abstract

Ein bekanntes Hindernis für die formale Verifikation von Systemen bildet die potentiell stark anwachsende Größe des Zustandsraums, genannt "Zustandsraumexplosion". Dieses Problem konnte für digitale Schaltungen durch den Einsatz symbolischer Methoden zufriedenstellend gelöst oder zumindest entscheidend entschärft werden. Für probabilistische Systeme, die als Markow-Kette oder Markow-Entscheidungsprozess modelliert sind, brachte die direkte Übertragung dieser symbolischen Methoden bisher keinen Durchbruch. In dieser Arbeit stellen wir zwei neue Ansätze vor, mit denen Markow-Modelle mit sehr großen Zustandsräumen verifiziert werden können. Die erste Methode ist ein symbolisches Verfahren zur Vorverarbeitung: Zu jedem Markow-Modell berechnen wir mit rein symbolischen Verfahren das kleinste Modell, das in den interessierenden Eigenschaften mit dem Original-Modell übereinstimmt. Die Verifikation kann danach auf dem minimierten Modell durchgeführt werden. Das zweite offene Problem, das in der Dissertation gelöst wird, ist die symbolische Berechnung von Gegenbeispielen, wenn Sicherheitseigenschaften von Markow-Ketten mit diskreter Zeit verletzt sind. Anhand von Experimenten wird gezeigt, dass die neu entwickelten Verfahren den bisher verfügbaren Verfahren hinsichtlich der Laufzeit bzw. der Größe der handhabbaren Systeme deutlich überlegen sind.