Serial and parallel algorithms for short time horizon multi-attribute queries on stochastic multi-agent systems

Statistical model checking (SMC) for the analysis of multi-agent systems has been studied in the recent past. A feature peculiar to multi-agent systems in the context of statistical model checking is that of aggregate queries–temporal logic formula that involves a large number of agents. To answer such queries through Monte Carlo sampling, the statistical approach to model checking simulates the entire agent population and evaluates the query. This makes the simulation overhead significantly higher than the query evaluation overhead. This problem becomes particularly challenging when the model checking queries involve multiple attributes of the agents. To alleviate this problem, we propose a population sampling algorithm that simulates only a subset of all the agents and scales to multiple attributes, thus making the solution generic. The population sampling approach results in increased efficiency (a gain in running time of 50%–100%) for a marginal loss in accuracy (between 1% and 5%) when compared with the exhaustive approach (which simulates the entire agent population to evaluate the query), especially for queries that involve limited time horizons. Finally, we report parallel versions of the above algorithms. We explore different strategies of core allocation, both for exhaustive simulations of all agents and the sampling approach. This yields further gains in running time, as expected. The parallel approach, when combined with the sampling idea, results in improving the efficiency (a gain in running time of 100%–150%) with a minor loss when compared with the exhaustive approach in accuracy (between 1% and 5%).