The formal development of multi-agent systems (MAS) may involve consideration of system functionality at three distinct levels of abstraction. The macro level focusses on the system’s overall, global behaviour, independently of how the agents of the system operate and interact. The meso level focusses on agent interactions, and the micro level on the operation of individual agents. While Object-Z with its high-level support for component-based specifications is well suited to modelling MAS at the macro and meso levels, it can become cumbersome at the micro level where the low-level mechanisms required for dealing with asynchronous communication between agents and timing constraints need to be explicitly defined. In this paper we introduce MAZE, an extension of Object-Z supporting (i) action refinement to facilitate the development process from the macro to micro level, and (ii) a number of syntactic conventions to facilitate micro-level specification. The syntactic conventions are shorthands for existing Object-Z notation and so require no redefinition of Object-Z’s semantics.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{SmithL14,
author = {Graeme Smith and
Qin Li},
editor = {Yamine A{\"{\i}}t Ameur and
Klaus{-}Dieter Schewe},
title = {{MAZE:} An Extension of Object-Z for Multi-Agent Systems},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8477},
pages = {72--85},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-662-43652-3\_6},
doi = {10.1007/978-3-662-43652-3\_6},
timestamp = {Thu, 07 Apr 2022 08:44:28 +0200},
biburl = {https://dblp.org/rec/conf/asm/SmithL14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}