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.

翻译：在运行时验证中，手动形式化用于监控系统执行的规范是一项繁琐且易错的过程。为解决此问题，我们研究了从系统执行中自动合成形式化规范的问题。为展示我们的方法，我们采用广泛使用的规范语言——度量时态逻辑（Metric Temporal Logic, MTL），该语言特别适用于网络物理系统（CPS）的时序属性描述。合成时态逻辑公式的经典方法大多致力于最小化公式的规模。然而，在监控效率方面，除了公式规模外，规范所需的"前瞻量"也变得重要，尤其在安全关键应用中。我们形式化了这一概念，并设计了一种学习算法，可合成具有有界前瞻量的简洁公式。为此，该算法将合成任务转化为一系列线性实数算术（Linear Real Arithmetic, LRA）的可满足性问题，并基于满足赋值生成MTL公式。该转化通过一种基于LRA对经典MTL监控流程的新型编码实现。最后，我们将该算法实现为名为TEAL的工具，并在CPS应用中验证了其合成可高效监控MTL公式的能力。