Verifying Interlevel Relations within Multi-Agent Systems

An approach to handle the complex dynamics of a multi-agent system is based on distinguishing aggregation levels by structuring the system into parts or components. The behavior of every aggregation level is specified by a set of dynamic properties for components and interactions at that level, expressed in some (temporal) language. The dynamic properties of higher aggregation levels in principle can be logically related to dynamic properties of lower levels. This asks for identification and verification of such interlevel relations. In this article it is shown how this problem can be addressed using model checking techniques