Automatic Verification of Temporal Epistemic Logic under Convergent Equational Theories

We 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.


Editor(s):
Conitzer, Vincent
Winikoff, Michael
Padgham, Lin
van der Hoek, Wiebe
Published in:
Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS12), II, 1141-1148
Presented at:
11th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS12), Valencia, Spania, June 2012
Year:
2012
Keywords:
Laboratories:




 Record created 2012-01-21, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)