Symbolic Model Checking Multi-Agent Systems against CTL*K Specifications

We introduce a technique for model checking multi-agent systems against temporal-epistemic specifications expressed in the logic CTL * K. 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.