Abstract:LTL synthesis is an important sub-class of program synthesis. The process of LTL synthesis is to automatically build a controller which interacts with the environment, where the objective is to make the interactive behaviors satisfy a given LTL formula. Generally speaking, LTL synthesis problem is often defined as a two-player game, one player is environment, and the other is controller. The solution of the problem is called synthesis policy. Recently, researchers have investigated that there exists close correspondence between LTL synthesis and non-deterministic planning from a theoretical point of view. This paper presents a novel LTL synthesis approach exploiting non-deterministic planning techniques. Moreover, the correctness and the completeness of the approach is proved formally. Concretely, at first LTL formulas are converted into Büchi automata, then the automata with the two-player game definition of LTL synthesis are translated into full-observable non-deterministic planning models which can be directly fed to existing effective planners. The experimental results show that planning based LTL synthesis has significant advantage over other approaches in improving the quality of solutions, i.e., the size of the obtained policies is much smaller.

Abstract:This paper improves the methods of observation reduction in non-deterministic planning (NDP) in three aspects: in finding MOS (minimal observation set); in finding out the optimal observation set (OOS) when observations have different costs; and in finding fault-tolerant OOS. A MOS problem is similar to a minimal set cover (MSC) problem, so it can be proved that finding MOS is NP-hard. Inspired by MSC methods, an O(2mm2) but Ω(2m?1) algorithm for MOS is presented, where m is the number of observations. By using integer programming (IP) technologies, OOS or fault tolerant OOS can be found out. Proofs are provided to show that these algorithms can guarantee finding optimal solutions.