Scarlet

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.

Documentation

We refer to the Github README for a documentation.

Contact

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

Citing

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