# Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic

arXiv: https://arxiv.org/abs/2310.17410 · HTML: https://mlsanity.com/paper/2310.17410/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 51 references that are in the map.
- First posted on arXiv 26 Oct 2023.

## Builds on (most cited first, 10 of 10)

- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [Robust Online Monitoring of Signal Temporal Logic](https://mlsanity.com/paper/1506.08234/) (2015)
- [Transfer of Temporal Logic Formulas in Reinforcement Learning](https://mlsanity.com/paper/1909.04256/) (2019)
- [Mining Parametric Temporal Logic Properties in Model Based Design for Cyber-Physical Systems](https://mlsanity.com/paper/1512.07956/) (2015)
- [On-Line Monitoring for Temporal Logic Robustness](https://mlsanity.com/paper/1408.0045/) (2014)
- [The Complexity of Learning Linear Temporal Formulas from Examples](https://mlsanity.com/paper/2102.00876/) (2021)
- [A Robust Genetic Algorithm for Learning Temporal Specifications from Data](https://mlsanity.com/paper/1711.06202/) (2017)
- [Learning Interpretable Models in the Property Specification Language](https://mlsanity.com/paper/2002.03668/) (2020)
- [Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach](https://mlsanity.com/paper/2104.15083/) (2021)
- [Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic](https://mlsanity.com/paper/2110.06726/) (2021)

## Built on by (most cited first, 3 of 3)

- [Learning temporal formulas from examples is hard](https://mlsanity.com/paper/2312.16336/) (2023)
- [Automata Learning of Preferences over Temporal Logic Formulas from Pairwise Comparisons](https://mlsanity.com/paper/2505.18030/) (2025)
- [On Synthesis of Metric Interval Temporal Logics](https://mlsanity.com/paper/2609.01032/) (2026)

## Abstract (arXiv)

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.