Header menu link for other important links
X
Short Duration Aggregate Statistical Model Checking for Multi-Agent Systems
Published in Springer Science and Business Media Deutschland GmbH
2021
Volume: 12568 LNAI
   
Pages: 420 - 427
Abstract
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. We argue that this approach is particularly useful for aggregate queries on Multi-Agent systems that are also restricted in the time horizon–for example, bounded until operators in probabilistic temporal languages. We show that this can result in significant improvement in running times at the expense of only a marginal loss in accuracy and provide empirical evidence for this. © 2021, Springer Nature Switzerland AG.