Imprecise Probabilistic Model Checking for Stochastic Multi-agent Systems

Standard techniques for model checking stochastic multi-agent systems usually assume the transition probabilities describing the system dynamics to be stationary and completely specified. As a consequence, neither non-stationary systems nor systems whose stochastic behaviour is partially unknown can be treated. So far, most of the approaches proposed to overcome this limitation suffer from complexity issues making them poorly efficient in the case of large state spaces. A fruitful but poorly explored way out is offered by the formalism of imprecise probabilities and the related imprecise Markov models. The aim of this paper is to show how imprecise probabilities can be fruitfully involved to model-check multi-agent systems characterised by non-stationary behaviours. Specifically, the paper introduces a new class of multi-agent models called Imprecise Probabilistic Interpreted Systems and their relative extensions with rewards. It also introduces a proper logical language to specify properties of such models and corresponding model checking algorithms based on iterative procedures to compute probabilistic and epistemic inferences over imprecise Markov models.