Linear Dynamic Logic (LDL) is a relatively modern temporal logic introduced by Vardi and De Giacomo at IJCAI 2013. LDL is attractive because it can express all omega-regular properties while, at the same time, it enjoys a PSPACE-complete model checking problem, like LTL.
This talk will discuss some of my work on symbolic model checking for LDL, which formed the main part of my master’s thesis. I will introduce a novel algorithm for reducing LDL model checking to CTL model checking
with fairness constraints developed during the project. I will then show how we can adapt the algorithm to support epistemic modalities under observational semantics, as well as a natural full-branching time epistemic extension of LDL, CDL*K.
I will then discuss the implementation of these algorithms in MCMAS-Dynamic, an extension of the MCMAS model checker which supports LDL (and CDL*K) specifications. I will also comment on some of the performance optimisations implemented which were essential in improving the scalability of LDL/CDL*K model checking to larger state spaces.
In the final talk in this series, I will address extensions of LDL on finite traces.