Deciding Asynchronous Hyperproperties for Recursive Programs

TL;DR

This paper introduces a new logic for asynchronous hyperproperties tailored for recursive programs, enabling more expressive analysis while maintaining manageable complexity for finite models and addressing the challenging recursive case.

Contribution

It presents a novel asynchronous hyperproperty logic with a new trace position mechanism, extending model checking capabilities to recursive programs.

Findings

Logic is more expressive than recent related logic.

Model checking complexity remains the same for finite state models.

First approach for hyperproperty model checking in recursive programs.

Abstract

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.