% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@PHDTHESIS{Mereacre:82778,
author = {Mereacre, Alexandru},
othercontributors = {Katoen, Joost-Pieter},
title = {{V}erification of continuous space stochastic systems},
address = {Aachen},
publisher = {Publikationsserver der RWTH Aachen University},
reportid = {RWTH-CONV-143142},
pages = {X, 125 S. : graph. Darst.},
year = {2012},
note = {Zsfassung in engl. und dt. Sprache; Aachen, Techn.
Hochsch., Diss., 2012},
abstract = {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.},
keywords = {Markov-Entscheidungsprozess (SWD) / Ergodische Kette (SWD)
/ Unendlicher Zustandsraum (SWD) / Model Checking (SWD)},
cin = {120000 / 121420},
ddc = {004},
cid = {$I:(DE-82)120000_20140620$ / $I:(DE-82)121420_20140620$},
typ = {PUB:(DE-HGF)11},
urn = {urn:nbn:de:hbz:82-opus-42041},
url = {https://publications.rwth-aachen.de/record/82778},
}
guest ::