Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Abstraction in Model Checking Multi-agent Systems
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.ORCID iD: 0000-0001-5432-6442
2009 (English)In: AAMAS '09 Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, Association for Computing Machinery (ACM), 2009, Vol. 1, 710-717 p.Conference paper, Published paper (Refereed)
Abstract [en]

We present an abstraction technique for multi-agent, systems preserving temporal-epistcrnic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2009. Vol. 1, 710-717 p.
Series
ACM International Joint Conference on Autonomous Agents and Multiagent Systems. Proceedings, ISSN 1548-8403
Keyword [en]
Abstraction, Epistemic logic, Model checking
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-62959Scopus ID: 2-s2.0-84899803198ISBN: 978-161567334-6 (print)OAI: oai:DiVA.org:kth-62959DiVA: diva2:481429
Conference
AAMAS '09, the 8th International Conference on Autonomous Agents and Multiagent Systems. Budapest, Hungary. May 10-15, 2009
Note

QC 20120507

Available from: 2012-01-20 Created: 2012-01-20 Last updated: 2015-04-20Bibliographically approved

Open Access in DiVA

No full text

Scopus

Authority records BETA

Dam, Mads

Search in DiVA

By author/editor
Dam, Mads
By organisation
Theoretical Computer Science, TCSACCESS Linnaeus Centre
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 47 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf