Monotonicity in parametric Markov chains
In several kinds of systems probabilistic behaviour occurs. For instance unreliable or unpredictable behaviour in computer networks can be seen as probabilistic behaviour. Also, in a communication protocols, messages might not be received with a given probability, this yields a probabilistic state change.
Research has been done on formal methods for the specification and verification of probabilistic systems. Questions like “what is the probability that the file is transferred correctly if messages are lost with a probability 0.05” could be analyzed through formal methods. One way to describe these probabilistic systems is through Markov chains. In a subset of these Markov chains all state changes are probabilistic and in discrete-time.
However, the probabilities of these state changes are not always known in advance. Therefore, parametric Markov chains have been developed. They allow you to use parameters in the probabilities. For instance when you have a biochemical reaction network, the rates of reactions might not be exactly known. In the past, they were then estimated. However, parametric Markov chains allow you to analyse them more precisely. Also in the case of transferring a file, the probability that a message is lost might not be known in advance. Instead of estimating this probability, we can now- based on the parametric Markov chain and a requirement, for instance "the probability that the file is transferred correctly should be at least 99%" - obtain parameter values for which the requirement holds.
I want to investigate the effect of changing these parameter values on the probability that a requirement holds. In particular, parameters might have a monotone effect on the probability that a given system state is reached. I want to find this monotonicity in parameters and exploit this to improve the analysis on the behaviour of systems. I started with this during my Master's thesis, in which I provided a framework to determine monotonicity based on the probabilistic program describing a system.