Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-79328
URL: http://www.freidok.uni-freiburg.de/volltexte/7932/


Wimmer, Ralf

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

Symbolic methods for probabilistic verification

Dokument1.pdf (2.598 KB) (md5sum: 420803c160d4957f1553818d50285f7b)

Kurzfassung in Deutsch

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 expliziten Methoden handhaben kann.


Kurzfassung in Englisch

Discrete- and continuous-time Markov chains as well as interactive Markov chains are widely used model classes for the analysis of stochastic systems. A fundamental problem thereby is the number of states, which in general grows exponentially in the size of the corresponding high-level model.

In this work we develop two methods to cope with this problem. The first one consists of the computation of a system with a minimal number of states and the same observable behavior as the original system. This allows us to carry out any analysis with well-known algorithms on the minimal system. Depending on the definition of observability we obtain different minimal systems. Our algorithm is able to handle a large number system types and minimization criteria which are considered practically relevant in the literature. Our method works with symbolic data structures and dedicated operations thereon whose runtime only depends on the size of the representation instead of the size of the represented system. The size of the symbolic representation of many real-world systems, however, is smaller by orders of magnitudes than the system itself. Experimental results prove the efficiency of our algorithm.

The other method to handle large state spaces is to develop algorithms which are directly applicable to large systems. For the refutation of safety properties in digital circuits a method called Bounded Model Checking has been developed, which is nowadays successfully applied also in industry. We show how Bounded Model Checking can be adapted to compute counterexamples for discrete-time Markov chains if a given safety property is violated. By a number of optimization technique we can reduce not only the runtime but also the size of the counterexamples. The result is a method which is able to handle significantly larger systems than the previously available algorithms.


SWD-Schlagwörter: Bisimulation , Markov-Kette , Binäres Entscheidungsdiagramm , OBDD , Gegenbeispiel , Bounded Model Checking
Freie Schlagwörter (englisch): Markov chains , bisimulation minimization , counterexamples , binary decision diagrams, bounded model checking
CCS Klassifikation G.3 F.3.1
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Erstgutachter: Becker, Bernd (Prof. Dr.)
Sprache: Deutsch
Tag der mündlichen Prüfung: 18.01.2011
Erstellungsjahr: 2011
Publikationsdatum: 25.01.2011
Indexliste