Verifying probabilistic systems : new algorithms and complexity results

Fu, Hongfei; Katoen, Joost-Pieter

doi:1999910016897

Verifying probabilistic systems : new algorithms and complexity results = Die Verifikation probabilistischer Systeme : neue Algorithmen und Komplexitätsergebnisse

Fu, Hongfei (Author)

2014

VerantwortlichkeitsangabeHongfei Fu

ImpressumAachen : RWTH, Department of Computer Science 2014

UmfangXII, 152 S.

ReiheAachener Informatik-Berichte Technical report / Department of Computer Science, RWTH Aachen ; 2014,16

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

Genehmigende Fakultät
Fak01

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

Tag der mündlichen Prüfung/Habilitation
2014-11-21

Online
URN: urn:nbn:de:hbz:82-opus-52856
URL: https://publications.rwth-aachen.de/record/465418/files/5285.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Algorithmus (Genormte SW) ; Verifikation (Genormte SW) ; probabilistic systems (frei) ; verification (frei) ; probabilistische Systeme (frei) ; Informatik (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Der Inhalt dieser Dissertation fällt in das Gebiet formaler Verifikation von probabilistischen Systemen. Die vier Bestandteile sind:1. Das Entscheidungsproblem von (probabilistischer) Simulationsquasiordnung zwischen probabilistischen Kellerautomaten (pPDAs) und endlichen probabilistischen Automaten (fPAs);2. Das Entscheidungsproblem einer Bisimulationsmetrik auf endlichen probabilistischen Automaten (fPAs);3. Das Approximationsproblem einer Akzeptanzwahrscheinlichkeit von deterministischen Zeitautomaten auf zeitkontinuierlichen Markow-Ketten (CTMCs);4. Das Approximationsproblem kostenbeschränkter Erreichbarkeitsprobleme auf zeitkontinuierlichen Markow-Entscheidungsprozessen (CTMDPs). Die ersten zwei Teile behandeln die Äquivalenzüberpruefung von probabilistischen Automaten, wobei probabilistische Automaten (PAs) analog zu zeitdiskreten Markow-Prozessen sind, welche sowohl Nichtdeterminismus als auch zeitdiskrete stochastische Transitionen besitzen. Die beiden letzten Teile behandeln numerische Algorithmen auf Markow-Sprungprozessen. In Teil 1 und 2 legen wir den Fokus auf Komplexitätsprobleme; in Teil 3 und 4 behandeln wir hauptsaechlich numerische Approximationsalgorithmen.

The content of the dissertation falls in the area of formal verification of probabilistic systems. It comprises four parts listed below:1. the decision problem of (probabilistic) simulation preorder between probabilistic pushdown automata (pPDAs) and finite probabilistic automata (fPAs);2. the decision problem of a bisimilarity metric on finite probabilistic automata (fPAs);3. the approximation problem of acceptance probability of deterministic-timed-automata (DTA) objectives on continuous-time Markov chains (CTMCs);4. the approximation problem of cost-bounded reachability probability on continuous-time Markov decision processes (CTMDPs).The first two parts are concerned with equivalence checking on probabilistic automata, where probabilistic automata (PAs) are an analogue of discrete-time Markov decision processes that involves both non-determinism anddiscrete-time stochastic transitions. The last two parts are concerned withnumerical algorithms on Markov jump processes. In Part 1 and Part 2, we mainly focus on complexity issues; as for Part 3 and Part 4, we mainly focus on numerical approximation algorithms.

Fulltext:
PDF