Core Concepts
Counterexamples and explanations for HyperLTL model-checking can be represented as computable Skolem functions for the existentially quantified trace variables.
Abstract
The content discusses two paradigms for computing counterexamples and explanations for HyperLTL model-checking:
- The up-paradigm:
- Restricts to ultimately periodic traces, which are finitely representable.
- Computes restrictions of Skolem functions to ultimately periodic inputs.
- Is complete, i.e., if a transition system T satisfies a HyperLTL formula ϕ, then there exists an explanation in the up-paradigm.
- However, the up-paradigm is limited to ultimately periodic traces and does not provide continuous explanations.
- The cs-paradigm:
- Works with computable Skolem functions, which are more general than the up-paradigm.
- Computable Skolem functions can be implemented by bounded-delay transducers, a simpler machine model than Turing machines.
- Continuity of computable Skolem functions is a desirable property, as it ensures that settled outputs are never revoked.
- However, the cs-paradigm is incomplete, i.e., there are pairs (T, ϕ) with T satisfying ϕ that do not have computable explanations.
- The authors show that it is decidable whether a given pair (T, ϕ) has a computable explanation, and provide an algorithm to compute such explanations if they exist.
The key insight is that computing counterexamples/explanations for HyperLTL model-checking can be formulated as a uniformization problem, which has been studied in the context of transducer synthesis.