Symbolic Model Checking for One-Resource RB+-ATL / 1069

N. Alechina; B. Logan; Hoang Nga Nguyen; F. Raimondi

Symbolic Model Checking for One-Resource RB+-ATL / 1069

N. Alechina, B. Logan, Hoang Nga Nguyen, F. Raimondi

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

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.

Original language	English
Title of host publication	Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)
Editors	Qiang Yang, Michael Wooldridge
Place of Publication	Palo Alto
Publisher	AAAI Press / International Joint Conferences on Artificial Intelligence
Pages	1069-1075
ISBN (Print)	978-1-57735-738-4
Publication status	Published - 2015
Externally published	Yes
Event	International Joint Conference on Artificial Intelligence - Buenos Aires, Argentina Duration: 25 Jul 2015 → 31 Jul 2015

Conference

Conference	International Joint Conference on Artificial Intelligence
Country	Argentina
City	Buenos Aires
Period	25/07/15 → 31/07/15

Bibliographical note

The full text is available from: http://ijcai.org/Proceedings/15/Papers/155.pdf

Access to Document

http://ijcai.org/Proceedings/15/Papers/155.pdf

Fingerprint Dive into the research topics of 'Symbolic Model Checking for One-Resource RB+-ATL / 1069'. Together they form a unique fingerprint.

Hoang Nga Nguyen
- Institute for Future transport and Cities - Assistant Professor Research
Person: Teaching and Research

Cite this

Alechina, N., Logan, B., Nguyen, H. N., & Raimondi, F. (2015). Symbolic Model Checking for One-Resource RB+-ATL / 1069. In Q. Yang, & M. Wooldridge (Eds.), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) (pp. 1069-1075). AAAI Press / International Joint Conferences on Artificial Intelligence. http://ijcai.org/Proceedings/15/Papers/155.pdf

Symbolic Model Checking for One-Resource RB+-ATL / 1069. / Alechina, N.; Logan, B.; Nguyen, Hoang Nga; Raimondi, F.

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) . ed. / Qiang Yang; Michael Wooldridge. Palo Alto : AAAI Press / International Joint Conferences on Artificial Intelligence, 2015. p. 1069-1075.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

Alechina, N, Logan, B, Nguyen, HN & Raimondi, F 2015, Symbolic Model Checking for One-Resource RB+-ATL / 1069. in Q Yang & M Wooldridge (eds), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) . AAAI Press / International Joint Conferences on Artificial Intelligence, Palo Alto, pp. 1069-1075, International Joint Conference on Artificial Intelligence, Buenos Aires, Argentina, 25/07/15. <http://ijcai.org/Proceedings/15/Papers/155.pdf>

Alechina, N. ; Logan, B. ; Nguyen, Hoang Nga ; Raimondi, F. / Symbolic Model Checking for One-Resource RB+-ATL / 1069. Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015) . editor / Qiang Yang ; Michael Wooldridge. Palo Alto : AAAI Press / International Joint Conferences on Artificial Intelligence, 2015. pp. 1069-1075

@inproceedings{068181f54bcf4ea6a4bda3d35dc81e22,

title = "Symbolic Model Checking for One-Resource RB+-ATL / 1069",

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

author = "N. Alechina and B. Logan and Nguyen, {Hoang Nga} and F. Raimondi",

note = "The full text is available from: http://ijcai.org/Proceedings/15/Papers/155.pdf; International Joint Conference on Artificial Intelligence ; Conference date: 25-07-2015 Through 31-07-2015",

year = "2015",

language = "English",

isbn = "978-1-57735-738-4",

pages = "1069--1075",

editor = "Qiang Yang and Michael Wooldridge",

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

publisher = "AAAI Press / International Joint Conferences on Artificial Intelligence",

address = "United States",

}

TY - GEN

T1 - Symbolic Model Checking for One-Resource RB+-ATL / 1069

AU - Alechina, N.

AU - Logan, B.

AU - Nguyen, Hoang Nga

AU - Raimondi, F.

N1 - The full text is available from: http://ijcai.org/Proceedings/15/Papers/155.pdf

PY - 2015

Y1 - 2015

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

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

M3 - Conference proceeding

SN - 978-1-57735-738-4

SP - 1069

EP - 1075

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

A2 - Yang, Qiang

A2 - Wooldridge, Michael

PB - AAAI Press / International Joint Conferences on Artificial Intelligence

CY - Palo Alto

T2 - International Joint Conference on Artificial Intelligence

Y2 - 25 July 2015 through 31 July 2015

ER -