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 nza@cs.nott.ac.uk

Brian Logan bsl@cs.nott.ac.uk

Hoang Nga Nguyen hnn@cs.nott.ac.uk

Franco Raimondi f.raimondi@mdx.ac.uk



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.

Start Date Jul 25, 2015
Publication Date Jul 25, 2015
Peer Reviewed Peer Reviewed
ISBN 978-1-57735-738-4
APA6 Citation Alechina, N., Logan, B., Nguyen, H. N., & Raimondi, F. (2015). Symbolic model checking for one-resource RB+-ATL
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.nottingh.../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

;