A Flexible and Efficient Temporal Logic Tool for Python: PyTeLo

TL;DR

PyTeLo is a Python tool that simplifies working with temporal logic specifications like MTL, STL, and wSTL, enabling system verification, monitoring, and synthesis through an easy-to-use interface and MILP encoding.

Contribution

The paper introduces PyTeLo, a modular Python software that supports multiple temporal logics and automates the translation of specifications into MILP for system synthesis.

Findings

PyTeLo effectively encodes temporal logic specifications into MILP.

It supports MTL, STL, and wSTL with a user-friendly interface.

Example applications demonstrate its flexibility and extensibility.

Abstract

Temporal logic is an important tool for specifying complex behaviors of systems. It can be used to define properties for verification and monitoring, as well as goals for synthesis tools, allowing users to specify rich missions and tasks. Some of the most popular temporal logics include Metric Temporal Logic (MTL), Signal Temporal Logic (STL), and weighted STL (wSTL), which also allow the definition of timing constraints. In this work, we introduce PyTeLo, a modular and versatile Python-based software that facilitates working with temporal logic languages, specifically MTL, STL, and wSTL. Applying PyTeLo requires only a string representation of the temporal logic specification and, optionally, the dynamics of the system of interest. Next, PyTeLo reads the specification using an ANTLR-generated parser and generates an Abstract Syntax Tree (AST) that captures the structure of the formula. For synthesis, the AST serves to recursively encode the specification into a Mixed Integer Linear Program (MILP) that is solved using a commercial solver such as Gurobi. We describe the architecture and capabilities of PyTeLo and provide example applications highlighting its adaptability and extensibility for various research problems.