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 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.
Cite
Text
Alechina et al. "Symbolic Model Checking for One-Resource RB+-ATL." International Joint Conference on Artificial Intelligence, 2015.Markdown
[Alechina et al. "Symbolic Model Checking for One-Resource RB+-ATL." International Joint Conference on Artificial Intelligence, 2015.](https://mlanthology.org/ijcai/2015/alechina2015ijcai-symbolic/)BibTeX
@inproceedings{alechina2015ijcai-symbolic,
title = {{Symbolic Model Checking for One-Resource RB+-ATL}},
author = {Alechina, Natasha and Logan, Brian and Nguyen, Hoang Nga and Raimondi, Franco},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2015},
pages = {1069-1075},
url = {https://mlanthology.org/ijcai/2015/alechina2015ijcai-symbolic/}
}