Symbolic model-checking for resource-bounded ATL

Natasha Alechina, Brian Logan, Hoang Nga Nguyen, Franco Raimondi, Leonardo Mostarda

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review

Abstract

In this paper we present a symbolic implementation of a model checking algorithm for the verification of properties expressed in Resource-Bounded Alternating Time Temporal Logic (RB-ATL). The implementation is based on the model checker MCMAS. We evaluate the performance of our implementation using simple multi- agent model checking problems of increasing complexity.

Original languageEnglish
Title of host publicationAAMAS 2015 - Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems
EditorsRafael H. Bordini, Pinar Yolum, Edith Elkind, Gerhard Weiss
PublisherInternational Foundation for Autonomous Agents and Multiagent Systems
Pages1809-1810
Number of pages2
ISBN (Electronic)9781450337717
Publication statusPublished - 2015
Externally publishedYes
Event14th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015 - Istanbul, Turkey
Duration: 4 May 20158 May 2015

Publication series

SeriesProceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS
Volume3
ISSN1548-8403

Conference

Conference14th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015
Abbreviated titleAAMAS 2015
Country/TerritoryTurkey
CityIstanbul
Period4/05/158/05/15

Keywords

  • Model-checking
  • Resources

Fingerprint

Dive into the research topics of 'Symbolic model-checking for resource-bounded ATL'. Together they form a unique fingerprint.

Cite this