Introducing Agents in Multi-agent System with Superposition Refinement

A formal and incremental approach is needed to introduce new agents in the development of multi-agent system (MAS) due to its intrinsic complexity. Incremental development with refinement theory is a traditional way to guarantee the dependability of a system. We specify MAS with Object-Z notation and under trace semantic of action system, give the mathematical relation model and refinement rules of superposition refinement based on the relational model and Object-Z notation. The refinement rules provide a foundation for introducing agents in MAS. A case study of repairing robots is used to show whether agents are introduced correctly.