Counterexamples in probabilistic verification

Jansen, Nils; Ábrahám, Erika; Becker, Bernd; Katoen, Joost-Pieter

doi:urn:nbn:de:hbz:82-rwth-2015-033184

Counterexamples in probabilistic verification = Gegenbeispiele in der probabilistischen Verifikation

Jansen, Nils

2015

Verantwortlichkeitsangabevorgelegt von Nils Jansen

ImpressumAachen : Publikationsserver der RWTH Aachen University 2015

UmfangXI, 224 S.S. . graph. Darst.

Aachen, Techn. Hochsch., Diss., 2015

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Ábrahám, Erika (Thesis advisor) ; Becker, Bernd (Thesis advisor) ; Katoen, Joost-Pieter (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2015-03-26

Online
URN: urn:nbn:de:hbz:82-rwth-2015-033184
URL: https://publications.rwth-aachen.de/record/479827/files/479827.pdf
URL: https://publications.rwth-aachen.de/record/479827/files/479827.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; verification (frei) ; Markov chain (frei) ; counterexample (frei) ; parameter synthesis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Das Thema dieser Doktorarbeit kann grob in die formale Verifikation probabilistischer Systeme eingeordnet werden. Genauer gesagt wird die Generierung von Gegenbeispielen für Markow-Modelle mit diskreter Zeit untersucht. Ein Gegenbeispiel für Markow-Ketten mit diskreter Zeit (DTMCs) ist ursprünglich als eine (endliche) Menge von Pfaden definiert. In dieser Arbeit repräsentieren wir diese Menge von Pfaden symbolisch durch einen kritischen Teil des originalen Systems, ein sogenanntes kritisches Teilsystem. Dieses Konzept wird erweitert auf Markow-Entscheidungsprozesse (MDPs) und probabilistische Automaten (PAs). Die Resultate werden unterteilt in vier Abschnitte vorgestellt: 1. Ein Algorithmus zur Modellüberprüfung für DTMCs basierend auf der Zerlegung des Systemgraphen in starke Zusammenhangskomponenten. Dieser Ansatz wird auf parametrische Markow-Ketten mit diskreter Zeit erweitert. 2. Die Generierung von Gegenbeispielen für DTMCs und Erreichbarkeitsbedingungen basierend auf Graphalgorithmen. Ein hierarchisches Abstraktionsschema zur Berechnung abstrakter Gegenbeispiele wird präsentiert, gefolgt von einem generellen Rahmenwerk für sowohl explizit repräsentierte Systeme als auch symbolisch repräsentierte Systeme unter Verwendung von binären Entscheidungsdiagrammen (BDDs). 3. Die Berechnung minimaler kritischer Teilsysteme unter Nutzung von Erfüllbarkeitsüberpüfung erweitert um Theorien (SMT) und gemischt ganzzahlig-linearer Optimierung (MILP). Dies wird untersucht für Erreichbarkeitsbedingungen und $\omega$-reguläre Eigenschaften für DTMCs, MDPs und PAs. 4. Ein neues Konzept für high-level Gegenbeispiele für PAs. Markow-Modelle können mit Hilfe einer probabilistischen Programmiersprache spezifiziert werden. Ein Ansatz zur Berechnung kritischer Teile solch einer symbolischen Systembeschreibung wird vorgestellt, resultierend in für Menschen lesbaren Gegenbeispielen.Alle Resultate wurden in Konferenzbänden oder Fachzeitschriften publiziert. Eine ausführliche Evaluierung anhand bekannter Benchmarks vergleicht alle Methoden untereinander und mit verfügbaren Implementierungen anderer Ansätze.

The topic of this thesis is roughly to be classified into the formal verification of probabilistic systems. In particular, the generation of counterexamples for discrete-time Markov Models is investigated. A counterexample for discrete-time Markov Chains (DTMCs) is classically defined as a (finite) set of paths. In this work, this set of paths is represented symbolically as a critical part of the original system, a so-called critical subsystem. This notion is extended to Markov decision processes (MDPs) and probabilistic automata (PAs). The results are introduced in four parts: 1. A model checking algorithm for DTMCs based on a decomposition of the system's graph in strongly connected components (SCCs). This approach is extended to parametric discrete-time Markov Chains. 2. The generation of counterexamples for DTMCs and reachability properties based on graph algorithms. A hierarchical abstraction scheme to compute abstract counterexamples is presented, followed by a general framework for both explicitly represented systems and symbolically represented systems using binary decision diagrams (BDDs). 3. The computation of minimal critical subsystems using SAT modulo theories (SMT) solving and mixed integer linear programming (MILP). This is investigated for reachability properties and $\omega$-regular properties on DTMCs, MDPs, and PAs. 4. A new concept of high-level counterexamples for PAs. Markov models can be specified by means of a probabilistic programming language. An approach for computing critical parts of such a symbolic description of a system is presented, yielding human-readable counterexamples. All results have been published in conference proceedings or journals. A thorough evaluation on common benchmarks is given comparing all methods and also competing with available implementations of other approaches.

OpenAccess:
PDF PDF (PDFA)
(additional files)