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

摘要：

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

关键词：二人博弈、Büchi自动机、LTL合成、非确定规划

所属期刊栏目：33

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金;国家自然科学基金;国家自然科学基金;国家自然科学基金;中国博士后科学基金;中国博士后科学基金;国家重点研发计划;陕西省重点科技创新团队;陕西省自然科学基础研究计划项目

在线出版日期：2022-08-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共13页

页码：2769-2781