Quantitative analysis of Multiagent systems through statistical model checking

Benjamin Herd*, Simon Miles, Peter McBurney, Michael Luck

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

12 Citations (Scopus)

Abstract

Due to their immense complexity, large-scale multiagent systems are often unamenable to exhaustive formal verification. Statistical approaches that focus on the verification of individual traces can provide an interesting alternative. However, due to its focus on finite execution paths, trace-based verification is inherently limited to certain types of correctness properties. We show how, by combining sampling with the idea of trace fragmentation, statistical model checking can be used to answer interesting quantitative correctness properties about multiagent systems on different observational levels. We illustrate the idea with a simple case study from the area of swarm robotics.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer-Verlag Berlin Heidelberg
Pages109-130
Number of pages22
Volume9318
ISBN (Print)9783319261836
DOIs
Publication statusPublished - 15 Nov 2015
Event3rd International Workshop on Engineering Multi-Agent Systems, EMAS 2015 - Istanbul, Turkey
Duration: 5 May 20155 May 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9318
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference3rd International Workshop on Engineering Multi-Agent Systems, EMAS 2015
Country/TerritoryTurkey
CityIstanbul
Period5/05/20155/05/2015

Keywords

  • Multiagent systems
  • Quantitative analysis
  • Statistical model checking
  • Verification

Fingerprint

Dive into the research topics of 'Quantitative analysis of Multiagent systems through statistical model checking'. Together they form a unique fingerprint.

Cite this