Symbolische Methoden für die probabilistische Verifikation : Zustandsraumreduktion und Gegenbeispiele ; Symbolic methods for probabilistic verification
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Doctoral Thesis;
E-Book;
Electronic Thesis
Title:
Symbolische Methoden für die probabilistische Verifikation : Zustandsraumreduktion und Gegenbeispiele ; Symbolic methods for probabilistic verification
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Markow-Ketten mit diskreter und kontinuierlicher Zeit sowie interaktive Markow-Ketten sind weitverbreitete Modellklassen zur Analyse von stochastischen Systemen. Ein grundlegendes Problem bei ihrer Analyse ist die Anzahl der Zustände. Diese wächst nämlich im Allgemeinen exponentiell in der Größe des zugehörigen Highlevel-Modells. Wir entwickeln in dieser Arbeit zwei Methoden, mit denen dieses Problem gelöst werden kann. Die erste besteht darin, zu jedem System dasjenige zu berechnen, das aus einer minimalen Anzahl von Zuständen besteht und das dasselbe beobachtbare Verhalten wie das ursprüngliche System aufweist. Danach kann die Analyse mit bekannten Algorithmen auf dem minimierten System durchgeführt werden. Abhängig von der Definition, welches Verhalten des Systems beobachtbar ist, erhalten wir verschiedene minimale Systeme. Unser Algorithmus ist in der Lage, eine ganze Reihe von Minimierungskriterien, die in der Literatur von Bedeutung sind, und Systemtypen zu berücksichtigen. Er arbeitet mit symbolischen Datenstrukturen und darauf angepassten Operationen, deren Laufzeit nur von der Größe der Darstellung abhängt. Für viele praktisch relevante Systeme ist diese um Größenordnungen kleiner als die Größe des dargestellten Systems. Experimentelle Ergebnisse belegen die Effzienz unseres Verfahrens. Die andere Methode, mit großen Zustandsräumen umzugehen, ist, symbolische Algorithmen zur Analyse zu entwickeln, die direkt auf große Systemen anwendbar sind. Für die Fehlersuche in Schaltkreisen wird eine Methode namens Bounded Model Checking verwendet, die inzwischen auch industriell sehr erfolgreich eingesetzt wird. Wir zeigen, wie Bounded Model Checking zur Berechnung von Gegenbeispielen für Markow-Ketten eingesetzt werden kann, wenn diese eine vorgegebene Sicherheitseigenschaft verletzen. Durch eine Reihe von Optimierungen gelingt es uns, sowohl die Laufzeit zu reduzieren als auch die Größe der Gegenbeispiele zu verringern. Das Resultat ist ein Verfahren, das deutlich größere Systeme als die bisher verfügbaren ...