Abstract

Markov chains (MCs) are an excellent formalism to capture the behaviour of systems that are governed by randomized behaviour. They are used in computer science, engineering, mathematics, and biology. MCs require xed distributions, but often these probabilities are not precisely known.

Parametric MCs (pMCs) allow for changing specfii c sets of distributions in the MC. One way to find the values for parameters is parameter synthesis. Based on the pMC and the speci fication, the parameter values for which the system meets these requirements are needed to be calculated. We investigate the e ffect of changing the parameter values.

In particular, we observe that parameters often have a monotone e ffect on the probability that a given system state is reached. We want to exploit this monotone effect to improve the analysis on the behaviour of systems. To that end, we provide a formal framework to verify efficiently whether these systems are monotone. The framework consists of two layers: the foundation, and the top layer. In the foundation we de fine a set of monotone pMCs through the composition of predefi ned building blocks. In the top layer, we show that structures in high level descriptions of systems naturally map to the building blocks of the foundation.

Additional Resources

1. Thesis Jip Spel