Model Checking Knowledge And Commitments In Multiagent Systems Using Actors And Uppaal

This paper proposes a method for modelling and analysis of knowledge and commitments in multi-agent systems. The approach is based on an actors model and its reduction onto UPPAAL. A key factor of the approach is the possibility of exploiting the same UPPAAL model for exhaustive verification or, when state explosion problems forbid model checking, for quantitative evaluation of system properties through statistical model checking. The article describes the method, shows its application to modelling the NetBill protocol, proposes a translation into the terms of the timed automata language of UPPAAL and demonstrates the analysis of the NetBill protocol together with some experimental results.