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.
|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|
|Publication status||Published - 2015|
|Event||International Joint Conference on Artificial Intelligence - Buenos Aires, Argentina|
Duration: 25 Jul 2015 → 31 Jul 2015
|Conference||International Joint Conference on Artificial Intelligence|
|Period||25/07/15 → 31/07/15|
Bibliographical noteThe full text is available from: http://ijcai.org/Proceedings/15/Papers/155.pdf
Alechina, N., Logan, B., Nguyen, H. N., & Raimondi, F. (2015). Symbolic Model Checking for One-Resource RB+-ATL / 1069. In Q. Yang, & M. Wooldridge (Eds.), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) (pp. 1069-1075). Palo Alto: AAAI Press / International Joint Conferences on Artificial Intelligence.