A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic

Cohen, Mika; Dam, Mads; Lomuscio, Alessio; Qu, Hongyang

A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic

Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu

Download BibTeX Cite

Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence. Pages 721-725.

Abstract

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.Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu

Mika Cohen, Mads Dam, Alessio Lomuscio, and Hongyang Qu. 2009. A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic. In Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence, IJCAI-09. IJCAI, 721–725. https://ijcai.org/proceedings/2009/125

@inproceedings{ijcai2009p125,
  title     = {A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic},
  author    = {Cohen, Mika and Dam, Mads and Lomuscio, Alessio and Qu, Hongyang},
  booktitle = {Proceedings of the Twenty-First International Joint Conference on
               Artificial Intelligence, {IJCAI-09}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Hiroaki Kitano},
  pages     = {721--725},
  year      = {2009},
  url       = {https://ijcai.org/proceedings/2009/125},
}

TY  - CPAPER
TI  - A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic
AU  - Cohen, Mika
AU  - Dam, Mads
AU  - Lomuscio, Alessio
AU  - Qu, Hongyang
T2  - Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence, IJCAI-09
PB  - International Joint Conferences on Artificial Intelligence
PY  - 2009
SP  - 721
EP  - 725
UR  - https://ijcai.org/proceedings/2009/125
ER  -