Model Checking Multi-Agent Systems against LDLK Specifications on Finite Traces

We introduce the logic LDL f K, a variant of the epistemic logic LDLK, interpreted on finite traces of multi-agent systems. We explore the verification problem of multi-agent systems against LDL f K specifications and give algorithms for the reduction of LDL f K model checking to LDLK verification on a different model and different specification. We analyse the resulting complexity and show it to be PSPACE-complete. We report on a full implementation of the algorithm and assess its performance on a number of examples.