Synthesis for LTL and LDL on Finite Traces

被引：0
|
作者：
De Giacomo, Giuseppe [1 ]
Vardi, Moshe Y. [2 ]
机构：
[1] Sapienza Univ Roma, Rome, Italy
[2] Rice Univ, Houston, TX USA
来源：
PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI) | 2015年
基金：
美国国家科学基金会;
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
In this paper, we study synthesis from logical specifications over finite traces expressed in LTL (f) and its extension LDL (f). Specifically, in this form of synthesis, propositions are partitioned in controllable and uncontrollable ones, and the synthesis task consists of setting the controllable propositions over time so that, in spite of how the value of the uncontrollable ones changes, the specification is fulfilled. Conditional planning in presence of declarative and procedural trajectory constraints is a special case of this form of synthesis. We characterize the problem computationally as 2EXPTIME-complete and present a sound and complete synthesis technique based on DFA (reachability) games.
引用
收藏
页码：1558 / 1564
页数：7
相关论文
共 50 条
  • [1] LTL and LDL on Finite Traces: Reasoning, Verification, and Synthesis
    De Giacomo, Giuseppe
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (218):
  • [2] Monitoring Business Metaconstraints Based on LTL and LDL for Finite Traces
    De Giacomo, Giuseppe
    De Masellis, Riccardo
    Grasso, Marco
    Maggi, Fabrizio Maria
    Montali, Marco
    BUSINESS PROCESS MANAGEMENT, BPM 2014, 2014, 8659 : 1 - 17
  • [3] On-the-fly Synthesis for LTL over Finite Traces
    Xiao, Shengping
    Li, Jianwen
    Zhu, Shufang
    Shi, Yingying
    Pu, Geguang
    Vardi, Moshe
    THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 6530 - 6537
  • [4] Model-Guided Synthesis for LTL over Finite Traces
    Xiao, Shengping
    Li, Yongkang
    Huang, Xinyue
    Xu, Yicong
    Li, Jianwen
    Pu, Geguang
    Strichman, Ofer
    Vardi, Moshe Y.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT I, 2024, 14499 : 186 - 207
  • [5] Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness
    De Giacomo, Giuseppe
    De Masellis, Riccardo
    Montali, Marco
    PROCEEDINGS OF THE TWENTY-EIGHTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2014, : 1027 - 1033
  • [6] The Complexity of LTL on Finite Traces: Hard and Easy Fragments
    Fionda, Valeria
    Greco, Gianluigi
    THIRTIETH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2016, : 971 - 977
  • [7] Exact Synthesis of LTL Properties from Traces
    Riener, Heinz
    PROCEEDINGS OF THE 2019 FORUM ON SPECIFICATION AND DESIGN LANGUAGES (FDL), 2019,
  • [8] Finite LTL Synthesis as Planning
    Camacho, Alberto
    Baier, Jorge A.
    Muise, Christian
    McIlraith, Sheila A.
    TWENTY-EIGHTH INTERNATIONAL CONFERENCE ON AUTOMATED PLANNING AND SCHEDULING (ICAPS 2018), 2018, : 29 - 38
  • [9] LTL on finite and process traces: Complexity results and a practical reasoner
    1600, AI Access Foundation (63):
  • [10] Aalta: An LTL Satisfiability Checker over Infinite/Finite Traces
    Li, Jianwen
    Yao, Yinbo
    Pu, Geguang
    Zhang, Lijun
    He, Jifeng
    22ND ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (FSE 2014), 2014, : 731 - 734
12345