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

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.