Collapsible Pushdown Graphs and First-Order Logic -- Navigating the fringe of decidability

Chris Broadbent


A higher-order pushdown automaton (HOPDA) generalises the standard notion of pushdown automaton (order-1) by allowing its stack to consist of nested stacks of stacks... of stacks rather than just the usual pile of atomic alphabet symbols. A collapsible pushdown automaton (CPDA) generalises this further by attaching `links' between different components of the higher-order stack. The interest in the latter derives from the fact that CPDA can generate precisely the same set of trees as so-called `higher-order recursion schemes', which are systems of rewrite rules with applications to the modelling and hence verification of higher-order functional programs.

Whilst the configuration graphs of HOPDA all have a decidable MSO (monadic second-order) theory, this is not the case for the configuration graphs of CPDA. Indeed, even at order-2 one can construct a graph with an undecidable MSO theory. This raises the question as to how first-order logic fares with CPDA. In a recent breakthrough, Kartzow
has shown that the configuration graphs of order-2 CPDA have decidable first-order theory -- indeed they are `tree automatic' (the graphs can be represented using finite tree automata recognising the nodes and pairs of nodes bearing edges).

Disappointingly, and a little surprisingly, we have a plethora of undecidability results that show such a result does not hold at order-3 and above. However, under certain restrictions we can recover interesting decidability results and the act of doing so introduces some novel apparatus in the form of `nested-tree automatic structures'.

In this talk I will endeavour to explain some of the background to this work and briefly outline the way in which these results have been obtained. This is work reasonably progressed but nevertheless still in progress!
Thursday 11th November 2010, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science