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 paper, we focus on the difficult class of hyperproperties of the form $\forall^*\exists^*\psi$, where $\psi$ 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. This enables intuitive proofs by coinduction. Based on this observation, we define HyCo (HYperproperties, COinductively), a mechanized framework to reason about temporal hyperproperties within the Coq proof assistant. We detail the construction of HyCo, provide a proof of its soundness, and exemplify its use by applying it to the verification of reactive systems modeled as imperative programs with nondeterminism and I/O.

翻译：超属性的时序逻辑作为一种表达关系性质的形式化规范技术，最近在反应式系统的关系属性描述中崭露头角。尽管此类逻辑的模型检测问题已得到广泛研究，但针对时序超属性的演绎证明系统却十分匮乏。特别是，那些在系统执行上涉及全称与存在量词交替的超属性很少得到支持。本文聚焦于形式为 $\forall^*\exists^*\psi$ 的超属性类别，其中 $\psi$ 为安全关系，这是一类极具挑战性的超属性。我们证明，此类超属性——包含许多重要的超活性性质——总可通过余归纳关系进行近似。这使得基于余归纳的直观证明成为可能。基于这一观察，我们定义了 HyCo（HYperproperties, COinductively），这是一个在 Coq 证明助手中进行时序超属性推理的机械化框架。我们详细阐述了 HyCo 的构造，提供了其可靠性的证明，并通过将其应用于以具有非确定性和输入/输出的命令式程序建模的反应式系统验证，展示了其使用方法。