Core Concepts
The core message of this article is to devise a SAT-based encoding for learning a minimal Computation Tree Logic (CTL) formula that distinguishes a given sample of positive and negative Kripke structures.
Abstract
The article addresses the problem of passive learning of Computation Tree Logic (CTL) formulas from a sample of positive and negative Kripke structures. The key highlights and insights are:
The authors prove that a CTL formula consistent with the sample always exists, and they provide an explicit construction to compute such a formula, though it may not be minimal.
To find a minimal distinguishing CTL formula, the authors reduce the bounded learning problem (finding a CTL formula of size at most n that is consistent with the sample) to a Boolean satisfiability (SAT) problem. They provide a SAT encoding that captures the bounded semantics of CTL.
The authors propose a bottom-up algorithm that iteratively solves the bounded learning problem with increasing bounds to find the minimal solution.
Several optimizations are introduced, including embedding negations in the syntactic tree and approximating the recurrence diameter of the Kripke structures to reduce the size of the SAT instances.
The authors implement a prototype tool and evaluate its performance on a benchmark suite, demonstrating the effectiveness of the proposed techniques.