The paper presents the method of model checking applied to verification of persuasive inter-agent communication. The model checker Perseus is designed on the basis of a logic of actions and graded beliefs AG n introduced by Budzynska and Kacprzak. The software tool makes it possible to semantically verify satisfaction of AG n formulas which describe different properties of a multi-agent system in a given model, and to perform parametric verification that enables searching for answers to questions about these properties.
|Number of pages||24|
|Journal||Studies in Logic, Grammar and Rhetoric|
|Publication status||Published - 2011|