A symmetry reduction technique for model checking temporal-epistemic logic
File(s)
Published version
Author(s)
Cohen, Mika
Dam, Mads
Lomuscio, Alessio
Qu, Hongyang
Type
Report
Abstract
We introduce a symmetry reduction technique for model checking temporalepistemic
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.
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.
Date Issued
2009-01-01
Citation
Departmental Technical Report: 09/1, 2009, pp.1-13
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
13
Journal / Book Title
Departmental Technical Report: 09/1
Copyright Statement
© 2009 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
09/1