Parameter Synthesis for Families of Markov Chains with an Application to Multi-agent Systems Privacy

Given a probabilistic system with parameters and a target specification, the parameter synthesis problem is defined as the search for actual values that can be assigned to the model parameters such that the system itself fulfills the given specification. This problem has been studied extensively in the case of (finite-state) Markov Chains. We study the parameter synthesis problem in a new formalism called families of Markov Chains (fMC), a special case of infinite Markov Chains. The latter can express Markov Chains with both discrete parameters as well as probabilistic parameters. After showing that in this setting the parameter synthesis problem is undecidable, we show a methodology that, under suitable conditions, reduces an infinite family of MCs to a single parametric MC. Then, by using standard techniques such as mixed integer linear programming (MILP), one can solve the parameter synthesis problem on the abstract parametric MC and obtain optimal parameter values for the given infinite family of MCs. In order to show the feasibility of our approach, despite the NP-hard complexity of MILP, we consider scenarios where Multi-Agent Systems needs to store sensitive information on a distributed storage.