Model Checking Multi-Agent Systems against LDLK Specifications on Finite Traces
Jeremy Kong, Alessio R. Lomuscio · 2018
We introduce the logic LDL_fK, 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_fK specifications and give algorithms for the reduction of LDL_fK 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.