signal-temporal-logic 0.1.2

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

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.