stlpy

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

| <img src="docs/source/images/either_or.png" alt="drawing" width="200"/> |<img src="docs/source/images/nonlinear_reach_avoid.png" alt="drawing" width="200"/> | <img src="docs/source/images/door_puzzle.png" alt="drawing" width="200"/> |<img src="docs/source/images/stepping_stones.png" alt="drawing" width="200"/> | | --- | --- | --- | --- |

Documentation

Can be found online at stlpy.readthedocs.io.

Installation

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

Usage

See the examples and the documentation.

Contributing

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.

Citing stlpy

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.

Stlpy

Install / Use

README