Benutzer: Gast  Login
Originaltitel:
Verification of Discrete- and Continuous-Time Non-Deterministic Markovian Systems 
Übersetzter Titel:
Verifikation von non-deterministischen Markovischen Systemen mit diskreter oder kontinuierlicher Zeit 
Jahr:
2013 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.) 
Gutachter:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.); Katoen, Joost-Pieter (Prof. Dr.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
verification, Markov decision processes, linear temporal logic, continuous time, assume-guarantee reasoning, compositional verification 
Schlagworte (SWD):
Markov-Entscheidungsprozess; Markov-Kette mit stetiger Zeit; Verifikation 
TU-Systematik:
DAT 325d; MAT 607d 
Kurzfassung:
This thesis deals with verification of probabilistic systems both in the setting of discrete time as well as continuous time. Firstly, we design a novel method to translate formulae of linear temporal logic to automata and show how this speeds up verification of Markov decision processes. Secondly, we provide the first compositional verification method in the continuous-time setting. We design a specification formalism and assume-guarantee algorithms to approximate probabilities to reach a given...    »
 
Übersetzte Kurzfassung:
Diese Arbeit beschäftigt sich mit Verifikation von probabilistischen Systemen sowohl in diskreter Zeit als auch in kontinuierlicher Zeit. Wir entwerfen eine neuartige Methode, um Formeln der linearen zeitlichen Logik in Automaten übersetzen, und zeigen, wie diese die Verifikation von Markov Entscheidungsprozessen beschleunigt. Wir entwerfen auch das erste kompositorische Verifikationsverfahren für kontinuierliche Zeit, namentlich ein assume-guarantee Algorithmus das die Wahrscheinlichkeiten, das...    »
 
Mündliche Prüfung:
28.11.2013 
Dateigröße:
2230120 bytes 
Seiten:
208 
Letzte Änderung:
07.10.2015