This paper presents a verification approach for multiagent systems. The specification is based upon Object-Z and uses the influence/reaction model. The verification process consists in the transformation of Object-Z specifications into transition systems. This allows us to verify automatically some properties of the specification such as history invariants expressed by temporal logic formulas.
Citation:
Pablo Gruer, Vincent Hilaire, Abder Koukam, "Towards Verification of Multi-Agent Systems," icmas, pp.0393, Fourth International Conference on Multi-Agent Systems (ICMAS'00), 2000