Tracy, Traces, and Transducers: Computable Counterexamples and Explanations for HyperLTL Model-Checking
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要