Abstract
We present the integration of a normative programming language in the MCAPL framework for model checking multi-agent systems. The result is a framework facilitating the implementation and verification of multi-agent systems coordinated via a normative organisation. The organisation can be programmed in the normative language while the constituent agents may be implemented in a number of (BDI) agent programming languages.
We demonstrate how this framework can be used to check properties of the organisation and of the individual agents in an LTL based property specification language. We show that different properties may be checked depending on the information available to the model checker about the internal state of the agents. We discuss, in particular, an error we detected in the organisation code of our case study which was only highlighted by attempting a verification with “white box” agents
We demonstrate how this framework can be used to check properties of the organisation and of the individual agents in an LTL based property specification language. We show that different properties may be checked depending on the information available to the model checker about the internal state of the agents. We discuss, in particular, an error we detected in the organisation code of our case study which was only highlighted by attempting a verification with “white box” agents
| Original language | Undefined |
|---|---|
| Publisher | Springer Nature |
| Number of pages | 19 |
| Volume | 6214 |
| ISBN (Print) | 9783642168666 |
| ISBN (Electronic) | 9783642168673 |
| DOIs | |
| Publication status | Published - 2010 |
Keywords
- Model check
- Multiagent system
- Operational semantic
- Transition rule
- Belief base