Short Duration Aggregate Statistical Model Checking for Multi-Agent Systems.

For analysing large and complex systems, Statistical Model Checking has proved to be an attractive alternative to the more expensive numerical model checking approaches. Statistical Model Checking involves Monte Carlo sampling of execution traces of the system. Stochastic multi-agent systems with very large agent populations add significant simulation overheads that dominate the model checking complexity. This offsets some of the advantage in terms of the speed that statistical model checking offers. To mitigate these simulation overheads, we explore an approach based on sampling agent populations in addition to the Monte Carlo sampling of execution traces.