A Flexible and Efficient Temporal Logic Tool for Python: PyTeLo

要約

時間論理は、システムの複雑な動作を指定するための重要なツールです。
これを使用して検証と監視のプロパティを定義したり、合成ツールの目標を定義したりできるため、ユーザーは豊富なミッションとタスクを指定できます。
最も一般的な時相ロジックには、メトリック時相ロジック (MTL)、信号時相ロジック (STL)、および重み付き STL (wSTL) が含まれており、タイミング制約の定義も可能です。
この作業では、時相論理言語、特に MTL、STL、wSTL の操作を容易にするモジュール式の多用途 Python ベース ソフトウェアである PyTeLo を紹介します。
PyTeLo を適用するには、時相論理仕様の文字列表現と、必要に応じて、対象のシステムのダイナミクスのみが必要です。
次に、PyTeLo は、ANTLR で生成されたパーサーを使用して仕様を読み取り、式の構造をキャプチャする抽象構文ツリー (AST) を生成します。
合成の場合、AST は仕様を混合整数線形計画 (MILP) に再帰的にエンコードする役割を果たします。MILP は、Gurobi などの市販のソルバーを使用して解決されます。
PyTeLo のアーキテクチャと機能について説明し、さまざまな研究問題に対するその適応性と拡張性を強調するアプリケーション例を提供します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google