Publications

Automatic Verification of Knowledge and Time with NuSMV

Authors
Alessio Lomuscio, Charles Pecheur, Franco Raimondi
Tags
, , , , ,
Title
Automatic Verification of Knowledge and Time with NuSMV
Authors
Alessio Lomuscio, Charles Pecheur, Franco Raimondi
FM2018 Δ   0Kb   28 May 2020
Fmics2013 Δ   0Kb   28 May 2020
GandALF2017 Δ   0Kb   28 May 2020
HMI2011 Δ   0Kb   28 May 2020
LVLPrivate Δ   0Kb   28 May 2020
LVLPrivateNews Δ   0Kb   28 May 2020
Main Δ   0Kb   28 May 2020
Members Δ   0Kb   28 May 2020
Publications Δ   4Kb   28 May 2020
Site Δ   0Kb   28 May 2020
Talks Δ   4Kb   28 May 2020
Tools Δ   0Kb   28 May 2020
Type
In Proceedings
Book title
20th International Joint Conference on Artificial Intelligence (IJCAI-07), Hyderabad, India
Year
2007

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.

Tags Tags: , , , , ,

BibTeX Record
  @INPROCEEDINGS{lvl-2007-2,
    TITLE = {Automatic Verification of Knowledge and Time with NuSMV},
    AUTHOR = {Alessio Lomuscio and Charles Pecheur and Franco Raimondi},
    YEAR = {2007},
    URL = {https://lvl.info.ucl.ac.be/Publications/AutomaticVerificationOfKnowledgeAndTimeWithNuSMV},
  }