Symbolic model checking for one-resource RB+-ATL
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, a...
| Main Authors: | , , , |
|---|---|
| Format: | Conference or Workshop Item |
| Language: | English |
| Published: |
2015
|
| Online Access: | https://eprints.nottingham.ac.uk/30173/ |
| _version_ | 1848793936235069440 |
|---|---|
| author | Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco |
| author_facet | Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco |
| author_sort | Alechina, Natasha |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T19:08:13Z |
| format | Conference or Workshop Item |
| id | nottingham-30173 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T19:08:13Z |
| publishDate | 2015 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-301732017-10-12T19:39:12Z https://eprints.nottingham.ac.uk/30173/ Symbolic model checking for one-resource RB+-ATL Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco 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. 2015-07-25 Conference or Workshop Item PeerReviewed application/pdf en https://eprints.nottingham.ac.uk/30173/1/ijcai15-symbolic-1res.pdf Alechina, Natasha, Logan, Brian, Nguyen, Hoang Nga and Raimondi, Franco (2015) Symbolic model checking for one-resource RB+-ATL. In: Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, 25-31 July 2015, Buenos Aires, Argentina. http://ijcai.org/papers15/Papers/IJCAI15-155.pdf |
| spellingShingle | Alechina, Natasha Logan, Brian Nguyen, Hoang Nga Raimondi, Franco Symbolic model checking for one-resource RB+-ATL |
| title | Symbolic model checking for one-resource RB+-ATL |
| title_full | Symbolic model checking for one-resource RB+-ATL |
| title_fullStr | Symbolic model checking for one-resource RB+-ATL |
| title_full_unstemmed | Symbolic model checking for one-resource RB+-ATL |
| title_short | Symbolic model checking for one-resource RB+-ATL |
| title_sort | symbolic model checking for one-resource rb+-atl |
| url | https://eprints.nottingham.ac.uk/30173/ https://eprints.nottingham.ac.uk/30173/ |