The Complexity of Monitoring Hyperproperties

TL;DR

This paper analyzes the computational complexity of runtime verification for hyperproperties expressed in HyperLTL, considering different Kripke structure shapes and formula complexities, revealing that complexity varies significantly with these factors.

Contribution

It provides a detailed complexity analysis of model checking hyperproperties over tree-shaped and acyclic Kripke structures, highlighting the impact of structure shape and formula alternation.

Findings

Model checking over trees is L-complete, regardless of quantifier alternation.

Model checking over acyclic structures is PSPACE-complete, matching the complexity of the polynomial hierarchy.

Combined complexity is PSPACE-complete, but reduces to NC for certain cases with alternation-free formulas.

Abstract

We study the runtime verification of hyperproperties, expressed in the temporal logic HyperLTL, as a means to inspect a system with respect to security polices. Runtime monitors for hyperproperties analyze trace logs that are organized by common prefixes in the form of a tree-shaped Kripke structure, or are organized both by common prefixes and by common suffixes in the form of an acyclic Kripke structure. Unlike runtime verification techniques for trace properties, where the monitor tracks the state of the specification but usually does not need to store traces, a monitor for hyperproperties repeatedly model checks the growing Kripke structure. This calls for a rigorous complexity analysis of the model checking problem over tree-shaped and acyclic Kripke structures. We show that for trees, the complexity in the size of the Kripke structure is L-complete independently of the number of quantifier alternations in the HyperLTL formula. For acyclic Kripke structures, the complexity is PSPACE-complete (in the level of the polynomial hierarchy that corresponds to the number of quantifier alternations). The combined complexity in the size of the Kripke structure and the length of the HyperLTL formula is PSPACE-complete for both trees and acyclic Kripke structures, and is as low as NC for the relevant case of trees and alternation-free HyperLTL formulas. Thus, the size and shape of both the Kripke structure and the formula have significant impact on the complexity of the model checking problem.