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.

翻译：时序逻辑是描述系统复杂行为的重要工具。它可用于定义验证与监测所需的属性，以及为综合工具设定目标，使用户能够指定丰富的任务与使命。最常用的时序逻辑包括度量时序逻辑（MTL）、信号时序逻辑（STL）及加权信号时序逻辑（wSTL），这些逻辑还允许定义时序约束。本文介绍PyTeLo——一个基于Python的模块化、多功能软件，旨在简化对时序逻辑语言（特别是MTL、STL和wSTL）的处理。使用PyTeLo仅需提供时序逻辑规范的字符串表示形式，以及（可选）目标系统的动力学信息。PyTeLo通过ANTLR生成的解析器读取规范，并生成捕获公式结构的抽象语法树（AST）。对于综合任务，AST可递归地将规范编码为混合整数线性规划（MILP），并通过Gurobi等商业求解器进行求解。我们阐述了PyTeLo的架构与功能，并通过示例应用展示了其在各类研究问题中的适应性与可扩展性。