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.

Formal Reasoning on Knowledge and Commitments in Multi-Agent Systems using Theatre

Libero Nigro
;
Paolo F. Sciammarella
Membro del Collaboration Group
2019-01-01

Abstract

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.
2019
Multi-agent systems, knowledge and commitments, actors, reduction to Uppaal timed automata, exhaustive model checking, statistical model checking, NetBill protocol
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/295452
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 4
social impact