OLTL: An Optimization Extension of Linear Temporal Logic

Linear Temporal Logic (LTL) can be used for problem-solving when all problem constraints can be specified in this logic through the use of satisfiability checking techniques. In optimization problems such as scheduling with preferences, where constraints are primarily temporal, LTL is a desirable specification formalism. However, LTL cannot be used as a standalone formalism due to the fact that it is unable to specify soft constraints. This article introduces Optimization LTL (OLTL), an optimization-oriented extension of LTL that can specify both hard and soft constraints in optimization problems. The syntax, semantics and basic formal properties of this logic are presented, along with an encoding based on bit-vector logic and Linear Real Arithmetic (LRA). Additionally, a tool called LiTeLLab (Linear Temporal Logic Laboratory) is introduced to solve optimization problems specified by OLTL. The feasibility and scalability of using OLTL as a specification formalism is demonstrated through two case studies. These problems, with multiple optimization parameters, are specified in OLTL and LiTeLLab successfully generates optimal solutions.