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 state of an interactive Markov chain within a given time bound.     «

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...     »

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, dass ein gegebene Zustand innerhalb gegebener Zeit erreicht ist annähert.      «

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...     »