First-Order Logic on CPDA Graphs

It is known that configuration graphs of higher-order pushdown automata (without the collapse operation) coincide with graphs in the Caucal hierarchy. In particular these graphs have decidable MSO theory. The next step is to consider configuration graphs of collapsible higher-order pushdown automata (CPDA). It turns out that MSO theory is undecidable for them. I will discuss results about decidability of first-order theory on these graphs. In general the first-order theory is also undecidable. However we can be more precise, and ask for decidability e.g. for existential formulas or for automata of order 2, etc. The results in this topic are mainly by A.Kartzow and C.Broadbent, but I also have some small contributions.