Unifying Hyper and Epistemic Temporal Logics

Abstract. 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 lit-erature. 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 expres-sively incomparable. Then, we introduce a natural linear past extension of HyperCTL∗, called HyperCTL∗lp, that unifies KCTL ∗ and HyperCTL∗. We show that the model-checking problem for HyperCTL∗lp is decidable, and we provide its exact computational complexity in terms of a new measure of path quantifiers ’ alternation. For this, we settle open com-plexity issues for unrestricted quantified propositional temporal logic.