Synthesizing Controllers: On the Correspondence Between LTL Synthesis and Non-deterministic Planning.

Linear Temporal Logic ((mathsf {LTL})) synthesis can be understood as the problem of building a controller that defines a winning strategy, for a two-player game against the environment, where the objective is to satisfy a given (mathsf {LTL}) formula. It is an important problem with applications in software synthesis, including controller synthesis. In this paper we establish the correspondence between (mathsf {LTL}) synthesis and fully observable non-deterministic (FOND) planning. We study (mathsf {LTL}) interpreted over both finite and infinite traces. We also provide the first explicit compilation that translates an (mathsf {LTL}) synthesis problem to a FOND problem. Experiments with state-of-the-art (mathsf {LTL}) FOND and synthesis solvers show automated planning to be a viable and effective tool for highly structured (mathsf {LTL}) synthesis problems.