HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we introduce two paradigms to compute counterexamples and explanations for HyperLTL model-checking, thereby considerably increasing its usefulness. Both paradigms are based on the maxim ``counterexamples/explanations are Skolem functions for the existentially quantified trace variables''. Our first paradigm is complete (everything can be explained), but restricted to ultimately periodic system traces. The second paradigm works with (Turing machine) computable Skolem functions and is therefore much more general, but also shown incomplete (not everything can computably be explained). Finally, we prove that it is decidable whether a given finite transition system and a formula have computable Skolem functions witnessing that the system satisfies the formula. Our algorithm also computes transducers implementing computable Skolem functions, if they exist.

翻译：HyperLTL模型检验能够对安全关键系统的信息流属性进行自动化验证，但仅提供二元结果。本文提出两种计算HyperLTL模型检验反例与解释的范式，从而显著提升其实用性。两种范式均基于"反例/解释是存在量化迹变量的斯科伦函数"这一准则。第一个范式具有完备性（所有内容均可被解释），但仅适用于最终周期性的系统迹。第二个范式基于（图灵机）可计算的斯科伦函数，因此更具普适性，但已被证明不完备（并非所有内容均可通过计算得到解释）。最后，我们证明：给定有限迁移系统与公式，判断是否存在可计算斯科伦函数验证该系统满足该公式是可知的。若存在此类函数，我们的算法还可生成实现可计算斯科伦函数的转换器。