anand-bala / signal-temporal-logic

A library for efficiently working with Signal Temporal Logic (STL) and its quantitative semantics. Has Python bindings!

This repository has been archived in favor of my other package argus

Signal Temporal Logic Monitoring

This package provides an interface to define offline monitoring for Signal Temporal Logic (STL) specifications. The library is written in C++ (and can be used with CMake) and has been wrapped for Python usage using pybind11.

The library is inspired by the following projects:

• py-metric-temporal-logic is a tool written in pure Python, and provides an elegant interface for evaluating discrete time signals using Metric Temporal Logic (MTL).
• Breach and S-TaLiRo are Matlab toolboxes designed for falsification and simulation-based testing of cyber-physical systems with STL and MTL specifications, respectively. One of their various features includes the ability to evaluate the robustness of signals against STL/MTL.

The signal-temporal-logic library aims to be different from the above in the following ways:

• Written for speed and targets Python.
  • While py-metric-temporal-logic is written in Python, it doesn't perform computations efficiently and quickly.
• Support for multiple quantitative semantics.
  • All the above tools have their own way of computing the quantitative semantics for STL/MTL specifications.
  • This tool will try to support common ways of computing the robustness, but will also have support for other quantitative semantics of STL.

List of Quantitative Semantics

• Classic Robustness
  • A. Donzé and O. Maler, "Robust Satisfaction of Temporal Logic over Real-Valued Signals," in Formal Modeling and Analysis of Timed Systems, Berlin, Heidelberg, 2010, pp. 92–106.
• Temporal Logic as Filtering
  • A. Rodionova, E. Bartocci, D. Nickovic, and R. Grosu, "Temporal Logic As Filtering," in Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, New York, NY, USA, 2016, pp. 11–20.
• Smooth Cumulative Semantics
  • I. Haghighi, N. Mehdipour, E. Bartocci, and C. Belta, "Control from Signal Temporal Logic Specifications with Smooth Cumulative Quantitative Semantics," arXiv:1904.11611 [cs], Apr. 2019.

Installing Python package

Using pip

$ python3 -m pip install signal-temporal-logic

Build from source

Requirements: cmake >= 3.5, git and a C++ compiler that supports C++17.

First clone the repository:

$ git clone https://github.com/anand-bala/signal-temporal-logic

Then install using pip, install the package:

$ python3 -m pip install -U .

Usage

See the examples/ directory for some usage examples in C++ and Python.

signal-temporal-logic's Issues

timed temporal operators

Does the project support timed temporal operators, such as Eventually0, 3, where a = stl.Predicate("a") > 0 ?
Thanks!

Publishing updated wheels for supporting the latest Python versions

Hi, thanks for working on this library :)

The last release (v0.1.3-post1) does not seem to have pre-built libraries in PyPI for the python versions >3.9 and also generating errors when trying to build locally.

I have updated the third party libraries and fixed the build here. Wondering if you can merge this to v0.1.3-post1 and update the packages in PyPI? (maybe with a tag v0.1.3-post2?)

Also wanted to ask if you are planning to further develop this library? (since it has been 2 years since the last update). If not, wondering if you are okay if I can publish a forked versions to PyPI if needed in the future? (e.g. updating packages/quick fixes etc.)

Thanks

Does the python library support implication ( --> )?

I am unable to figure out how to write a statement with implication in python
eg: a --> b

Is there a python binding for implication? An example of how to write that statement in python would be helpful!

Thanks!

Time appending error

My specification is Always(dist & cgap). where dist is the predicate d > 10 and cgap is the predicate d<30. When I try to calculate robustness for the following trace, It fails to do so and gives a time appending error.

Trace: {'dist': (0.0, 20.0989990234375), (1.0, 20.06622314453125), (2.0, 20.0333251953125), (3.0, 20.02685546875), (4.0, 20.0), 'cgap': (0.0, 20.0989990234375), (1.0, 20.06622314453125), (2.0, 20.0333251953125), (3.0, 20.02685546875), (4.0, 20.0)}

error: ValueError: Trying to append a Sample timestamped at or before the Signal end_time,i.e., time is not strictly monotonically increasing.Current end_time is 4.0, given Sample is (4.0, 10.0).