Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

7-2012

Abstract

Accurate analysis of the stochastic dynamics of multi-agent system is important but challenging. Probabilistic model checking, a formal technique for analysing a system which exhibits stochastic behaviors, can be a natural solution to analyse multi-agent systems. In this paper, we investigate this problem in the context of dispersion games focusing on two strategies: basic simple strategy (BSS) and extended simple strategies (ESS). We model the system using discrete-time Markov chain (DTMC) and reduce the state space of the models by applying counter abstraction technique. Two important properties of the system are considered: convergence and convergence rate. We show that these kinds of properties can be automatically analysed and verified using probabilistic model checking techniques. Better understanding of the dynamics of the strategies can be obtained compared with empirical evaluations in previous work. Through the analysis, we are able to demonstrate that probabilistic model checking technique is applicable, and indeed useful for automatic analysis and verification of multi-agent dynamics.

Keywords

Model Check, Multiagent System, Model Check Technique, Vickrey Auction, Statistical Model Check

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 15th International Conference, Kuching, Sarawak, Malaysia, September 3-7

First Page

16

Last Page

30

ISBN

9783642327285

Identifier

10.1007/978-3-642-32729-2_2

Publisher

Springer Link

City or Country

Sarawak, Malaysia

Additional URL

https://doi.org/10.1007/978-3-642-32729-2_2

Download

Share

COinS