First-order model checking on nested pushdown trees is complete for doubly exponential alternating time

Abstract

Recently we proved that first-order model checking on nested pushdown trees can be done in doubly exponential alternating time with linearly many alternations. Using the interpretation method of Compton and Henson we give a matching lower bound, i.e., we prove that first-order model checking on nested pushdown trees is complete for with respect to log-lin reductions. © 2012 Springer-Verlag Berlin Heidelberg.