Coinductive Proofs for Temporal Hyperliveness

TL;DR

This work addresses the lack of deductive tools for temporal hyperproperties, focusing on the challenging $\forall^*\exists^*\psi$ class. It introduces HyCo, a Coq-mechanized, language-agnostic framework that uses parameterized coinduction to build incremental witnesses for hyperproperties, aligning with a game-interpretation yet avoiding explicit arena construction. The key contributions include the soundness of HyCo, incremental reasoning rules, derivatives-based handling of temporal modalities, up-to techniques via GPACO, and a specialized deductive system for imperative programs with I/O. The framework enables interactive proofs of infinite-trace hyperproperties in reactive systems, with concrete Coq demonstrations and avenues for future enhancements such as prophecy variables and enhanced completeness.

Abstract

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^*ψ$, 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 (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.

Figures (9)

• Figure 1: Rules of parameterized coinduction
• Figure 2: Incremental reasoning rules for $\texttt{fei}$
• Figure 3: Incremental reasoning rules for $\texttt{fe}$
• Figure 4: Derivatives of common temporal modalities
• Figure 5: Selection of proof rules for temporal modalities

Theorems & Definitions (12)

• lemma 1: Coinduction principle
• theorem 1: Soundness of $\texttt{fei}_\varphi$
• lemma 2: Progress
• definition 1: Functional Choice
• corollary 1
• lemma 3: Witness
• definition 2: Safety closure
• definition 3: Safety relations
• lemma 4
• corollary 2: Coinductive safety proofs