Nathanaël Fijalkow (CNRS, LaBRI, Univ. Bordeaux)

We consider the problem of learning a logical formula from a set of positive and negative examples. The logic we target is Linear Temporal Logic (LTL), a prominent formalism in program verification and analysis, software engineering, and robot motion planning.

We’ll discuss on the one hand theoretical results, in particular NP-completeness, and on the other hand a practical approach, arguing that the problem is a perfect match for GPUs (Graphical Processing Units). No knowledge of LTL or GPU will be required to follow the talk.