Logic, Automata, and Games in Linear Temporal Logics on Finite Traces

Temporal logics on finite traces (LTLf, LDLf, PPLTL, etc.) are increasingly attracting the interest of the scientific community. These logics are variants of temporal logics used for specifying dynamic properties in Formal Methods, but focussing on finite though unbounded traces. They are becoming popular in several areas, including AI planning for expressing temporally extended goals, reactive synthesis for automatically synthesizing interactive programs, reinforcement learning for expressing non-Markovian rewards and dynamics, and Business Process Modeling for declaratively specifying processes. These logics can express general safety and guarantee (reachability) properties, though they cannot talk about the behaviors at the infinitum as more traditional temporal logics on infinite traces. The key characteristic of these logics is that they can be reduced to equivalent regular automata, and in turn, automata, once determinized, into two-player games on graphs. This gives them unprecedented computational effectiveness and scalability. In this talk, we will look at these logics, their corresponding automata, and resulting games, and show their relevance in service composition. In particular, we show how they can be used for automatically synthesizing orchestrators for advanced forms of goal-oriented synthesis.