一种利用非确定规划的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:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [27]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    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.

    参考文献
    [1] Church A.Applications of recursive arithmetic to the problem of circuit synthesis.Journal of Symbolic Logic, 1963, 28(4):289-290.[doi:10.2307/2271310]
    [2] Pnueli A, Rosner R.On the synthesis of a reactive module.In:Proc.of the 16th Annual ACM Symp.on Principles of Programming Languages (POPL'89).ACM, 1989.179-190.[doi:10.1145/75277.75293]
    [3] Piterman N, Pnueli A, Sa'ar Y.Synthesis of reactive (1) designs.In:Emerson EA, Namjoshi KS, eds.Proc.of the 7th Int'l Conf.on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006).Springer, 2006.364-380.[doi:10.1007/11609773_24]
    [4] Bohy A, Bruyère V, Filiot E, et al.Acacia+:Atool for LTLsynthesis.In:Madhusudan P, Seshia SA, eds.Proc.of the 24th Int'l Conf.on Computer Aided Verification (CAV 2012).Springer, 2012.652-657.[doi:10.1007/978-3-642-31424-7_45]
    [5] Jobstmann B, Bloem R.Optimizations for LTL synthesis.In:Proc.of the 6th Int'l Conf.on Formal Methods in Computer-Aided Design (FMCAD 2006).IEEE Computer Society, 2006.117-124.[doi:10.1109/FMCAD.2006.22]
    [6] Camacho A, Muise C, Baier JA, et al.LTL realizability via safety and reachability games.In:Lang J, ed.Proc.of the 27th Int'l Joint Conf.on Artificial Intelligence (IJCAI 2018).2018.4683-4691.[doi:10.24963/ijcai.2018/651]
    [7] Michaud T, Colange M.Reactive synthesis from LTL specification with Spot.In:Proc.of the 7th Workshop on Synthesis (SYNT 2018).2018.
    [8] Zhu SF, Tabajara LM, Li JW, et al.A symbolic approach to safety LTLsynthesis.In:Strichman O, Tzoref-Brill R, eds.Proc.of the 13th Int'l Haifa Verification Conf.(HVC 2017).Springer, 2017.147-162.[doi:10.1007/978-3-319-70389-3_10]
    [9] Li JW, Zhang LJ, Pu GG, et al.LTLf satisfiability checking.In:Schaub T, Friedrich G, O'Sullivan B, eds.Proc.of the 21st European Conf.on Artificial Intelligence (ECAI 2014).IOS, 2014.513-518.[doi:10.3233/978-1-61499-419-0-513]
    [10] Giacomo GD, Vardi MY.Synthesis for LTL and LDL on finite traces.In:Yang Q, Wooldridge MJ, eds.Proc.of the 24th Int'l Joint Conf.on Artificial Intelligence (IJCAI 2015).AAAI, 2015.1558-1564.
    [11] Zhu SF, Tabajara LM, Li JW, et al.Symbolic LTLf synthesis.In:Sierra C, ed.Proc.of the 26th Int'l Joint Conf.on Artificial Intelligence (IJCAI 2017).2017.1362-1369.[doi:10.24963/ijcai.2017/189]
    [12] He KL, Wells AM, Kavraki LE, et al.Efficient symbolic reactive synthesis for finite-horizon tasks.In:Proc.of the Int'l Conf.on Robotics and Automation (ICRA 2019).IEEE, 2019.8993-8999.[doi:10.1109/ICRA.2019.8794170]
    [13] He KL, Lahijanian M, Kavraki LE, et al.Reactive synthesis for finite tasks under resource constraints.In:Proc.of the 2017 IEEE/RSJ Int'l Conf.on Intelligent Robots and Systems (IROS 2017).IEEE, 2017.5326-5332.[doi:10.1109/IROS.2017.8206426]
    [14] Zhu SF, Giacomo GD, Pu GG, et al.LTLf synthesis with fairness and stability assumptions.In:Proc.of the 34th AAAI Conf.on Artificial Intelligence (AAAI 2020).AAAI, 2020.3088-3095.[doi:10.1609/aaai.v34i03.5704]
    [15] Giacomo GD, Stasio AD, Vardi MY, et al.Two-stage technique for LTLf synthesis under LTL assumptions.In:Calvanese D, Erdem E, Thielscher M, eds.Proc.of the 17th Int'l Conf.on Principles of Knowledge Representation and Reasoning (KR 2020).2020.304-314.[doi:10.24963/kr.2020/31]
    [16] Ghallab M, Nau D, Traverso P.Automated Planning-Theory and Practice.Elsevier, 2004.1-635.
    [17] Camacho A, Baier JA, Muise C, et al.Finite LTL synthesis as planning.In:de Weerdt M, Koenig S, Röger G, Spaan MTJ, eds.Proc.of the 28th Int'l Conf.on Automated Planning and Scheduling (ICAPS 2018).AAAI, 2018.29-38.
    [18] Camacho A, Bienvenu M, McIlraith SA.Towards a unified view of AI planning and reactive synthesis.In:Benton J, Lipovetzky N, Onaindia E, Smith DE, Srivastava S, eds.Proc.of the 29th Int'l Conf.on Automated Planning and Scheduling (ICAPS 2019).AAAI, 2019.58-67.
    [19] Camacho A, Baier JA, Muise C, et al.Bridging the gap between LTL synthesis and automated planning.In:Proc.of the Workshop Generalized Planning.2017.1-10.
    [20] D'Ippolito N, Rodriguez N, Sardina S.Fully observable non-deterministic planning as assumption-based reactive synthesis.Journal of Artificial Intelligence Research, 2018, 61:593-621.[doi:10.1613/jair.5562]
    [21] Blai B, Giuseppe DG, Hector G, et al.High-level programming via generalized planning and LTL synthesis.In:Calvanese D, Erdem E, Thielscher M, eds.Proc.of the 17th Int'l Conf.on Principles of Knowledge Representation and Reasoning (KR 2020).2020.152-161.[doi:10.24963/kr.2020/16]
    [22] Raman V, Donze A, Sadigh D, et al.Reactive synthesis from signal temporal logic specifications.In:Girard A, Sankaranarayanan S, eds.Proc.of the 18th Int'l Conf.on Hybrid Systems:Computation and Control (HSCC 2015).ACM, 2015.239-248.[doi:10.1145/2728606.2728628]
    [23] Vardi MY, Wolper P.Reasoning about infinite computations.Information and Computation, 1994, 115(1):1-37.[doi:10.1006/inco.1994.1092]
    [24] Geffner H, Bonet B.A concise introduction to models and methods for automated planning.In:Proc.of the Synthesis Lectures on Artificial Intelligence and Machine Learning.Morgan&Claypool Publishers, 2013.1-141.[doi:10.2200/S00513ED1V01Y 201306AIM022]
    [25] Zielonka W.Infinite games on finitely coloured graphs with applications to automata on infinite trees.Theoretical Computer Science, 1998, 200(1-2):135-183.[doi:10.1016/S0304-3975(98)00009-7]
    [26] Muise C, McIlraith SA, Beck JC.Improved non-deterministic planning by exploiting state relevance.In:McCluskey L, Williams BC, Silva JR, Bonet B, eds.Proc.of the 22nd Int'l Conf.on Automated Planning and Scheduling (ICAPS 2012).AAAI, 2012.172-180.
    [27] Gastin P, Oddoux D.Fast LTL to Büchi automata translation.In:Berry G, Comon H, Finkel A, eds.Proc.of the 13th Int'l Conf.on Computer Aided Verification (CAV 2001).Springer, 2001.53-65.[doi:10.1007/3-540-44585-4_6]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

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

京公网安备 11040202500063号