We present a model checking algorithm for alternating-time temporal logic (ATL) with imperfect information and imperfect recall. This variant of ATL is arguably most appropriate when it comes to modeling and specification of multi-agent systems. The related variant of model checking is known to be theoretically hard (ΔP2 to PSPACE-complete, depending on the assumptions), but virtually no practical attempts at it have been proposed so far. Our algorithm searches through the set of possible uniform strategies, utilizing a simple reduction technique. In consequence, it not only verifies 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. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Pilecki, J., Bednarczyk, M. A., & Jamroga, W. (2014). Synthesis and verification of uniform strategies for multi-agent systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8624 LNAI, pp. 166–182). Springer Verlag. https://doi.org/10.1007/978-3-319-09764-0_11
Mendeley helps you to discover research relevant for your work.