典型文献
一种利用非确定规划的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合成;非确定规划
中图分类号：
作者姓名：
陆旭;于斌;田聪;段振华
作者机构：
西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 710071
文献出处：
引用格式：
[1]陆旭;于斌;田聪;段振华-.一种利用非确定规划的LTL合成方法)[J].软件学报,2022(08):2769-2781
A类：
非确定规划,二人博弈
B类：
LTL,合成方法,linear,temporal,logic,synthesis,程序合成,program,要子,子问题,自动构建,controller,environment,行为交互,一般来说,two,player,game,合成策略,deterministic,planning,规划求解,成问题,完备性,chi,自动机,问题转换,规划模型,交由,规模较
AB值：
0.344164
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
