  Strategy Logic with imperfect information (SLiR) is a very expressive logic
designed to express complex properties of strategic abilities in distributed
systems. Previous work on SLiR focused on finite systems, and showed that the
model-checking problem is decidable when information on the control states of
the system is hierarchical among the players or components of the system,
meaning that the players or components can be totally ordered according to
their respective knowledge of the state. We show that moving from finite to
infinite systems generated by collapsible (higher-order) pushdown systems
preserves decidability, under the natural restriction that the stack content is
visible. The proof follows the same lines as in the case of finite systems, but
requires to use (collapsible) alternating pushdown tree automata. Such automata
are undecidable, but semi-alternating pushdown tree automata were introduced
and proved decidable, to study a strategic problem on pushdown systems with two
players. In order to tackle multiple players with hierarchical information, we
refine further these automata: we define direction-guided (collapsible)
pushdown tree automata, and show that they are stable under projection,
nondeterminisation and narrowing. For the latter operation, used to deal with
imperfect information, stability holds under some assumption that is satisfied
when used for systems with visible stack. We then use these automata to prove
our main result.
