Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications

File Description SizeFormat 
AAAI15-CLM.pdfAccepted version320.21 kBAdobe PDFDownload
Title: Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications
Author(s): Lomuscio, AR
Cermak, P
Murano, A
Item Type: Conference Paper
Abstract: © Copyright 2015, Association for the Advancement of Artificial Intelligence (www.aaa1.org). All rights reserved.Strategy Logic (SL) has recently come to the fore as a useful specification language to reason about multi-agent systems. Its one-goal fragment, or SL[1g], is of particular interest as it strictly subsumes widely used logics such as ATL∗, while maintaining attractive complexity features. In this paper we put forward an automata-based methodology for verifying and synthesising multi-agent systems against specifications given in SL[Ig], We show that the algorithm is sound and optimal from a computational point of view. A key feature of the approach is that all data structures and operations on them can be performed on BDDs. We report on a BDD-based model checker implementing the algorithm and evaluate its performance on the fair process scheduler synthesis.
Publication Date: 31-Dec-2015
Date of Acceptance: 10-Jan-2015
URI: http://hdl.handle.net/10044/1/26816
Publisher: AAAI Press
Start Page: 2038
End Page: 2044
Conference Name: Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15)
Copyright Statement: © 2015, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
Publication Status: Published
Publisher URL: http://www.aaai.org/Press/Proceedings/iaai15.php
Start Date: 2015-01-25
Finish Date: 2015-01-30
Conference Place: Austin, Texas
Appears in Collections:Faculty of Engineering
Computing



Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons