The verification of Multi-Agent Systems (MAS) presents a significant challenge, with various approaches and methodologies available to address it. However, tools supporting these methodologies are not always readily accessible. Existing tools often lack compositionality, are hard-coded, and have a steep learning curve. In this paper, we present VITAMIN, a modular and versatile tool designed for the formal verification of MAS. Unlike existing tools, VITAMIN offers high usability and can be easily extended to support various models and logics for MAS.

On the Usability and Extensibility of VITAMIN / Ferrando, A., Malvone, V.. - 16031:(2026), pp. 354-359. (23rd International Conference on Practical applications of Agents and Multi-Agent Systems, PAAMS 2025 fra 2025) [10.1007/978-3-032-07638-0_30].

On the Usability and Extensibility of VITAMIN

Ferrando A.;
2026

Abstract

The verification of Multi-Agent Systems (MAS) presents a significant challenge, with various approaches and methodologies available to address it. However, tools supporting these methodologies are not always readily accessible. Existing tools often lack compositionality, are hard-coded, and have a steep learning curve. In this paper, we present VITAMIN, a modular and versatile tool designed for the formal verification of MAS. Unlike existing tools, VITAMIN offers high usability and can be easily extended to support various models and logics for MAS.
2026
23rd International Conference on Practical applications of Agents and Multi-Agent Systems, PAAMS 2025
fra
2025
16031
354
359
Ferrando, A.; Malvone, V.
On the Usability and Extensibility of VITAMIN / Ferrando, A., Malvone, V.. - 16031:(2026), pp. 354-359. (23rd International Conference on Practical applications of Agents and Multi-Agent Systems, PAAMS 2025 fra 2025) [10.1007/978-3-032-07638-0_30].
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

Licenza Creative Commons
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11380/1413456
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
  • OpenAlex ND
social impact