  Information-flow policies prescribe which information is available to a given
user or subsystem. We study the problem of specifying such properties in
reactive systems, which may require dynamic changes in information-flow
restrictions between their states. We formalize several flavours of sequential
information-flow, which cover different assumptions about the semantic relation
between multiple observations of a system. Information-flow specification falls
into the category of hyperproperties. We define different variants of
sequential information-flow specification using a first-order logic with both
trace quantifiers and temporal quantifiers called Hypertrace Logic. We prove
that HyperLTL, equivalent to a subset of Hypertrace Logic with restricted
quantifier prefixes, cannot specify the majority of the studied two-state
independence variants. For our results, we introduce a notion of equivalence
between sets of traces that cannot be distinguished by certain classes of
formulas in Hypertrace Logic. This presents a new approach to proving
inexpressiveness results for logics such as HyperLTL.
