Some Things are Easier for the Dumb and the Bright Ones (Beware of the Average!)

Model checking strategic abilities in multi-agent systems is hard, especially for agents with partial observability of the state of the system. In that case, it ranges from NP-complete to undecidable, depending on the precise syntax and the semantic variant. That, however, is the _worst case complexity_, and the problem might as well be easier when restricted to particular subclasses of inputs. In this paper, we study some natural restrictions on models, that might lead to cheaper verification. More specifically, we look at models with “extreme” epistemic structure, arising when the agents have almost nil, or, symmetrically, almost perfect observability. A sensor observing only one variable, with a fixed number of possible values, provides a natural example of the former type. For the latter class, consider a central controller monitoring a team of robots, with only a fixed number of units being unavailable at a time. It turns out that, when we consistently pair those restrictions with the assumptions about agents’ memory (i.e., assume almost perfect observability and perfect recall, or almost nil observability and no recall), model checking can become easier than in general. This applies especially to the verification of abilities of singleton coalitions. We also show that no gain is possible for the other combinations. To prove the latter kind of results, we develop generic techniques that may be useful also outside of this study. The paper has been accepted for the 28th International Joint Conference on Artificial Intelligence IJCAI 2019. It reports joint work with Michal Knapik.

Authors

• Wojtek Jamroga.

Keywords

No keywords are indexed for this paper.