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区分公式方面的性能。