Symbolic Model Checking for One-Resource RB+-ATL / 1069

N. Alechina, B. Logan, Hoang Nga Nguyen, F. Raimondi

Research output: Chapter in Book/Report/Conference proceedingConference proceedingpeer-review

8 Citations (Scopus)


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 languageEnglish
Title of host publicationProceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)
EditorsQiang Yang, Michael Wooldridge
Place of PublicationPalo Alto
PublisherAAAI Press / International Joint Conferences on Artificial Intelligence
ISBN (Print)978-1-57735-738-4
Publication statusPublished - 2015
Externally publishedYes
EventInternational Joint Conference on Artificial Intelligence - Buenos Aires, Argentina
Duration: 25 Jul 201531 Jul 2015


ConferenceInternational Joint Conference on Artificial Intelligence
CityBuenos Aires

Bibliographical note

The full text is available from:


Dive into the research topics of 'Symbolic Model Checking for One-Resource RB+-ATL / 1069'. Together they form a unique fingerprint.

Cite this