A python library for control from Signal Temporal Logic (STL) specifications.
Includes implementations of several state-of-the-art synthesis algorithms and benchmark specifications (shown below).
Can be found online at stlpy.readthedocs.io.
pip install stlpy
The basic installation allows for defining and evaluating STL formulas. The more advanced solvers require one or more of the following additional packages. See the documentation for more details.
- scipy (for gradient-based optimization)
- Drake with Gurboi/Mosek enabled (for MICP-based optimization)
- Drake with SNOPT enabled (for smooth optimization with sparse SQP)
- Gurobi python bindings (version 9.0 or higher) for MICP-based optimization
See the examples and the documentation.
If you have a new STL trajectory synthesis algorithm or benchmark scenario you would like to see included in this package, please open a pull request.
To reference stlpy in academic research, please cite our paper:
@article{kurtz2022mixed,
title={Mixed-Integer Programming for Signal Temporal Logic with Fewer Binary Variables},
author={Kurtz, Vince and Lin, Hai},
journal={arXiv preprint arXiv:2204.06367},
year={2022}
}
References for specific synthesis methods can be found in the solver documentation.