ABSTRACT. We study the runtime verification (RV) complexity of hyperproperties expressed in the temporal logic HyperLTL as a means to inspect a system with respect to a set of security polices. The monitor analyzes trace logs organized by common prefixes that form a finite tree-shaped Kripke structure, or, by common prefixes and suffixes that form a finite acyclic Kripke structure. Unlike the RV techniques for trace-based languages, where monitors are often memoryless, to monitor a hyperproperty as the system execution(s) evolve, the monitor has to repeatedly check a growing Kripke structure that records the traces observed so far. This calls for a rigorous complexity analysis of RV for hyperproperties.

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 the Kripke structure as well as the formula have significant impact on the efficiency of monitoring.