Linear Temporal Logic was designed to express properties of words in a natural and intuitive way.
The problem
We study the following problem, called the LTL learning problem.
We are given two finite lists of finite words, \(u_1, ..., u_n\) and \(v_1, ..., v_m\), as well as an integer \(k\).
The goal is to determine whether there is an LTL formula of size at most \(k\) satisfied by all \(u_i\) but no \(v_j\).