**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:

- An efficient
*enumeration*algorithm for directed LTL formulas, which are formulas that can be evaluated only moving forward in words - An algorithm solving the
*Boolean set cover problem*, which constructs Boolean combination of already constructed formulas in order to separate positive and negative examples.

**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:

*Ritam Raha, Rajarshi Roy, NathanaĆ«l Fijalkow, and Daniel Neider.***Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic.***TACAS 22: International Conference on Tools and Algorithms for the Construction and Analysis of Systems.*

preprint