Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic

要約

実行時検証において、システム実行を監視するための仕様を手動で形式化するのは、面倒でエラーが発生しやすいプロセスです。
この問題に対処するために、システムの実行から正式な仕様を自動的に合成する問題を検討します。
私たちのアプローチを実証するために、サイバーフィジカル システム (CPS) の時間プロパティを指定するために特に調整された、一般的な仕様言語メトリック テンポラル ロジック (MTL) を検討します。
時相論理式を合成するための古典的なアプローチのほとんどは、式のサイズを最小限に抑えることを目的としています。
ただし、特に安全性が重要なアプリケーションの場合、サイズとともに監視の効率を高めるために、仕様に必要な「先読み」の量が重要になります。
私たちはこの概念を形式化し、有界先読みを持つ簡潔な式を合成する学習アルゴリズムを考案します。
これを行うために、私たちのアルゴリズムは合成タスクを線形実数演算 (LRA) の一連の充足可能性問題に落とし込み、それらの満足のいく代入から MTL 式を生成します。
この削減には、LRA を使用した一般的な MTL モニタリング手順の新しいエンコーディングが使用されます。
最後に、TEAL と呼ばれるツールにアルゴリズムを実装し、CPS アプリケーションで効率的に監視可能な MTL 式を合成する機能を実証します。

要約(オリジナル)

In runtime verification, manually formalizing a specification for monitoring system executions is a tedious and error-prone process. To address this issue, we consider the problem of automatically synthesizing formal specifications from system executions. To demonstrate our approach, we consider the popular specification language Metric Temporal Logic (MTL), which is particularly tailored towards specifying temporal properties for cyber-physical systems (CPS). Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. However, for efficiency in monitoring, along with the size, the amount of ‘lookahead’ required for the specification becomes relevant, especially for safety-critical applications. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead. To do so, our algorithm reduces the synthesis task to a series of satisfiability problems in Linear Real Arithmetic (LRA) and generates MTL formulas from their satisfying assignments. The reduction uses a novel encoding of a popular MTL monitoring procedure using LRA. Finally, we implement our algorithm in a tool called TEAL and demonstrate its ability to synthesize efficiently monitorable MTL formulas in a CPS application.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google