Graph Width and Practical Existential Second Order Model Checking.
Speaker:
David Mitchell, Simon Fraser University
Date and Time:
Tuesday, October 10, 2017 - 10:45am to 11:10am
Location:
Fields Institute, Room 230
Abstract:
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.