Formal reasoning on knowledge and commitments in multi-agent systems using Theatre. (February 2020)

• Record Type: Journal Article
• Authors: Nigro, Christian; Nigro, Libero; Sciammarella, Paolo F
• Is Part Of: Simulation. Volume 96:Number 2(2020)
• Page Start: 233
• Page End: 250
• Publication Date: 2020-02
• Subjects: Multi-agent systems -- knowledge and commitments -- actors -- reduction to Uppaal timed automata -- exhaustive model checking -- statistical model checking -- NetBill protocol; Computer simulation -- Periodicals; 003.3
• DOI: 10.1177/0037549719879753
• Languages: English
• ISSNs: 0037-5497

Abstract

This paper proposes a formal method based on the Theatre framework for modeling and analysis of knowledge and commitments in multi-agent systems (MASs). Theatre centers on actors and a reduction on toUppaal, 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 the same model. The article describes the modeling and analysis approach based on Theatre andUppaal, and shows its application to the 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.