Refinement of TSL Specifications for LTL Synthesis
Jonas Linn
Due to its high complexity, the synthesis problem is still a major challenge to computer science. Even with modern computers, it is barely possible to synthesize reactive systems that handle even small amounts of data using classical synthesis methods. The introduction of Temporal Stream Logic as a specification language is a big step in scalable reactive synthesis. It provides useful abstractions for data handling while being similar to LTL. The synthesis of a TSL specification is possible by generating an under- approximation of the specification in LTL, which is then refined in a CEGAR manner and synthesized by using bounded synthesis. However, the suggested algorithms have not yet been implemented. In this thesis, we optimize the TSL synthesis process for implementation, while also presenting a parallelized version of the algorithm. Furthermore, we propose a way of generating initially stronger underapproximations for speeding up the CEGAR-loop. Additionally, a more generalized way of generating additional assumptions is introduced. Finally, we introduce a set of test specifications on which the implementations are benchmarked.
Bachelor Thesis.