Temporal logics for hyperproperties have recently emerged as an expressive specification technique for relational properties of reactive systems. While the model checking problem for such logics has been widely studied, there is a scarcity of deductive proof systems for temporal hyperproperties. In particular, hyperproperties with an alternation of universal and existential quantification over system executions are rarely supported. In this presentation, we focus on hyperproperties of the form ∀ * ∃ * ψ, where ψ is a safety relation. We show that hyperproperties of this class – which includes many hyperliveness properties of interest – can always be approximated by coinductive relations. In turn, this enables intuitive proofs by coinduction. Building on this observation, we present a mechanized framework (in Coq/Rocq) to prove temporal hyperproperties of programs with nondeterminism and I/O.
