We consider model checking problem of probabilistic multiagent systems with respect to a probabilistic epistemic logic, which can specify both temporal and epistemic properties. In contrast to existing work, we focus on decentralized schedulers, which are implementable and more realistic for multiagent systems. Unfortunately, the model checking problem turns to be undecidable in this setting. However, by restricting to decentralized memoryless schedulers, we present a decision algorithm and we further show that the problem is NP-hard.

Date: 07 October 2015