About

stlpy is a python library for control from Signal Temporal Logic (STL) specifications.

This software is designed with the following goals in mind:

If this software is helpful to you, if you have a new synthesis method you would like to see included in the package, or if you have any questions, feel free to reach out.

Signal Temporal Logic

Signal Temporal Logic (STL) is a formal language that can be used to define complex control objectives for robotic and cyber-physical systems. STL is similar to boolean logic in that it includes boolean operators like “and” (\(\land\)), “or” (\(\lor\)) and “not” (\(\lnot\)), but it also includes some special temporal operators like “always/globally” (\(G_{[t_1,t_2]}\)), “eventually/finally” (\(F_{[t_1,t_2]}\)), and “until” (\(U_{[t_1,t_2]}\)).

As the name suggests, STL is defined over continuous-valued signals:

\[y = y_0,y_1,y_2,\dots,y_T,\]

where \(y_t \in \mathbb{R}^p\) is the value of the signal at timestep \(t\).

Note

This software focuses on discrete-time signals of finite length, though STL is also well-defined for infinitely long and continuous-time signals.

The fundamental building blocks of STL are predicates \(\pi\), defined by inequalities

\[\pi = ( g^{\pi}(y) > 0 )\]

Many (though not all) STL synthesis algorithms require linear predicates, i.e., \(g^{\pi}(y) = a y - b\).

STL Syntax

The syntax of STL defines what counts as a valid STL formula. In short form, STL’s synatax is

\[\varphi = \pi \mid \lnot \varphi \mid \bigvee_i \varphi_i \mid \bigwedge_i \varphi_i \mid G_{[t_1,t_2]} \varphi \mid F_{[t_1,t_2]} \varphi \mid \varphi_1 U_{[t_1,t_2]} \varphi_2\]

This essentially means that:

  • All predicates \(\pi\) are valid STL formulas.

  • Given an STL formula \(\varphi\), its negation \(\lnot \varphi\) is also a valid STL formula.

  • The conjunction (“and”, \(\land\)) of multiple STL formulas is a valid STL formula.

  • The disjunction (“or”, \(\lor\)) of multiple STL formulas is a valid STL formula.

  • Given an STL formula \(\varphi\), \(G_{[t_1,t_2]} \varphi\) (always \(\varphi\)) is also a valid STL formula.

  • Given an STL formula \(\varphi\), \(F_{[t_1,t_2]} \varphi\) (eventually \(\varphi\)) is also a valid STL formula.

  • Given two STL formulas \(\varphi_1\) and \(\varphi_2\), \(\varphi_1 U_{[t_1,t_2]} \varphi_2\) (\(\varphi_1\) until \(\varphi_2\)) is also a valid STL formula.

STL Semantics

As with any formal language, while the syntax defines what counts as a formula, the semantics defines what a formula means. Here we’ll present a fairly inutitive explanation of the semantics:

  • Saying that a signal satisfies a specification (\(y \vDash \varphi\)) is equivalent to saying that the first timestep of the signal satisfies the specification.

  • Predicates: \(\pi\) holds if the inequality \(g^{\pi}(y) > 0\) holds.

  • Conjunction: \(\varphi_1 \land \varphi_2\) holds if both subformulas hold.

  • Disjunction: \(\varphi_1 \lor \varphi_2\) holds if at least one of the subformulas holds.

  • Always: \(G_{[t_1,t_2]} \varphi\) holds if \(\varphi\) holds at all timesteps between \(t_1\) and \(t_2\).

  • Eventually: \(F_{[t_1,t_2]} \varphi\) holds if \(\varphi\) holds at at least one timestep between \(t_1\) and \(t_2\).

  • Until: \(\varphi_1 U_{[t_1,t_2]} \varphi_2\) holds if \(\varphi_2\) holds at some timestep between \(t_1\) and \(t_2\), and \(\varphi_1\) holds before that point.

Note

A more rigorous recursive definition of the STL semantics can be found in most STL-related papers.

STL is also equipped with a “robustness measure” \(\rho^{\varphi}(y)\). This is a function that maps a signal to a scalar value. \(\rho\) is positive only if the signal satisfies the specification, and negative only if the signal does not satisfy the specification. The robustness measure allows us to consider “more satisfying” signals and “closer-to-satisfying” signals, which is very useful for optimization.

This software provides tools for working with STL formulas, including computation of the robustness measure. See this example for more details.

STL for Control

STL becomes particularly useful when we consider the signal \(y\) to be the output of a dynamical system:

\[ \begin{align}\begin{aligned}x_{t+1} = f(x_t, u_t),\\y_t = g(x_t, u_t),\end{aligned}\end{align} \]

where \(x_t\) is the system state and \(u_t\) is a control input.

In this context, STL specifications formally define some desired behavior for the system. Such specifications can become quite complicated (see the Benchmarks for some examples).

One thing we might like to do is find a sequence of control inputs such that the resulting output trajectory satisfies the specification: this is the trajectory synthesis problem.

STL trajectory synthesis is an NP-hard problem, and efficient algorithms remain an area of active research. This software provides high-quality implementations of several state-of-the-art algorithms as well as an interface for designing new algorithms.

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={IEEE Control Systems Letters},
  year={2022},
  publisher={IEEE}
}

References for specific synthesis methods can be found in the solver documentation.