No Cover Image

Conference Paper/Proceeding/Abstract 505 views

Symbolic model-checking for single resource RB+-ATL

Natasha Alechina, Brian Logan, Hoang Nguyen Orcid Logo, Franco Raimondi

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)

Swansea University Author: Hoang Nguyen Orcid Logo

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

Full description

Published in: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)
Published: 2015
Online Access: http://ijcai.org/Proceedings/15/Papers/155.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa61992
Tags: Add Tag
No Tags, Be the first to tag this record!
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.
Item Description: http://ijcai.org/Proceedings/15/Papers/155.pdf
College: Faculty of Science and Engineering