We address the problem of learning temporal properties from the branching-time behavior of systems. Existing research in this field has mostly focused on learning linear temporal properties specified using popular logics, such as Linear Temporal Logic (LTL) and Signal Temporal Logic (STL). Branching-time logics such as Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL), despite being extensively used in specifying and verifying distributed and multi-agent systems, have not received adequate attention. Thus, in this paper, we investigate the problem of learning CTL and ATL formulas from examples of system behavior. As input to the learning problems, we rely on the typical representations of branching behavior as Kripke structures and concurrent game structures, respectively. Given a sample of structures, we learn concise formulas by encoding the learning problem into a satisfiability problem, most notably by symbolically encoding both the search for prospective formulas and their fixed-point based model checking algorithms. We also study the decision problem of checking the existence of prospective ATL formulas for a given sample. We implement our algorithms in an Python prototype and have evaluated them to extract several common CTL and ATL formulas used in practical applications.

翻译：本文研究从系统分支时序行为中学习时序性质的问题。该领域现有研究主要集中于学习使用常见逻辑（如线性时序逻辑LTL与信号时序逻辑STL）描述的线性时序性质。尽管分支时序逻辑（如计算树逻辑CTL与交替时序逻辑ATL）在分布式与多智能体系统的规约与验证中已被广泛应用，却尚未获得足够关注。为此，本文探究从系统行为示例中学习CTL与ATL公式的问题。针对学习问题的输入，我们分别采用克里普克结构与并发博弈结构作为分支行为的典型表示形式。给定一组结构样本，我们将学习问题编码为可满足性问题，特别是通过符号化编码对候选公式的搜索及其基于不动点的模型检测算法，从而学习简洁的公式。我们还研究了针对给定样本检验候选ATL公式存在性的判定问题。我们在Python原型中实现了相关算法，并通过提取实际应用中常见的若干CTL与ATL公式进行了评估。