SMC: synthesis of uniform strategies and verification of strategic ability for multi-agent systems

We present a model checking algorithm for a subset of alternating-time temporal logic (ATL) with imperfect information and imperfect recall. This variant of ATL is arguably most appropriate when it comes to modelling and specification of multi-agent systems. The related variant of model checking is known to be theoretically hard (NP- to PSPACE-complete, depending on the assumptions), but very few practical attempts at it have been proposed so far. Our algorithm searches through the set of possible uniform strategies, utilizing a simple technique that reduces the search space. In consequence, it does not only verify existence of a suitable strategy but also produces one (if it exists). We validate the algorithm experimentally on a simple scalable class of models, with promising results. We also discuss two variants of the model checking problem, related to the objective vs. subjective interpretation of strategic ability. We provide algorithms for reductions between the two semantic variants of model checking. The algorithms are experimentally validated as well.