A Data Symmetry Reduction Technique for Temporal-epistemic Logic

We present a data symmetry reduction approach for model temporal-epistemic logic. The technique abstracts the epistemic indistinguishably relation for the knowledge operators, and is shown to preserve temporal-epistemic formulae. We show a method for statically detecting data symmetry in an ISPL program, the input to the temporalepistemic model checker MCMAS. The experiments we report show an exponential saving in verification time and space while verifying security properties of the NSPK protocol.

• Type: Conference
• Year: 2009
• Where: ATVA
• Authors: Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu
• Keywords: ATVA 2009, Data Symmetry, Data Symmetry Reduction, Hardware, Model Temporal-epistemic Logic