Complexity of Model Checking Second-Order Hyperproperties on Finite Structures

TL;DR

This paper investigates the decidability and complexity of model checking Hyper2LTL, a second-order hyperlogic, over finite structures, providing complexity bounds for different model classes and fragments.

Contribution

It establishes decidability of Hyper2LTL model checking on finite structures and characterizes its complexity, including for a fragment with simpler computational properties.

Findings

Hyper2LTL model checking is decidable on finite structures.

Complexity is PSPACE for tree-shaped models and EXPSPACE for acyclic models.

The Fixpoint Hyper2LTLfp fragment has lower complexity, P-complete on trees and EXP-complete on acyclic graphs.

Abstract

We study the model checking problem of Hyper2LTL over finite structures. Hyper2LTL is a second-order hyperlogic, that extends the well-studied logic HyperLTL by adding quantification over sets of traces, to express complex hyperproperties such as epistemic and asynchronous hyperproperties. While Hyper2LTL is very expressive, its expressiveness comes with a price, and its general model checking problem is undecidable. This motivates us to study the model checking problem for Hyper2LTL over finite structures -- tree-shaped or acyclic graphs, which are particularly useful for monitoring purposes. We show that Hyper2LTL model checking is decidable on finite structures. It is in PSPACE (in the size of the model) on tree-shaped models and in EXPSPACE on acyclic models. Additionally, we show that for an expressive fragment of Hyper2LTL, namely the Fixpoint Hyper2LTLfp fragment, the model checking problem is much simpler and is P-complete on tree-shaped models and EXP-complete on acyclic models. Last, we present some preliminary results that take into account not only the size of the model, but also the formula size.