We consider the problem of automatically inferring specifications in the branching-time logic, Computation Tree Logic (CTL), from a given system. Designing functional and usable specifications has always been one of the biggest challenges of formal methods. While in recent years, works have focused on automatically designing specifications in linear-time logics such as Linear Temporal Logic (LTL) and Signal Temporal Logic (STL), little attention has been given to branching-time logics despite its popularity in formal methods. We intend to infer concise (thus, interpretable) CTL formulas from a given finite state model of the system in consideration. However, inferring specification only from the given model (and, in general, from only positive examples) is an ill-posed problem. As a result, we infer a CTL formula that, along with being concise, is also language-minimal, meaning that it is rather specific to the given model. We design a counter-example guided algorithm to infer a concise and language-minimal CTL formula via the generation of undesirable models. In the process, we also develop, for the first time, a passive learning algorithm to infer CTL formulas from a set of desirable and undesirable Kripke structures. The passive learning algorithm involves encoding a popular CTL model-checking procedure in the Boolean Satisfiability problem.

翻译：我们考虑从给定系统中自动推断分支时态逻辑——计算树逻辑（CTL）中的规范问题。设计功能性强且可用的规范一直是形式化方法的最大挑战之一。近年来，虽然已有研究聚焦于自动设计线性时态逻辑（如LTL和STL）中的规范，但分支时态逻辑尽管在形式化方法中应用广泛，却鲜受关注。我们的目标是基于给定的系统有限状态模型，推断简洁（因此可解释）的CTL公式。然而，仅从给定模型（以及一般情况下仅从正例）推断规范是一个不适定问题。为此，我们推断的CTL公式在保持简洁的同时，还需具备语言最小性，即该公式应针对给定模型具有特定性。我们设计了一种反例引导算法，通过生成非期望模型来推断简洁且语言最小的CTL公式。在此过程中，我们首次开发了一种被动学习算法，用于从一组期望与非期望的克里普克结构中推断CTL公式。该被动学习算法将经典的CTL模型检测过程编码为布尔可满足性问题。