Abstract
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 look at the verification of models with
“extreme” epistemic structure, and identify several
special cases for which model checking is easier
than in general. We also prove that, in the other
cases, no gain is possible even if the agents have
almost full (or almost nil) observability. To prove
the latter kind of results, we develop generic techniques that may be useful also outside of this study