Boureanu, Ioana CristinaJones, AndrewLomuscio, Alessio2012-01-212012-01-212012-01-212012https://infoscience.epfl.ch/handle/20.500.14299/77023We present a methodology for the automatic verification of multi-agent systems against temporal-epistemic specifications derived from higher-level languages defined 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 verification 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.NCCR-MICSNCCR-MICS/Secutext::conference output::conference proceedings::conference paper