2014 | OriginalPaper | Buchkapitel
Synthesis and Verification of Uniform Strategies for Multi-agent Systems
verfasst von : Jerzy Pilecki, Marek A. Bednarczyk, Wojciech Jamroga
Erschienen in: Computational Logic in Multi-Agent Systems
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.