  We introduce an extension of Strategy Logic for the imperfect-information
setting, called SLii, and study its model-checking problem. As this logic
naturally captures multi-player games with imperfect information, this problem
is undecidable; but we introduce a syntactical class of "hierarchical
instances" for which, intuitively, as one goes down the syntactic tree of the
formula, strategy quantifications are concerned with finer observations of the
model, and we prove that model-checking SLii restricted to hierarchical
instances is decidable. To establish this result we go through QCTL, an
intermediary, "low-level" logic much more adapted to automata techniques. QCTL
is an extension of CTL with second-order quantification over atomic
propositions. We extend it to the imperfect information setting by
parameterising second-order quantifiers with observations. While the
model-checking problem of QCTLii is, in general, undecidable, we identify a
syntactic fragment of hierarchical formulas and prove, using an
automata-theoretic approach, that it is decidable. We apply our result to solve
complex strategic problems in the imperfect-information setting. We first show
that the existence of Nash equilibria for deterministic strategies is decidable
in games with hierarchical information. We also introduce distributed rational
synthesis, a generalisation of rational synthesis to the imperfect-information
setting. Because it can easily be expressed in our logic, our main result
provides solution to this problem in the case of hierarchical information.
