Diagnosis, Synthesis and Analysis of Probabilistic Models

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 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 single-clock 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.