Temporal hyperproperties are system properties that relate multiple execution traces. In finite-state systems, temporal hyperproperties are supported by model-checking algorithms, and tools for general temporal logics like HyperLTL exist. In infinite-state systems, the analysis of temporal hyperproperties has, so far, been limited to k-safety properties, i.e., properties that stipulate the absence of a bad interaction between any k traces. In this paper, we present an automated method for the verification of <InlineEquation ID="IEq1"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_482_Article_IEq1.gif" Format="GIF" Height="17" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\forall ^k\exists ^l$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <msup> <mo>∀</mo> <mi>k</mi> </msup> <msup> <mo>∃</mo> <mi>l</mi> </msup> </mrow> </math></EquationSource> </InlineEquation>-safety properties in infinite-state systems. A <InlineEquation ID="IEq2"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_482_Article_IEq1.gif" Format="GIF" Height="17" Rendition="HTML" Resolution="72" Type="Linedraw" Width="33" /> </InlineMediaObject> <EquationSource Format="TEX">$\forall ^k\exists ^l$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <msup> <mo>∀</mo> <mi>k</mi> </msup> <msup> <mo>∃</mo> <mi>l</mi> </msup> </mrow> </math></EquationSource> </InlineEquation>-safety property stipulates that for any k traces, there exist l traces such that the resulting <InlineEquation ID="IEq3"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10703_2025_482_Article_IEq3.gif" Format="GIF" Height="15" Rendition="HTML" Resolution="72" Type="Linedraw" Width="39" /> </InlineMediaObject> <EquationSource Format="TEX">$k+l$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi>k</mi> <mo>+</mo> <mi>l</mi> </mrow> </math></EquationSource> </InlineEquation> traces do not interact badly. This combination of universal and existential quantification captures many properties beyond k-safety, including hyperliveness properties such as generalized non-interference or program refinement. Our verification method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction.

Predicate abstraction for hyperliveness verification

期刊论文
出版模式：

开放获取
发表日期：

2025年7月16日

查看全文

Raven Beutner,
Bernd Finkbeiner

摘要

Temporal hyperproperties are system properties that relate multiple execution traces. In finite-state systems, temporal hyperproperties are supported by model-checking algorithms, and tools for general temporal logics like HyperLTL exist. In infinite-state systems, the analysis of temporal hyperproperties has, so far, been limited to k-safety properties, i.e., properties that stipulate the absence of a bad interaction between any k traces. In this paper, we present an automated method for the verification of $\forall ^k\exists ^l$ $\forall^{k} \exists^{l}$ -safety properties in infinite-state systems. A $\forall ^k\exists ^l$ $\forall^{k} \exists^{l}$ -safety property stipulates that for any k traces, there exist l traces such that the resulting $k+l$ $k + l$ traces do not interact badly. This combination of universal and existential quantification captures many properties beyond k-safety, including hyperliveness properties such as generalized non-interference or program refinement. Our verification method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction.