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
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.