In this extended abstract, we discuss about Linear Temporal Logic Modulo Theories over finite traces (LTLMTf ), a temporal logic that we recently introduced with the goal of providing an equilibrium between generality of the formalism and decidability of the logic. After recalling its distinguishing features, we discuss some future applications. 2012 ACM Subject Classification Theory of computation → Logic and verification
