Symbolic model checking for one-resource RB±ATL

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