This paper proposes a formal method based on the THEATRE framework, for modeling and analysis of knowledge and commitments in multi-agent systems (MAS). THEATRE centres on actors and a reduction on to UPPAAL which enables both non-deterministic analysis (that is, qualitative analysis by exhaustive verification, or showing that something can possibly occur) and quantitative analysis (that is, estimating probability measures of event occurrence through simulations) of a same model. The article describes the modeling and analysis approach based on THEATRE and UPPAAL and shows its application to modeling and property checking of the NetBill protocol used in web-based MAS applications when selling/buying goods. Properties of the NetBill protocol are demonstrated by experimental results.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||Formal Reasoning on Knowledge and Commitments in Multi-Agent Systems using Theatre|
NIGRO, Libero (Corresponding)
SCIAMMARELLA, PAOLO FRANCESCO [Membro del Collaboration Group]
|Data di pubblicazione:||2019|
|Appare nelle tipologie:||1.1 Articolo in rivista|