Learning Branching-Time Properties in CTL and ATL via Constraint Solving

TL;DR

The paper tackles learning branching-time properties by automatically inducing CTL and ATL formulas from samples of Kripke and concurrent game structures. It introduces a SAT-based framework that encodes both the prospective formula structure and its fixed-point model-checking semantics into a single propositional formula $\Omega^{\mathcal{S}}_n$, enabling iterative discovery of minimal consistent formulas. A key theoretical contribution is the polynomial-time decidability of separability for full ATL and exponential-time decidability for any ATL fragment, along with exponential bounds on formula size. Empirically, the authors implement a Python prototype and demonstrate that their method can extract common CTL/ATL formulas from synthetic benchmarks, highlighting runtime insights and optimization opportunities for the encoding. This work advances automatic specification learning for branching-time logics and provides a scalable, interpretable path toward generating concise ATL/CTL descriptions for distributed and multi-agent systems.

Abstract

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.

Figures (5)

• Figure 1: Syntax DAG with identifiers (indicated above nodes) of $\langle\!\langle2\rangle\!\rangle\!\mathop{\mathrm{\mathbf{X}}}\nolimits p \lor \langle\!\langle1\rangle\!\rangle(p \mathop{\mathrm{\mathbf{U}}}\nolimits \langle\!\langle1,\!3\rangle\!\rangle\!\mathop{\mathrm{\mathbf{G}}}\nolimits q )$.
• Figure 2: Runtime of CTL and ATL learning algorithms on samples with varying number of examples (considering structures of size $\leq 20$).
• Figure 3: Runtime improvement with optimized encodings for CTL and ATL learning on first and second benchmark suites, respectively. The runtimes are in seconds and “ TO” represents timeout.
• Figure 4: Runtime of CTL and ATL learning algorithms on samples with varying number of examples (considering structures of size $\leq 20$).
• Figure 5: Runtime of CTL and ATL learning algorithms on samples with varying size of structures (considering number of examples $\leq 40$).

Theorems & Definitions (56)

• Definition 1
• Definition 2
• Remark 3
• Definition 5
• Proposition 6
• Theorem 7
• Definition 8
• Lemma 9
• Definition 10
• Definition 11