Hyperproperties govern the behavior of a system or systems across multiple executions, and are being recognized as an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by modern software model-checking approaches such as IC3/PDR, due to the need to find not only an inductive invariant but also a \emph{total} alignment of different executions that facilitates simpler inductive invariants. We show how this treatment is achieved via a reduction from the verification problem of $\forall^k\exists^l$ properties to Constrained Horn Clauses. The approach is based on combining the inference of an alignment and inductive invariant in a single CHC encoding; and, for existential quantification over traces, incorporating also inference of a witness function for the existential choices, based on a game semantics with a sound-and-complete encoding to CHCs as well.

翻译：超属性控制系统在多次执行中的行为，被认为是常规时序属性的重要扩展。迄今为止，由于不仅需要找到归纳不变式，还需找到促进更简单归纳不变式的不同执行的*完全*对齐，这类属性一直难以由现代软件模型检测方法（如IC3/PDR）进行全面处理。我们展示了如何通过将$\forall^k\exists^l$属性的验证问题归约为约束Horn子句来实现这一处理。该方法基于将对齐推理与归纳不变式推理结合到单一CHC编码中；对于迹上的存在量化，还基于具有可靠且完全CHC编码的博弈语义，融入了存在性选择的见证函数推理。