A Flexible and Efficient Temporal Logic Tool for Python: PyTeLo
Gustavo A. Cardona, Kevin Leahy, Makai Mann, and Cristian-Ioan Vasile

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.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Model-Driven Software Engineering Techniques
