Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction

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 p...

Full description

Saved in:
Bibliographic Details
Main Authors: HAO, Jianye, SONG, Songzheng, LIU, Yang, SUN, Jun, GUI, Lin, DONG, Jin Song, LEUNG, Ho-fung
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2012
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/5025
https://ink.library.smu.edu.sg/context/sis_research/article/6028/viewcontent/Probabilistic_Model_Checking_Multi_agent_Behaviors_in_Dispersion_Games_Using_Counter_Abstraction.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-6028
record_format dspace
spelling sg-smu-ink.sis_research-60282020-03-12T08:59:36Z Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction HAO, Jianye SONG, Songzheng LIU, Yang SUN, Jun GUI, Lin DONG, Jin Song LEUNG, Ho-fung 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. 2012-07-09T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5025 info:doi/10.1007/978-3-642-32729-2_2 https://ink.library.smu.edu.sg/context/sis_research/article/6028/viewcontent/Probabilistic_Model_Checking_Multi_agent_Behaviors_in_Dispersion_Games_Using_Counter_Abstraction.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Model Check Multiagent System Model Check Technique Vickrey Auction Statistical Model Check Programming Languages and Compilers Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Model Check
Multiagent System
Model Check Technique
Vickrey Auction
Statistical Model Check
Programming Languages and Compilers
Software Engineering
spellingShingle Model Check
Multiagent System
Model Check Technique
Vickrey Auction
Statistical Model Check
Programming Languages and Compilers
Software Engineering
HAO, Jianye
SONG, Songzheng
LIU, Yang
SUN, Jun
GUI, Lin
DONG, Jin Song
LEUNG, Ho-fung
Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction
description 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.
format text
author HAO, Jianye
SONG, Songzheng
LIU, Yang
SUN, Jun
GUI, Lin
DONG, Jin Song
LEUNG, Ho-fung
author_facet HAO, Jianye
SONG, Songzheng
LIU, Yang
SUN, Jun
GUI, Lin
DONG, Jin Song
LEUNG, Ho-fung
author_sort HAO, Jianye
title Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction
title_short Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction
title_full Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction
title_fullStr Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction
title_full_unstemmed Probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction
title_sort probabilistic model checking multi-agent behaviors in dispersion games using counter abstraction
publisher Institutional Knowledge at Singapore Management University
publishDate 2012
url https://ink.library.smu.edu.sg/sis_research/5025
https://ink.library.smu.edu.sg/context/sis_research/article/6028/viewcontent/Probabilistic_Model_Checking_Multi_agent_Behaviors_in_Dispersion_Games_Using_Counter_Abstraction.pdf
_version_ 1770575192748195840