A Survey on Model Checking for Collapsible Pushdown Graphs

The model checking problem for some logic L and a class of
graphs C is the problem to decide, on input a graph G from C and a
formula phi from L, whether G satisfies phi.
We first introduce the hierarchies of (collapisble) higher-order
pushdown graphs and then survey the various (un)decidability results on
this hierarchy concerning model checking with respect to different
logics. These results give a rather complete picture of the "logical"
behaviour of these hierarchies.
In contrast, structural results on the collapsible pushdown graph
hierarchy are rare. If time permits we will briefly discuss this lack of
understanding of the hierarchy as well.