---
title: "Symbolic Model Checking for One-Resource RB+-ATL"
authors:
  - "Natasha Alechina"
  - "Brian Logan"
  - "Nguyen Hoang Nga"
  - "Franco Raimondi"
doi: ""
url: "https://ijcai.org/proceedings/2015/155"
pdf: "https://ijcai.org/proceedings/2015/0155.pdf"
venue: "Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence"
year: 2015
pages: "1069-1074"
track: "Main Track"
keywords:
---

# Symbolic Model Checking for One-Resource RB+-ATL

Natasha Alechina, Brian Logan, Nguyen Hoang Nga, Franco Raimondi

*Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence*, pages 1069-1074.

## 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.