Deciding Asynchronous Hyperproperties for Recursive Programs

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 decidability and 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 this combination of asynchronicity and a non-regular model class constitutes the first suitable approach for hyperproperty model checking against recursive programs.