  In the literature, two powerful temporal logic formalisms have been proposed
for expressing information flow security requirements, that in general, go
beyond regular properties. One is classic, based on the knowledge modalities of
epistemic logic. The other one, the so called hyper logic, is more recent and
subsumes many proposals from the literature; it is based on explicit and
simultaneous quantification over multiple paths. In an attempt to better
understand how these logics compare with each other, we consider the logic
KCTL* (the extension of CTL* with knowledge modalities and synchronous perfect
recall semantics) and HyperCTL*. We first establish that KCTL* and HyperCTL*
are expressively incomparable. Second, we introduce and study a natural linear
past extension of HyperCTL* to unify KCTL* and HyperCTL*; indeed, we show that
KCTL* can be easily translated in linear time into the proposed logic.
Moreover, we show that the model-checking problem for this novel logic is
decidable, and we provide its exact computational complexity in terms of a new
measure of path quantifiers' alternation. For this, we settle open complexity
issues for unrestricted quantified propositional temporal logic.
