  We introduce a novel logic for asynchronous hyperproperties with a new
mechanism to identify relevant positions on traces. While the new logic is more
expressive than a related logic presented recently by Bozzelli et al., we
obtain the same complexity of the model checking problem for finite state
models. Beyond this, we study the model checking problem of our logic for
pushdown models. We argue that the combination of asynchronicity and a
non-regular model class studied in this paper constitutes the first suitable
approach for hyperproperty model checking against recursive programs.
