一句话：提出 HyCo：面向 ∀*∃* 安全型时序超性质的余归纳证明框架，并在 Coq 中机械化与验证其可靠性。
针对时序超性质缺乏演绎证明系统、尤其难以处理执行量词交替的问题，本文研究形如 ∀*∃* ψ（ψ 为安全关系）的超性质，并证明该类性质总可被余归纳关系近似，从而支持直观的余归纳证明。基于此，作者在 Coq 证明助手中实现机械化框架 HyCo，用于推理时序超性质，给出其构造与可靠性证明，并将其应用于验证建模为带非确定性和 I/O 的命令式反应系统。该工作为超活性等性质提供了可机器检验的演绎验证途径。
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 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. This enables intuitive proofs by coinduction. Based on this observation, we define HyCo ( Hy perproperties, Co inductively), 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2501-07920,
title = {Coinductive Proofs for Temporal Hyperliveness},
author = {Arthur Correnson and Bernd Finkbeiner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704889}
}