A Survey on Model Checking for Collapsible Pushdown Graphs

Speaker(s)

Alexander Kartzow

Affiliation

Universitat Leipzig

Date

Nov. 2, 2011, 2:15 p.m.

Room

room 5870

Seminar

Seminar Automata Theory

---

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.

---