The CTL learning problem consists in finding for a given sample of positive and negative Kripke structures a distinguishing CTL formula that is verified by the former but not by the latter. Further constraints may bound the size and shape of the desired formula or even ask for its minimality in terms of syntactic size. This synthesis problem is motivated by explanation generation for dissimilar models, e.g. comparing a faulty implementation with the original protocol. We devise a SAT-based encoding for a fixed size CTL formula, then provide an incremental approach that guarantees minimality. We further report on a prototype implementation whose contribution is twofold: first, it allows us to assess the efficiency of various output fragments and optimizations. Secondly, we can experimentally evaluate this tool by randomly mutating Kripke structures or syntactically introducing errors in higher-level models, then learning CTL distinguishing formulas.

翻译：CTL学习问题在于：针对给定的正负样例Kripke结构集合，寻找一个能够被前者验证但被后者否定的区分性CTL公式。进一步约束可限制期望公式的规模与形态，甚至要求其达到句法规模意义上的最小化。该综合问题的动机源于不同模型间的解释生成，例如将存在缺陷的实现与原始协议进行比对。我们设计了一种面向固定规模CTL公式的SAT编码方案，随后提供一种可保证最小性的增量式方法。我们还报告了一个原型工具的实现，其贡献具有双重性：首先，它使我们能够评估不同输出片段和优化策略的效率；其次，我们可通过随机变异Kripke结构或在高层模型中句法引入错误后学习CTL区分公式，对该工具进行实验性评估。