Shufang Zhu - Temporal Synthesis with Reachability and Safety Goals
Synthesis from temporal specifications is a fundamental problem in Artificial Intelligence and Computer Science. A popular specification is Linear Temporal Logic (LTL). The standard approach to solving LTL synthesis requires, however, determinization of automata on infinite words and solving parity games, both challenging algorithmic problems. Thus a major barrier of temporal synthesis has been algorithmic difficulty. One approach to combating this difficulty is to focus on using fragments of LTL, for which synthesis problems are simpler. A new logic for temporal synthesis, called LTLf , was proposed recently by De Giacomo and Vardi. The focus there is not on limiting the syntax of LTL, but on interpreting it semantically on finite traces, rather than infinite traces. Such interpretation allows the executions being arbitrarily long, but not infinite, and is adequate for finite-horizon planning problems. While limiting the semantics to finite traces does not change the computational complexity of temporal synthesis (2EXPTIME), the algorithms are much simpler. The reason is that those algorithms require determinization of automata on finite words (rather than infinite words), and solving reachability games (rather than parity games). Another application, is that temporal synthesis of Safety LTL formulas, a syntactic fragment of LTL expressing safety properties, can be reduced to reasoning about finite words. This approach has been implemented in a tool Syft for LTLf synthesis and in SSyft for synthesis of Safety LTL formulas, and has been shown to outperform existing temporal-synthesis tools such as Unbeast and Acacia+.
Short bio: Shufang Zhu is a PhD student in the School of Computer Science and Software Engineering at East China Normal University. She is advised by Prof. Geguang Pu and Prof. Moshe Vardi from Rice University. Her works are in formal verification and synthesis, specifically focusing on developing techniques for synthesis from temporal specifications.