Our Lunch Seminar series continues on Monday, April 11th! Our speaker will be Alberto Termine ( University of Milan) who will give a talk on Model Checking Stochastic Multi Agent Systems with Imprecise Probabilities.

See below for more information and the abstract:

Abstract:

Stochastic multi-agent systems raise the necessity to extend probabilistic model checking to the epistemic domain. Results in this direction have been achieved by epistemic extensions of Probabilistic Computation Tree Logic and related Probabilistic Interpreted Systems. The latter, however, require the probabilities governing the system’s behaviour to be fully specified. As a consequence, neither non-stationary stochastic systems nor systems whose stochastic behaviour is not fully knowable can be treated. Almost all approaches proposed to overcome this limitation require exponential complexity of the checking procedures in the number of states of the model. The theory of imprecise probabilities offers a natural way out. In this paper, we use it to introduce a formalism suitable to model-check multi-agent systems with either a non-stationary or not fully knowable probabilistic behaviour. To this aim, we introduce imprecise probabilistic interpreted systems and present the logical language EIPCTL to specify their properties. Later, we propose an extension of these models based on the introduction of state-rewards and introduce proper operators to specify rewards-related inferences. Finally, we present appropriate model-checking procedures for both cases.