Tree-width has been a popular parameter that gives tractable algorithms in parametrised algorithms. In this talk we explore its use in verification.
Verification amounts to guaranteeing that a property holds on all runs of the system. We will consider systems with stacks, communicating channels, variables etc. As expected, these systems are Turing powerful and their verification is undecidable in general.
Under-approximation is a technique that allows to still reason about such Turing powerful systems, and has been proven efficient in finding bugs. In under-approximate verification, only a subset of runs are explored, and the subset is often specified by a parameter. We will now impose a bound on tree-width as the parameter.
Towards this, we will depart from the traditional view of treating runs as just words (sequences) to a richer understanding in terms of graphs. Thus the behaviours of a system is a (possibly infinite) set of unbounded graphs.
With bounded tree-width under-approximation, we will explore only those behaviours whose tree-width is bounded by the given parameter. We will see that many verification problems become efficiently decidable when restricted to graphs of tree-width bounded by a parameter k, even though it allows to explore infinitely many runs (behaviours).
We will see this in the particular case of multi-pushdown systems, communicating finite state machines, communicating pushdown machines, timed multi-pushdown systems and multi-pushdown systems handling numerical data.