2014 | OriginalPaper | Chapter
Synthesis and Verification of Uniform Strategies for Multi-agent Systems
Authors : Jerzy Pilecki, Marek A. Bednarczyk, Wojciech Jamroga
Published in: Computational Logic in Multi-Agent Systems
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 (
$\Delta^{\rm P}_{2}$
- 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.