  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.
