  Adding propositional quantification to the modal logics K, T or S4 is known
to lead to undecidability but CTL with propositional quantification under the
tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability
problem. We investigate the complexity of strict fragments of tQCTL as well as
of the modal logic K with propositional quantification under the tree
semantics. More specifically, we show that tQCTL restricted to the temporal
operator EX is already Tower-hard, which is unexpected as EX can only enforce
local properties. When tQCTL restricted to EX is interpreted on N-bounded trees
for some N >= 2, we prove that the satisfiability problem is AExpPol-complete;
AExpPol-hardness is established by reduction from a recently introduced tiling
problem, instrumental for studying the model-checking problem for interval
temporal logics. As consequences of our proof method, we prove Tower-hardness
of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as
K, KD, GL, K4 and S4 with propositional quantification under a semantics based
on classes of trees.
