一种利用非确定规划的LTL合成方法

LTL Synthesis via Non-deterministic Planning

LTL合成(linear temporal logic synthesis)是程序合成(program synthesis)的一类重要子问题,旨在自动构建一个控制器(controller),且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说,可以将LTL合成定义为二人博弈(two-player game)问题,博弈的双方是环境和控制器,该问题的解称为合成策略.近年来,有研究从理论角度讨论了LTL合成与非确定规划(non-deterministicplanning)的相关性.基于此,提出了一种新的利用非确定规划求解LTL合成问题的方法,并证明了方法的正确性和完备性.具体而言,首先获得LTL公式对应的Büchi自动机,结合二人博弈定义,将LTL合成问题转换为完全可观测的非确定规划模型;然后交由高效规划器求解.通过实验结果说明:与其他LTL合成方法相比,提出的基于规划的合成方法在解质量方面具有较大的优势,能够获得规模较小的合成策略.

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.