Abstract We define the logic LDLK, a formalism for specifying multi-agent systems. LDLK extends LDL with epistemic modalities, including common knowledge, for reasoning about evolution of knowledge states of agents in the system. We show that the problem of verifying multi-agent systems against LDLK specifications is PSPACE-complete. We give an algorithm for practical verification of multiagent systems specified in LDLK. We show that the model checking algorithm, based on alternating automata and -NFAs, is fixed parameter tractable, scalable in the size of models analysed, and amenable to symbolic implementation on OBDDs. We introduce MCMASLDLK, an extension of the open-source model checker MCMAS implementing the algorithm presented, and discuss the experimental results obtained