Automatic Verification of Knowledge and Time with NuSMV
Proceedings of the Twentieth International Joint Conference on Artificial Intelligence. Pages 1384-1388.
Abstract
We show that the problem of model checking multi-dimensional modal logics can be reduced to the problem of model checking ARCTL, an extension of the temporal logic CTL with action labels and operators to reason about actions. In particular, we introduce a methodology for model checking a temporal-epistemic logic by building upon an extension of the model checker NuSMV that enables the verification of ARCTL. We briefly present the implementation and report experimental results for the verification of a typical security protocol involving temporal-epistemic properties: the protocol of the dining cryptographers.
@inproceedings{ijcai2007p223,
title = {Automatic Verification of Knowledge and Time with NuSMV},
author = {Lomuscio, Alessio and Pecheur, Charles and Raimondi, Franco},
booktitle = {Proceedings of the Twentieth International Joint Conference on
Artificial Intelligence, {IJCAI-07}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Ramon López de Mántaras},
pages = {1384--1388},
year = {2007},
url = {https://ijcai.org/proceedings/2007/223},
}
TY - CPAPER TI - Automatic Verification of Knowledge and Time with NuSMV AU - Lomuscio, Alessio AU - Pecheur, Charles AU - Raimondi, Franco T2 - Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, IJCAI-07 PB - International Joint Conferences on Artificial Intelligence PY - 2007 SP - 1384 EP - 1388 UR - https://ijcai.org/proceedings/2007/223 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
