软件学报

作者：陆旭，于斌，田聪，段振华

单位：陆旭，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007111,于斌，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007102,田聪，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007103,段振华，西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 71007104

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

基金：国家自然科学基金(61806158,61732013,62172322,62002290);中国博士后科学基金(2019T120881,2018M643585);国家重点研发计划(2018AAA0103202);陕西省重点科技创新团队(2019TD-001);陕西省自然科学基础研究计划(2021JQ-208)

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

来源：2022年第8期

《软件学报》期刊编辑部

查看软件学报杂志2022年第8期