Tinting Han, MEng

 

Diagnosis, Synthesis and Analysis of Probabilistic Models

 

Abstract:

 

In this talk, we consider two important aspects of model checking Markov models: diagnosis --- generating counterexamples, and synthesis --- providing valid parameter values. The two aspects are relatively independent while both contribute to developing new theory and algorithms in the research field of probabilistic model checking.

In the first part, we consider counterexample generation in the setting of probabilistic model checking. To achieve this, we transform the problem of finding informative counterexamples to shortest path(s) (SP) problems in graph theory, where new SP algorithms are proposed to tackle new scenarios. We then present a more compact representation of counterexamples by regular expressions. Heuristic-based algorithms are applied to generate short regular expression counterexamples. Finally we extend the definition and counterexample generation algorithms to various combinations of probabilistic models and logics.

The second part of the presentation is concerned with 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. To this end, a symbolic approach based on a closed-from expression and a nonsymbolic approach based on interval arithmetic will be presented with the respective error bound, time complexity as well as a detailed comparison.