Symbolic Model Checking Multi-Agent Systems against CTL*K Specifications
Jeremy Kong, Alessio R. Lomuscio · Adaptive Agents and Multi-Agents Systems · 2017
We introduce a technique for model checking multi-agent systems against temporal-epistemic specifications expressed in the logic CTL. We present an algorithm for the verification of explicit models and use this to show that the problem is PSPACE-complete. We show that the technique is amenable to symbolic implementation via binary decision diagrams. We introduce MCMAS, a toolkit based on the open-source model checker MCMAS which presently supports CTLK only, implementing the technique. We present the experimental results obtained and show its attractiveness compared to all other toolkits available.