A symmetry reduction technique for model checking temporal epistemic logic
2009 (English)In: 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, 721-726 p.Conference paper (Refereed)
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.
DINING CRYPTOGRAPHERS, KNOWLEDGE
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-62958DOI: 10.1007/978-3-642-04761-9ISI: 000283727900113ScopusID: 2-s2.0-78650517677OAI: oai:DiVA.org:kth-62958DiVA: diva2:481426
21st Internation Joint Conference on Artifical Intelligence (IJCAI-09), Pasadena, CA, JUL 11-17, 2009
QC 201202072012-01-202012-01-202012-02-07Bibliographically approved