Fast Parametric Model Checking

We present a technique for reducing the complexity of parametric model checking (PMC) by automatically decomposing parametric discrete-time Markov chains (pDTMCs) into fragments that can be analysed independently, yielding results that we combine to obtain the solution of the original PMC verification problem. Our fast parametric model checking (fPMC) technique enables the formal analysis of reliability, performance and other nonfunctional properties of software systems modelled by pDTMCs that are too complex to be handled by existing PMC methods. Furthermore, for many pDTMCs that state-of-the-art parametric model checkers can analyse, fPMC produces solutions (i.e., algebraic formulae) that are simpler and much faster to evaluate. We show experimentally that adding fPMC to the existing repertoire of PMC methods improves the efficiency of parametric model checking significantly, and extends its applicability to systems with more complex behaviour than currently possible.