Parameter Synthesis for Continuous-Time Markov Models



Joost-Pieter Katoen



+49 241 80 21200



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, and so on are often not—or at the best partially—known. In such cases, parametric probabilistic models are useful, whose transitions are labelled with arithmetic expressions over real-valued parameters. Parametric probabilistic models are challenging, for example 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 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 given 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, such as CTMDPs, have been 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, either acyclic, uniform, and so on, and investigate their lifting to CTMDPs. Promising directions to tackle this research challenge are to consider approximate techniques based on flow and parameter lifting.