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区分公式，我们可对该工具进行实验性评估。