Symbolic Model Checking for One-Resource RB+-ATL
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. 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.
@inproceedings{ijcai2015p155,
title = {Symbolic Model Checking for One-Resource RB+-ATL},
author = {Alechina, Natasha and Logan, Brian and Nga, Nguyen Hoang and Raimondi, Franco},
booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on
Artificial Intelligence, {IJCAI-15}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Qiang Yang and Michael Wooldridge},
pages = {1069--1074},
year = {2015},
month = {7},
note = {Main Track},
url = {https://ijcai.org/proceedings/2015/155},
}
TY - CPAPER TI - Symbolic Model Checking for One-Resource RB+-ATL AU - Alechina, Natasha AU - Logan, Brian AU - Nga, Nguyen Hoang AU - Raimondi, Franco T2 - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15 PB - International Joint Conferences on Artificial Intelligence PY - 2015 SP - 1069 EP - 1074 UR - https://ijcai.org/proceedings/2015/155 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
