Skip to main content

Research Repository

Advanced Search

Symbolic model checking for one-resource RB+-ATL

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

Authors

Natasha Alechina

Brian Logan

Hoang Nga Nguyen

Franco Raimondi



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
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 http://eprints.nottingham.ac.uk/id/eprint/30173
Publisher URL http://ijcai.org/papers15/Papers/IJCAI15-155.pdf
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf
Additional Information ISBN 9781577357384 (six-volume set)

Files

ijcai15-symbolic-1res.pdf (324 Kb)
PDF

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





You might also like



Downloadable Citations