Predicate abstraction for hyperliveness verification

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 <i>k</i>-safety properties, i.e., properties that stipulate the absence of a bad interaction between any <i>k</i> traces. In this paper, we present an automated method for the verification of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow><mml:msup><mml:mo>∀</mml:mo> <mml:mi>k</mml:mi></mml:msup> <mml:msup><mml:mo>∃</mml:mo> <mml:mi>l</mml:mi></mml:msup> </mml:mrow> </mml:math> -safety properties in infinite-state systems. A <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow><mml:msup><mml:mo>∀</mml:mo> <mml:mi>k</mml:mi></mml:msup> <mml:msup><mml:mo>∃</mml:mo> <mml:mi>l</mml:mi></mml:msup> </mml:mrow> </mml:math> -safety property stipulates that for any <i>k</i> traces, there exist <i>l</i> traces such that the resulting <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mrow><mml:mi>k</mml:mi> <mml:mo>+</mml:mo> <mml:mi>l</mml:mi></mml:mrow> </mml:math> traces do not interact badly. This combination of universal and existential quantification captures many properties beyond <i>k</i>-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.