Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 99-122 |
| Number of pages | 24 |
| Journal | Studies in Logic, Grammar and Rhetoric |
| Volume | 23 |
| Issue number | 36 |
| Publication status | Published - 2011 |