First-Order Model Checking on Nested Pushdown Trees is Complete for Doubly Exponential Alternating Time.

Alexander Kartzow

Browse the full FOSSACS paper archive.