Graph Width and Practical Existential Second Order Model Checking.
For two decades we have known how to automatically generate linear-time algorithms for MSO model checking on any bounded-tree-width class of structures. However, obtaining practical algorithms remains a major challenge. Over the same time period, software systems for $\exists$SO model checking have become very effective in practical applications. However, they do not generally provide FPT performance even for $\exists$MSO formulas, leading to the question of when they can (or could be adapted to) do so. I will survey properties relevant to this question, in part by viewing the systems as implementing MSO transformations.