一种利用非确定规划的LTL合成方法
作者:
作者单位:

作者简介:

陆旭(1985-),男,博士,副教授,CCF专业会员,主要研究领域为智能规划,模型检测,程序验证;
田聪(1981-),女,博士,教授,博士生导师,CCF杰出会员,主要研究领域为可信软件的基础理论与方法,人工智能系统安全;
于斌(1990-),男,博士,讲师,CCF专业会员,主要研究领域为模型检测,运行时验证;
段振华(1948-),男,博士,教授,博士生导师,CCF会士,主要研究领域为时序逻辑,形式化方法,高可信嵌入式系统.

通讯作者:

于斌,E-mail:byu@xidian.edu.cn;田聪,E-mail:ctian@mail.xidian.edu.cn;段振华,E-mail:zhhduan@mail.xidian.edu.cn

中图分类号:

TP311

基金项目:

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


LTL Synthesis via Non-deterministic Planning
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

陆旭,于斌,田聪,段振华.一种利用非确定规划的LTL合成方法.软件学报,2022,33(8):2769-2781

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-02
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号