The Complexity of Verifying Strategic Abilities in Succinct Multiagent Systems

This paper studies the complexity of model checking strategic abilities in multiagent systems under imperfect information, in particular systems represented succinctly. Such a representation can describe systems that are exponentially larger than their input and is particularly relevant to practical implementations of model checkers such as MCMAS. The logics we consider include epistemic strategy logic supporting partial binding $SL{K}_P$, and its syntactic fragments: epistemic strategy logic $SLK$ and variants of Alternating Time Temporal logics. We show that succinct model checking for $SL{K}_P$ and $SLK$ is $AEXP(poly)$-complete, while objective ATL and ATL${}^{\ast }$ are $P^{NEXP}$-complete. The latter corrects a previous NEXP-completeness result for model checking succinct imperfect-information systems. Under subjective semantics, $P^{NEXP}$-completeness already holds for one-step Coalition Logic, and therefore also for ATL and ATL${}^{\ast }$.