Quantitative analysis of multi-agent systems through statistical verification of simulation traces.

Due to their immense complexity, large-scale multi-agent systems are often not amenable to exhaustive formal verification. Statistical approaches that focus on the verification of individual traces can provide an interesting alternative that circumvents combinatorial explosion. 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 verification can be used to answer interesting quantitative correctness questions about multi-agent systems at different observational levels. The usefulness of the verification approach is illustrated with a simple case study from the area of swarm robotics.