Sciweavers

Share
CLIMA
2011

Verifying Team Formation Protocols with Probabilistic Model Checking

8 years 7 months ago
Verifying Team Formation Protocols with Probabilistic Model Checking
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 twoplayer 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.
Taolue Chen, Marta Z. Kwiatkowska, David Parker, A
Added 18 Dec 2011
Updated 18 Dec 2011
Type Journal
Year 2011
Where CLIMA
Authors Taolue Chen, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis
Comments (0)
books