Symbolic model checking for one-resource RB+-ATL

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

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

Citation

Alechina, N., Logan, B., Nguyen, H. N., & Raimondi, F. (2015). Symbolic model checking for one-resource RB+-ATL.

• Conference Name: Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015
• Conference Location: Buenos Aires, Argentina
• Start Date: Jul 25, 2015
• End Date: Jul 31, 2015
• Acceptance Date: Jul 25, 2015
• Publication Date: Jul 25, 2015
• Deposit Date: Sep 18, 2015
• Publicly Available Date: Sep 18, 2015
• Peer Reviewed: Peer Reviewed
• ISBN: 978-1-57735-738-4
• Public URL: https://nottingham-repository.worktribe.com/output/756281
• Publisher URL: http://ijcai.org/papers15/Papers/IJCAI15-155.pdf
• Additional Information: ISBN 9781577357384 (six-volume set)