When: **Wednesday**, June 15, 2pm

Where: room G2.91b

**Abstract**

Courcelle's Theorem states that all MSO-definable problems can be solved in linear time on graphs of bounded treewidth. The standard approach of constructing a tree automaton from the MSO-formula and running this automaton on the tree decomposition often fails because the automaton cannot be constructed. We implemented a program that does not use tree automata, but constructs game trees for each node of the tree decomposition. From these game trees optimal solutions can easily be computed. Several algorithmic improvements were necessary to turn this idea into practically useful software.

Joint work with Peter Rossmanith