Robust Strategies for Stochastic Multi-Agent Systems

The precise probabilities of stochastic systems are often partially unknown and may face perturbations. Finding a strategy in this setting is difficult, as it requires dealing with uncertainty on the system transitions while interacting with other agents. In this paper, we introduce the robust model checking problem for Multi-Agent Systems, in which agents play strategies that ensure the satisfaction of a specification is satisfied, even though the system probabilities are uncertain. We consider specifications in a variant of Alternating-time Temporal Logic with bounded memory.