TY - CPAPER AB - We present an automatic data-abstraction technique for the verification of the universal fragment of the temporal-epistemic logic CTLK. We show the correctness of the methodology and present an implementation operating on ISPL models, the input files for MCMAS, a model checker for multi-agent systems. The experimental results point to the attractiveness of the technique in a number of examples in the multi-agent systems domain. © 2011 Springer-Verlag. AU - Lomuscio,A AU - Qu,H AU - Russo,F DO - 10.1007/978-3-642-20674-0_4 EP - 68 PY - 2011/// SN - 0302-9743 SP - 52 TI - Automatic data-abstraction in model checking multi-agent systems UR - http://dx.doi.org/10.1007/978-3-642-20674-0_4 ER -