The Tree-Width of Decidable Problems

Gennaro Parlato

We describe a common and uniform principle that explains the decidability of several decision problems. The main ingredient of our approach is representing solutions with labelled graphs that are definable in Monadic Second Order logic (MSO). For an appropriate graph encoding, it turns out that an instance of the problem has a positive answer if there is a solution whose graph representation has bounded tree-width. This allows us to reduce all those problems to the satisfiability problem of MSO on graphs of bounded tree-width (which is decidable due to Seese's theorem). We illustrate this approach for several decidable automata with auxiliary storage (stacks and queues) and for integer linear programming. We conclude with a conjecture whose positive answer will allow to extend this principle to a larger class of automata.