Abstract
RB+-ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The model-checking problem for RB+-ATL is known to be decidable. However the only available model-checking algorithm for RB+-ATL uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB+-ATL, 1RB+-ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB+-ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces.
Original language | English |
---|---|
Title of host publication | Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) |
Editors | Qiang Yang, Michael Wooldridge |
Place of Publication | Palo Alto |
Publisher | AAAI Press / International Joint Conferences on Artificial Intelligence |
Pages | 1069-1075 |
ISBN (Print) | 978-1-57735-738-4 |
Publication status | Published - 2015 |
Externally published | Yes |
Event | International Joint Conference on Artificial Intelligence - Buenos Aires, Argentina Duration: 25 Jul 2015 → 31 Jul 2015 |
Conference
Conference | International Joint Conference on Artificial Intelligence |
---|---|
Country | Argentina |
City | Buenos Aires |
Period | 25/07/15 → 31/07/15 |
Bibliographical note
The full text is available from: http://ijcai.org/Proceedings/15/Papers/155.pdfFingerprint Dive into the research topics of 'Symbolic Model Checking for One-Resource RB+-ATL / 1069'. Together they form a unique fingerprint.
Profiles
-
Hoang Nga Nguyen
- Institute for Future Transport and Cities - Assistant Professor (Research)
Person: Teaching and Research