Change search
ReferencesLink to record
Permanent link

Direct link
A symmetry reduction technique for model checking temporal epistemic logic
Univ London Imperial Coll Sci Technol & Med.ORCID iD: 0000-0001-5432-6442
2009 (English)In: 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, 721-726 p.Conference paper (Refereed)
Abstract [en]

We introduce a symmetry reduction technique for model checking temporal-epistemic properties of multi-agent systems defined in the mainstream interpreted systems framework. The technique, based on counterpart semantics, aims to reduce the set of initial states that need to be considered in a model. We present theoretical results establishing that there are neither false positives nor false negatives in the reduced model. We evaluate the technique by presenting the results of an implementation tested against two well known applications of epistemic logic, the muddy children and the dining cryptographers. The experimental results obtained confirm that the reduction in model checking time can be dramatic, thereby allowing for the verification of hitherto intractable systems.

Place, publisher, year, edition, pages
2009. 721-726 p.
Keyword [en]
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-62958DOI: 10.1007/978-3-642-04761-9ISI: 000283727900113ScopusID: 2-s2.0-78650517677OAI: diva2:481426
21st Internation Joint Conference on Artifical Intelligence (IJCAI-09), Pasadena, CA, JUL 11-17, 2009
QC 20120207Available from: 2012-01-20 Created: 2012-01-20 Last updated: 2012-02-07Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Dam, Mads
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 11 hits
ReferencesLink to record
Permanent link

Direct link