Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
This addresses the tedious and error-prone manual specification process in runtime verification for safety-critical cyber-physical systems, but it is incremental as it builds on existing synthesis approaches by optimizing for monitoring efficiency.
The paper tackles the problem of automatically synthesizing formal specifications from system executions in runtime verification, focusing on Metric Temporal Logic (MTL) for cyber-physical systems, and presents an algorithm that synthesizes concise formulas with bounded lookahead, implemented in a tool called TEAL.
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.