AAAI Publications, Twenty-First International Joint Conference on Artificial Intelligence

Font Size: 
A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic
Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu

Last modified: 2009-06-25


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.


Model checking; symmetry reduction; epistemic logic

Full Text: PDF