Name
Abstract | ||
|---|---|---|
We show that the problem ofmodel 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. |
Year | Venue | Keywords |
|---|---|---|
2007 | IJCAI | model checker nusmv,automatic verification,typical security protocol,temporal-epistemic logic,temporal-epistemic property,multi-dimensional modal logic,dining cryptographers,temporal logic ctl,action label,problem ofmodel,temporal logic,col,epistemic logic,model checking,security protocol,modal logic |
Field | DocType | Citations |
Computation tree logic,Dining cryptographers problem,Programming language,Model checking,Cryptographic protocol,Computer science,Operator (computer programming),Temporal logic,Modal | Conference | 18 |
PageRank | References | Authors |
0.84 | 11 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alessio Lomuscio | 1 | 1611 | 110.20 |
| Charles Pecheur | 2 | 284 | 28.50 |
| Franco Raimondi | 3 | 832 | 48.18 |