This repository accompanies the paper submitted to L-CSS with ACC "Interval Signal Temporal Logic from Natural Inclusion Functions." The code necessary to generate the figures in our paper is contained in this repository.

This code builds on stlpy. See stlpy's documentation.

Python 3.6 or greater must be installed.
Install the following packages

• numpy
• matplotlib
• scipy
• npinterval

Run python blimp-trace-monitoring.py.

Install the following package

• pypoman (control synthesis only)

Follow the instructions to install gurobi for Python. It is free for academia. Next,

• Clone the stlpy repo
• Replace the file stlpy/solvers/gurobi/gurobi_micp.py with the one in this repo
• Replace stlpy/STL/predicate.py with the one in this repo
• Replace stlpy/STL/formula.py with the one in this repo
• Run python setup.py install from the home directory of the stlpy repo.

Run python double-integrator-interval-control-synthesis.py.

Follow the setup instructions above, except replace stlpy/solvers/gurobi/gurobi_micp.py with gurobi_micp_interval.py.

Run python double-integrator-true-robustness-milp.py for the comparison.

• MikTex or another LaTeX interpreter, for LaTeX to appear in PyPlot plots.