@inproceedings{918e0badfaa5477789deba58ad769526,
title = "Symbolic model checking for one-resource RB±ATL",
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 modelchecking problem for RB±ATL is known to be decidable. However the only available modelchecking 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.",
author = "Natasha Alechina and Brian Logan and Nguyen, {Hoang Nga} and Franco Raimondi",
year = "2015",
language = "English",
series = "IJCAI International Joint Conference on Artificial Intelligence",
publisher = "International Joint Conferences on Artificial Intelligence",
pages = "1069--1075",
editor = "Michael Wooldridge and Qiang Yang",
booktitle = "IJCAI 2015 - Proceedings of the 24th International Joint Conference on Artificial Intelligence",
address = "United States",
note = "24th International Joint Conference on Artificial Intelligence, IJCAI 2015, IJCAI 2015 ; Conference date: 25-07-2015 Through 31-07-2015",
}