Conference Paper/Proceeding/Abstract 609 views
Symbolic model-checking for single resource RB+-ATL
Natasha Alechina,
Brian Logan,
Hoang Nguyen 
,
Franco Raimondi
,
Franco Raimondi
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)
Swansea University Author:
Hoang Nguyen
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,...
| 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 |