Automatic Verification of Temporal Epistemic Logic under Convergent Equational Theories
We present a methodology for the automatic veriﬁcation of multi-agent systems against temporal-epistemic speciﬁcations derived from higher-level languages deﬁned over convergent equational theories. We introduce a modality called rewriting knowledge that operates on local equalities. We discuss the conditions under which its interpretation can be approximated by a second modality that we introduce called empirical knowledge. Empirical knowledge is computationally attractive from a veriﬁcation perspective. We report on an implementation of a technique to verify this modality inside the open source model checker MCMAS. We evaluate the approach by verifying multi-agent models of electronic voting protocols automatically extracted from high-level descriptions.