Combining Simulation and Formal Tools for Developing Self-Organizing MAS


Luca Gardelli, Mirko Viroli, Andrea Omicini

Adelinde M. Uhrmacher, Danny Weyns (eds.)
Multi-Agent Systems: Simulation and Applications, chapter 5, pages 133–165
Computational Analysis, Synthesis, and Design of Dynamic Systems
CRC Press
June 2009

In this chapter, we focus on methodological aspects concerning the early-design stage of SOS built relying on the agent-oriented paradigm: in particular we refer to the A&A meta-model, where MAS are composed by agents and artifacts, i.e. environmental resources. Then, we describe an architectural pattern that has been extracted from a recurrent solution in designing self-organising systems: this pattern is based on a MAS environment formed by artifacts, modelling non-proactive resources, and environmental agents acting on artifacts so as to enable self-organising mechanisms. In this context, we propose an approach for the engineering of self-organising systems based on simulation at the early design stage: in particular, the approach is articulated in four stages, modelling, simulation, formal verification, and tuning. In this approach, simulations of an abstract system model are used to drive design choices until the required quality properties are obtained, thus providing guarantees that the subsequent design steps would lead to a correct implementation. However, system analysis exclusively based on simulation results does not provide sound guarantees for the engineering of complex systems: to this purpose, we envision the application of formal verification techniques, specifically model checking, in order to exactly characterise the system behaviours. Given a formal specification a probabilistic model checker determines wether a specific property is satisfied or not or the actual likelihood value: properties are specified using different flavours of temporal logic, depending on the model type, e.g. probabilistic, stochastic or non-deterministic. Unfortunately, the applicability of model checking techniques is hindered by the explosion of state space: nonetheless, in those cases model checking still a valuable tool for validating simulation results on small problem instances. 

As a case to clarify the approach, we analyse a self-organising solution to the problem of plain diffusion: given a networked set of nodes hosting information, we have to homogeneously distribute the information across the nodes. In order for a solution to be self-organising, control must be decentralized and entities have to interact locally: hence, we consider solutions having at least one agent for each node whose skills consist in sending information only to neighboring nodes and agent knowledge is restricted to the local node. We devise a strategy solving this problem following the methodological approach previously described. As far as formal tools are concerned, we rely on the PRISM Probabilistic Model Checker for the entire process, namely, modelling, simulation and verification. 

Publications

Publications / Views

Home

Clouds
•  tags  •  authors  •  editors  •  journals  

Year
 2023    2022    2021    2020    2019    2018    2017    2016    2015    2014–1927

Sort
•  in journal  •  in proc  •  chapters  •  books  •  edited  •  spec issues  •  editorials  •  entries  •  manuals  •  tech reps  •  phd th  •  others  

Status
•  online  •  in press  •  proof  •  camera-ready  •  revised  •  accepted  •  revision  •  submitted  •  draft  •  note  

Services
•  ACM Digital Library  •  DBLP  •  IEEE Xplore  •  IRIS  •  PubMed  •  Google Scholar  •  Scopus  •  Semantic Scholar  •  Web of Science  •  DOI  

Publication

— authors

— editors

Adelinde M. Uhrmacher, Danny Weyns

— status

published

— sort

book chapter

— publication date

June 2009

— volume

Multi-Agent Systems: Simulation and Applications

— series

Computational Analysis, Synthesis, and Design of Dynamic Systems

— chapter

5

— pages

133–165

URLs

original page

identifiers

— DOI

10.1201/9781420070248-15

— IRIS

11585/82469

— Scopus

2-s2.0-85068357847

— print ISBN

978-1-4200-7024-8

— online ISBN

 978-1-3152-1878-6

— ISBN–10

1-4200-7023-1

— ISBN–13

978-1-4200-7023-1

Partita IVA: 01131710376 — Copyright © 2008–2023 APICe@DISI – PRIVACY