Combining Simulation and Formal Tools for Developing Self-Organizing MAS
- Manage
- Copy
- Actions
- Export
- Annotate
- Print Preview
Choose the export format from the list below:
- Office Formats (1)
-
Export as Portable Document Format (PDF) using Apache Formatting Objects Processor (FOP)
-
- Other Formats (1)
-
Export as HyperText Markup Language (HTML)
-
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 / Views
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
Luca Gardelli, Mirko Viroli, Andrea Omicini
— 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
identifiers
— DOI
— IRIS
— Scopus
— 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