Abstract
This dissertation considers three important aspects of model checking Markov models:
diagnosis — generating counterexamples, synthesis — providing valid parameter
values and analysis — verifying linear realtime 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 continuoustime
Markov chains (pCTMCs) wrt. timebounded 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 nonsymbolic 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 realtime 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 PathsC(A). We consider DTAs with reachability (finite, DTA♦)
and Muller (infinite, DTAω) acceptance conditions, respectively. It is shown that
PathsC(A) is measurable and computing its probability for DTA♦ 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 singleclock DTA♦ can be simplified to
solving a system of linear equations. We also deal with DTAω specifications, where the
problem is proven to be reducible to the reachability problem as in the DTA♦ case.
Original language  Undefined 

Awarding Institution 

Supervisors/Advisors 

Thesis sponsors  
Award date  25 Sep 2009 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9789036528580 
DOIs  
Publication status  Published  25 Sep 2009 
Keywords
 METIS264048
 EWI16108
 FMTPM: PROBABILISTIC METHODS
 FMTMC: MODEL CHECKING
 IR67415
Cite this
Han, T. (2009). Diagnosis, Synthesis and Analysis of Probabilistic Models. Enschede: University of Twente. https://doi.org/10.3990/1.9789036528580