A major practical obstacle is that probabilistic model-checking techniques and tools work under the assumption that all probabilities in models are known a priori. However, at early development stages, certain system quantities such as faultiness, reliability, reaction rates, packet loss ratios, etc. are often not—or at the best partially—known. In such cases, parametric probabilistic models are useful, whose transitions are labeled with arithmetic expressions over real-valued parameters. Parametric probabilistic models are challenging, e.g., the sample problem of checking whether some parameter evaluation induces a Markov chain is NP-hard. Parametric probabilistic models have been used to rank patches in software repair, in analysing adaptive software, and for model repair.

Parameter synthesis is the core problem for such models: Given a finite-state parametric Markov model, what are the parameter values for which a certain reachability property exceeds (or is below) a given threshold? This problem is well investigated for discrete-time Markov chains by leveraging state elimination from automata theory to obtain symbolic representations of reachability probabilities. The parameter synthesis problem can then be solved using SMT techniques over non-linear real arithmetic. The tool PROPhESY  supports these steps. Exact parameter synthesis techniques for continuous-time Markov chains (for timed reachability) are not known so far; this relies e.g., on the fact that the satisfiability of logics with exponentials is a long-standing open problem. For CTMCs, only approximative techniques are known. The scalability of these methods is however rather restricted. Extensions to continuous-time Markov decision processes (CTMDPs) are fully unexplored so far.

The aim of this dissertation project is to develop efficient approximate parameter synthesis technique for CTMCs, to study exact synthesis techniques for restricted classes of CTMCs (acyclic, uniform, etc.), and investigate their lifting to CTMDP. Promising directions to tackle this research challenge are to consider approximate techniques based on flow pipes and parameter lifting.

(This dissertation project is related to project AP4.)