LTL Synthesis via Non-deterministic Planning
Author:
Affiliation:

Clc Number:

TP311

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 02,2021
  • Revised:October 14,2021
  • Adopted:
  • Online: January 28,2022
  • Published: August 06,2022
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063