Verification of continuous space stochastic systems

Mereacre, Alexandru; Katoen, Joost-Pieter

doi:urn:nbn:de:hbz:82-opus-42041

Verification of continuous space stochastic systems = Verifikation von stochastischen Systemen des kontinuierlichen Raums

Mereacre, Alexandru (Author)

2012

Verantwortlichkeitsangabevorgelegt von Alexandru Mereacre

ImpressumAachen : Publikationsserver der RWTH Aachen University 2012

UmfangX, 125 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2012

Zsfassung in engl. und dt. Sprache

Genehmigende Fakultät
Fak01

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

Tag der mündlichen Prüfung/Habilitation
2011-05-02

Online
URN: urn:nbn:de:hbz:82-opus-42041
URL: https://publications.rwth-aachen.de/record/82778/files/4204.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Markov-Entscheidungsprozess (Genormte SW) ; Ergodische Kette (Genormte SW) ; Unendlicher Zustandsraum (Genormte SW) ; Model Checking (Genormte SW) ; Informatik (frei) ; Markov (frei) ; stochastic (frei) ; verification (frei) ; continuous (frei) ; decision (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Diese Dissertation behandelt Verifikationsalgorithmen für inhomogene, zeit-kontinuierliche Markov-Ketten (ICTMC), zeit-diskrete stochastische hybride Systeme (DTSHS), sowie Markov'sche timed automata (MTA). Für diese drei Modelle definieren wir die Begriffe der zeit-beschränkten und -unbeschränkten Erreichbarkeit. Diese verwenden wir, um die Erfüllbarkeitswahrscheinlichkeiten von omega-regulären Eigenschaften zu berechnen. Für ICTMCs definieren wir die Begriffe der zeit-beschränkten und -unbeschränkten Erreichbarkeit als Lösung eines Systems von Integralgleichungen. Wir zeigen, dass für den beschränkten Fall die Erreichbarkeitswahrscheinlichkeiten durch Lösen eines Systems gewöhnlicher Differentialgleichungen hergeleitet werden können. Für den unbeschränkten Fall betrachten wir zwei verschieden Klassen von ICTMCs: periodische sowie uniforme. Für beide Klassen entwickeln wir effiziente Methoden basierend auf zeit-diskreten Markov-Ketten, um die unbeschränkten Erreichbarkeitswahrscheinlichkeiten zu berechnen. Die Ergebnisse im unbeschränkten Fall werden benutzt, um die Erfüllbarkeitswahrscheinlichkeiten von omega-regulären Eigenschaften zu berechnen. Schließlich führen wir die Begriffe von zeit-beschränkter und -unbeschränkter Erreichbarkeit für DTSHS ein. Wir entwickeln einen Diskretisierungsalgorithmus, der ein DTSHS in eine DTMC verwandelt und Erreichbarkeitswahrscheinlichkeiten als Lösung eines linearen Gleichungssystems berechnet. Wir berechnen auch Fehlergrenzen für den beschränkten Fall. Die Begriffe der zeit-beschränkten und -unbeschränkten Erreichbarkeit versetzen uns in der Lage, die Erfüllbarkeit einer omega-regulären Eigenschaft zu bestimmen. Alle Ergebnisse werden anhand eines Beispiels (das Beheizen zweier Räume) erläutert. Wir führen MTA als eine Erweiterung von timed automata mit exponentiellen Verteilungen ein. Wir definieren die maximalen zeit-beschränkten und -unbeschränkten Erreichbarkeitswahrscheinlichkeiten als Lösung eines Systems von Integralgleichungen ein. Für den beschränkten Fall entwickeln wir einen Diskretisierungsalgorithmus, der einen MTA in einen Markov'schen Entscheidungsprozess umwandelt. Wir berechnen Fehlerschranken. Für MTAs mit einer einzigen Uhr stellen wir ein System von linearen Gleichungen auf, dessen Lösung die zeit-unbeschränkte Erreichbarkeit beschreibt.

This thesis deals with verification algorithms for inhomogeneous continuous time Markov chains (ICTMC), discrete time stochastic hybrid systems (DTSHS) and Markovian timed automata (MTA). For all of these three models we define the notions of time-bounded and time-unbounded reachability. We use time-bounded and time-unbounded reachability in order to compute the satisfiability probability of an omega-regular property. For ICTMCs we introduce the notions of time-bounded and time-unbounded reachability as a solution of a system of integral equations. We show that for the time-bounded case the reachability probability can be computed by solving a system of ordinary differential equations. For the time-unbounded case we consider two special classes of ICTMCs: periodic and uniform. For both classes we develop efficient techniques based on discrete time Markov chains (DTMCs) in order to compute the time-unbounded reachability. Using the time-unbounded measure we can compute the satisfiability probability for an omega-regular property against an ICTMC. We introduce the notions of time-bounded and time-unbounded reachability for DTSHS. We develop a discretization algorithm, where the DTSHS is discretized into a DTMC and the resulting reachability probabilities are computed as a solution of a system of linear equations. We compute also an error bound for the time-bounded reachability case. Using the notions of time-bounded and time-unbounded reachability we are able to verify whether a DTSHS satisfies a given omega-regular property. All obtained results are applied to a two-room heating example. We introduce MTA as an extension of timed automata with exponential distributions. We define the maximum time-bounded and time-unbounded reachability probabilities as a solution of a system of integral equations. We develop a discretization algorithm for the time-bounded reachability case. We discretize the MTA into a Markov decision process and we compute an error bound. For MTAs with a single clock we introduce a system of linear equations which solves the time-unbounded rechability case.

Fulltext:
PDF