Oxford logo
[CKPS11] T. Chen, M. Kwiatkowska, D. Parker and A. Simaitis. Verifying Team Formation Protocols with Probabilistic Model Checking. In Proc. 12th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XII 2011), volume 6814 of LNCS, pages 190-297, Springer. July 2011. [pdf] [bib]
Downloads:  pdf pdf (623 KB)  bib bib
Notes: The original publication is available at link.springer.com.
Abstract. Multi-agent systems are an increasingly important software paradigm and in many of its applications agents cooperate to achieve a particular goal. This requires the design of efficient collaboration protocols, a typical example of which is team formation. In this paper, we illustrate how probabilistic model checking, a technique for formal verification of probabilistic systems, can be applied to the analysis, design and verification of such protocols. We start by analysing the performance of an existing team formation protocol modelled as a discrete-time Markov chain. Then, using a Markov decision process model, we construct optimal algorithms for team formation. Finally, we use stochastic two-player games to analyse the competitive coalitional setting, in which agents are split into cooperative and hostile classes. We present experimental results from these models using the probabilistic model checking tool PRISM, which we have extended with support for stochastic games.