% 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{Han:51529,
author = {Han, Tingting},
othercontributors = {Katoen, Joost-Pieter},
title = {{D}iagnosis, synthesis and analysis of probabilistic
models},
volume = {2009-21},
address = {Enschede},
publisher = {Univ. Twente},
reportid = {RWTH-CONV-113814},
isbn = {978-90-365-2858-0},
series = {IPA dissertation series},
pages = {XII, 191 S. : graph. Darst.},
year = {2009},
note = {Zsfassung in engl. und dt. Sprache. - Weitere Reihe: CTIT
Ph. D. thesis series ; 09-149; Zugl.: Aachen, Techn.
Hochsch., Diss., 2009},
abstract = {This dissertation considers three important aspects of
model checking Markov models: diagnosis --- generating
counterexamples, synthesis --- providing valid parameter
values and analysis --- verifying linear real-time
properties. The three aspects are relatively independent
while all contribute to developing new theory and algorithms
in the research field of probabilistic model checking. We
start by introducing a formal definition of counterexamples
in the setting of probabilistic model checking. We transform
the problem of finding informative counterexamples to
shortest path problems. A framework is explored and provided
for generating such counterexamples. We then investigate a
more compact representation of counterexamples by regular
expressions. Heuristic based algorithms are applied to
obtain short regular expression counterexamples. In the end
of this part, we extend the definition and counterexample
generation algorithms to various combinations of
probabilistic models and logics. We move on to the problem
of synthesizing values for parametric continuous-time Markov
chains (pCTMCs) wrt. time-bounded reachability
specifications. The rates in the pCTMCs are expressed by
polynomials over reals with parameters and the main question
is to find all the parameter values (forming a synthesis
region) with which the specification is satisfied. We first
present a symbolic approach where the intersection points
are computed by solving polynomial equations and then
connected to approximate the synthesis region. An
alternative non-symbolic approach based on interval
arithmetic is investigated, where pCTMCs are instantiated.
The error bound, time complexity as well as some
experimental results have been provided, followed by a
detailed comparison of the two approaches. In the last part,
we focus on verifying CTMCs against linear real-time
properties specified by deterministic timed automata (DTAs).
The model checking problem aims at computing the probability
of the set of paths in CTMC C that can be accepted by DTA A,
denoted $Paths^C(A).$ We consider DTAs with reachability
(finite, DTAr) and Muller (infinite, DTAo) acceptance
conditions, respectively. It is shown that $Paths^C(A)$ is
measurable and computing its probability for DTAr can be
reduced to computing the reachability probability in a
piecewise deterministic Markov process PDP. The reachability
probability is characterized as the least solution of a
system of integral equations and is shown to be approximated
by solving a system of PDEs. Furthermore, we show that the
special case of single-clock DTAr can be simplified to
solving a system of linear equations. We also deal with DTAo
specifications, where the problem is proven to be reducible
to the reachability problem as in the DTAr case.},
keywords = {Model Checking (SWD) / Richtigkeit von Ergebnissen (SWD) /
Stochastischer Automat (SWD)},
cin = {121310 / 120000},
ddc = {004},
cid = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
typ = {PUB:(DE-HGF)11 / PUB:(DE-HGF)3},
urn = {urn:nbn:de:hbz:82-opus-31398},
url = {https://publications.rwth-aachen.de/record/51529},
}
guest ::