h1

TY  - THES
AU  - Mereacre, Alexandru
TI  - Verification of continuous space stochastic systems
CY  - Aachen
PB  - Publikationsserver der RWTH Aachen University
M1  - RWTH-CONV-143142
SP  - X, 125 S. : graph. Darst.
PY  - 2012
N1  - Zsfassung in engl. und dt. Sprache
N1  - Aachen, Techn. Hochsch., Diss., 2012
AB  - 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.
KW  - Markov-Entscheidungsprozess (SWD)
KW  - Ergodische Kette (SWD)
KW  - Unendlicher Zustandsraum (SWD)
KW  - Model Checking (SWD)
LB  - PUB:(DE-HGF)11
UR  - https://publications.rwth-aachen.de/record/82778
ER  -