Bounded Synthesis for Past LTL
Peter Wita
Linear-time Temporal Logic (LTL) is a popular specification language to describe the input and output behavior of a system. Its synthesis problem aims for the automatic derivation of an implementation that meets an input LTL formula. To traverse this enormous (and possibly infinite) search space of candidates in a structured manner, Finkbeiner and Schewe introduced the idea of bounded synthesis. Here a given LTL specification is first translated into a universal co-Büchi tree automaton before an implementation of bounded size is guessed and encoded within a constraint system. Past Linear-time Temporal Logic (PLTL) characterizes an extension of LTL, which allows to refer to the past by using additional modalities. A resistance to its inclusion was based on the request of minimality and Gabbay’s Separation Theorem that proves PLTL to add no expressive power by providing a rewriting algorithm of non-elementary complexity. However, recent research has proven that it is more succinct than pure-future LTL. Furthermore, the complexity of its verification problem is still PSPACE-complete. In this thesis, we consider the bounded synthesis problem for PLTL. We present three solutions, each focusing on a different part of the original approach. The first one considers Gabbay’s Separation Theorem and, additionally, presents a complete rewriting of its algorithm. The others describe a partial approach using temporal testers as well as an approach using an algorithm from PLTL to non-deterministic Büchi automata. To evaluate our approaches we additionally compare their efficiency for the famous future(past)-fragment of PLTL.
Master Thesis.