# SAT-based Learning of Computation Tree Logic

arXiv: https://arxiv.org/abs/2402.06366 · HTML: https://mlsanity.com/paper/2402.06366/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Feb 2024.

## Built on by (most cited first, 4 of 4)

- [Learning Probabilistic Temporal Logic Specifications for Stochastic Systems](https://mlsanity.com/paper/2505.12107/) (2025)
- [SAT-Based Bounded Fitting for the Description Logic ALC](https://mlsanity.com/paper/2507.21752/) (2025)
- [Automata Learning of Preferences over Temporal Logic Formulas from Pairwise Comparisons](https://mlsanity.com/paper/2505.18030/) (2025)
- [Bounded Fitting for Expressive Description Logics](https://mlsanity.com/paper/2605.07452/) (2026)

## Abstract (arXiv)

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.