Scarlet logo


Tool solving the problem of learning LTL formulas from positive and negative examples over finite traces.

Scarlet is a tool for constructing LTL formulas over finite traces from a set of positive and negative examples.

We believe that the path to scalability for LTL learning is to leverage normal forms for LTL formulas and derive efficient enumeration algorithms from them. Scarlet combines two insights:

Scarlet was written in Python by Ritam Raha and Rajarshi Roy.


We refer to the Github README for a documentation.


For questions, suggestions and comments, you may contact Ritam, Rajarshi, Nathanaƫl, and Daniel. Contributions are most welcome!


Cite Scarlet in academic publications as: