  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.
