Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic

TL;DR

This paper introduces a method for automatically synthesizing concise Metric Temporal Logic formulas with bounded lookahead, enhancing runtime verification efficiency for cyber-physical systems.

Contribution

It presents a novel learning algorithm that reduces MTL formula synthesis to satisfiability problems in Linear Real Arithmetic, focusing on monitorability and efficiency.

Findings

Successfully synthesizes monitorable MTL formulas in CPS

Reduces synthesis to satisfiability problems in LRA

Implemented in the TEAL tool demonstrating practical effectiveness

Abstract

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.