Multi-Agent Systems with Information Sharing: Strategies and Model Checking

We introduce a prototyping language for multi-agent systems with information sharing, allowing agents to act in parallel and to migrate between distributed locations according to explicit timers. While all agents have access to public information, each agent also has access to private information to decide its next actions. The formal semantics of this language is provided, and an example is used to illustrate multi-agent systems with information sharing. An implementation in the rewriting engine Maude provides the possibility to describe and analyze the evolution of some multi-agent systems. Using the advantage of a strategy module in Maude, we can guide the application of rules, substantially reducing the state space in multi-agent systems with non-deterministic behavior. Given the executable specifications of a multi-agent system, we use the model checking tools of Maude to check various behavioral properties and to detect some behavioral problems.