User: Guest  Login
Original title:
Verification of Discrete- and Continuous-Time Non-Deterministic Markovian Systems
Translated title:
Verifikation von non-deterministischen Markovischen Systemen mit diskreter oder kontinuierlicher Zeit
Author:
Kretinsky, Jan
Year:
2013
Document type:
Dissertation
Faculty/School:
Fakultät für Informatik
Advisor:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.)
Referee:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.); Katoen, Joost-Pieter (Prof. Dr.)
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik
Keywords:
verification, Markov decision processes, linear temporal logic, continuous time, assume-guarantee reasoning, compositional verification
Controlled terms:
Markov-Entscheidungsprozess; Markov-Kette mit stetiger Zeit; Verifikation
TUM classification:
DAT 325d; MAT 607d
Abstract:
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...     »
Translated abstract:
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...     »
WWW:
https://mediatum.ub.tum.de/?id=1166641
Date of submission:
10.07.2013
Oral examination:
28.11.2013
File size:
2230120 bytes
Pages:
208
Urn (citeable URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20131128-1166641-0-1
Last change:
07.10.2015
 BibTeX