Diagnosis, synthesis and analysis of probabilistic models

Han, Tingting; Katoen, Joost-Pieter

doi:3139

Diagnosis, synthesis and analysis of probabilistic models = Diagnose, Synthese und Analyse probabilistischer Modelle

Han, Tingting (Author)

2009

Verantwortlichkeitsangabevorgelegt von Tingting Han

ImpressumEnschede : Univ. Twente 2009

UmfangXII, 191 S. : graph. Darst.

ISBN978-90-365-2858-0

ReiheIPA dissertation series ; 2009-21

Zugl.: Aachen, Techn. Hochsch., Diss., 2009

Zsfassung in engl. und dt. Sprache. - Weitere Reihe: CTIT Ph. D. thesis series ; 09-149

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2009-10-16

Online
URN: urn:nbn:de:hbz:82-opus-31398
URL: https://publications.rwth-aachen.de/record/51529/files/Han_Tingting.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Model Checking (Genormte SW) ; Richtigkeit von Ergebnissen (Genormte SW) ; Stochastischer Automat (Genormte SW) ; counterexamples (frei) ; linear real-time properties (frei) ; parameter synthesis (frei) ; probabilistic model checking (frei) ; verification (frei) ; Verifikation (frei) ; Informatik (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
In dieser Dissertation werden drei wichtige Aspekte bei der Modellüberprüfung von Markov-Modellen betrachtet: Die Diagnose --- das Generieren von Gegenbeispielen, die Synthese --- das zur Verfügung stellen korrekter Parameterwerte und die Analyse --- das Verifizieren von linearen Realzeiteigenschaften. Die drei Aspekte sind vergleichsweise unabhängig, obwohl sie alle dem Zweck dienen, neue Theorie und Algorithmen für das Forschungsfeld der probabilistischen Modellüberprüfung zu entwickeln. Zu Beginn führen wir eine formale Definition von Gegenbeispielen im Bereich der probabilistische Modellüberprüfung ein. Wir transformieren das Problem, informative Gegenbeispiele zu finden, auf das Shortest-Path Problem. Es wird ein Framework untersucht und entwickelt um solche Gegenbeispiele zu erzeugen. Weiterhin untersuchen wir eine kompaktere Darstellung von Gegenbeispielen durch reguläre Ausdrücke. Algorithmen, die auf Heuristiken basieren, werden genutzt, um kurze reguläre Ausdruüke als Gegenbeispiele zu erhalten. Am Ende dieses Teils erweitern wir die Definition und die Algorithmen zum Generieren von Gegenbeispielen auf verschiedene Kombinationen von probabilistischen Modellen und Logiken. Danach betrachten wir das Problem, Werte für parametrisierte zeitkontinuierliche Markovketten (pCTMCs) bezüglich zeitbeschränkter Erreichbarkeitseigenschaften zu synthetisieren. Das Ziel hierbei ist es, alle Werte für die Ratenparameter (die eine Syntheseregion bilden) zu finden, die die Spezifikation erfüllen können; hierbei sind die Ratenausdrücke Polynome über den reellen Zahlen. Zuerst stellen wir einen symbolischen Ansatz vor, in dem zunächst die Schnittpunkte durch das Lösen von Polynomgleichungen berechnet und dann miteinander verbunden werden, um die Syntheseregion zu approximieren. Ein anderer, nicht symbolischer Ansatz, der auf Intervallarithmetik beruht und für den pCTMCs instanziiert werden, wird ebenfalls untersucht. Die Fehlerschranke, die Zeitkomplexität sowie einige experimentelle Resultate werden dargestellt, gefolgt von einem detaillierten Vergleich der beiden Ansätze. Im letzten Abschnitt steht das Verifizieren von linearen Realzeiteigenschaften auf CTMCs im Vordergrund, wobei die Eigenschaften als deterministische Zeitautomaten (DTA) gegeben sind. Das Modellüberprüfungsproblem zielt darauf ab, die Wahrscheinlichkeit der Menge aller Pfade einer CTMC C, die von einem DTA A akzeptiert werden, zu bestimmen. Wir betrachten DTAs mit Erreichbarkeits- (endliche, DTAr) und Muller- (unendliche, DTAo) Akzeptanzbedingungen. Es wird gezeigt, dass Paths^C(A) messbar ist und dass die Berechnung dieser Wahrscheinlichkeit im Falle von DTAr auf die Berechnung der Erreichbarkeitswahrscheinlichkeit in einem Piecewise Deterministic Markov Process (PDP) reduziert werden kann. Die Erreichbarkeitswahrscheinlichkeit wird charakterisiert als die kleinste Lösung eines Systems von Integralgleichungen und es wird gezeigt, dass sie durch Lösen eines Systems von PDEs approximiert werden kann. Weiterhin zeigen wir, dass der Spezialfall eines DTAr, der auf eine Uhrenvariable beschränkt ist, zu einem linearen Gleichungssystem vereinfacht werden kann. Zusätzlich betrachten wir DTAo Spezifikationen und zeigen, dass das Problem hier wie im Fall von DTAr auf das Erreichbarkeitsproblem reduziert werden kann.

This dissertation considers three important aspects of model checking Markov models: diagnosis --- generating counterexamples, synthesis --- providing valid parameter values and analysis --- verifying linear real-time properties. The three aspects are relatively independent while all contribute to developing new theory and algorithms in the research field of probabilistic model checking. We start by introducing a formal definition of counterexamples in the setting of probabilistic model checking. We transform the problem of finding informative counterexamples to shortest path problems. A framework is explored and provided for generating such counterexamples. We then investigate a more compact representation of counterexamples by regular expressions. Heuristic based algorithms are applied to obtain short regular expression counterexamples. In the end of this part, we extend the definition and counterexample generation algorithms to various combinations of probabilistic models and logics. We move on to the problem of synthesizing values for parametric continuous-time Markov chains (pCTMCs) wrt. time-bounded reachability specifications. The rates in the pCTMCs are expressed by polynomials over reals with parameters and the main question is to find all the parameter values (forming a synthesis region) with which the specification is satisfied. We first present a symbolic approach where the intersection points are computed by solving polynomial equations and then connected to approximate the synthesis region. An alternative non-symbolic approach based on interval arithmetic is investigated, where pCTMCs are instantiated. The error bound, time complexity as well as some experimental results have been provided, followed by a detailed comparison of the two approaches. In the last part, we focus on verifying CTMCs against linear real-time properties specified by deterministic timed automata (DTAs). The model checking problem aims at computing the probability of the set of paths in CTMC C that can be accepted by DTA A, denoted Paths^C(A). We consider DTAs with reachability (finite, DTAr) and Muller (infinite, DTAo) acceptance conditions, respectively. It is shown that Paths^C(A) is measurable and computing its probability for DTAr can be reduced to computing the reachability probability in a piecewise deterministic Markov process PDP. The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of PDEs. Furthermore, we show that the special case of single-clock DTAr can be simplified to solving a system of linear equations. We also deal with DTAo specifications, where the problem is proven to be reducible to the reachability problem as in the DTAr case.

Fulltext:
PDF