Sciweavers

ENTCS
2006

Automated Game Analysis via Probabilistic Model Checking: a case study

13 years 11 months ago
Automated Game Analysis via Probabilistic Model Checking: a case study
It has been recognised for some time that there are close links between the various logics developed for the analysis of multi-agent systems and the many game-theoretic models developed for the same purpose. In this paper, we contribute to this burgeoning body of work by showing how a probabilistic model checking tool can be used for the automated analysis of game-like multi-agent systems in which both agents and environments can act with uncertainty. Specifically, we show how a variation of the well-known alternating offers negotiation protocol of Rubinstein can be encoded as a model for the PRISM model checker and its behaviour analysed through automatic verification of probabilistic CTL's properties.
Paolo Ballarini, Michael Fisher, Michael Wooldridg
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Paolo Ballarini, Michael Fisher, Michael Wooldridge
Comments (0)