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 条
  • [41] Distributed PROMPT-LTL Synthesis
    Jacobs, Swen
    Tentrup, Leander
    Zimmermann, Martin
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (226): : 228 - 241
  • [42] Antichains and compositional algorithms for LTL synthesis
    Filiot, Emmanuel
    Jin, Naiyong
    Raskin, Jean-Francois
    FORMAL METHODS IN SYSTEM DESIGN, 2011, 39 (03) : 261 - 296
  • [43] LTL Reactive Synthesis under Assumptions
    Aminof, Benjamin
    De Giacomo, Giuseppe
    Murano, Aniello
    Patrizi, Fabio
    Rubin, Sasha
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (218): : 52 - +
  • [44] Towards symbolic strategy synthesis for ⟪A⟫-LTL
    Harding, A
    Ryan, M
    Schobbens, PY
    TIME-ICTL 2003: 10TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING AND FOURTH INTERNATIONAL CONFERENCE ON TEMPORAL LOGIC, PROCEEDINGS, 2003, : 137 - 146
  • [45] A LTL Fragment for GR(1)-Synthesis
    Morgenstern, Andreas
    Schneider, Klaus
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (50): : 33 - 45
  • [46] Model checking LTL properties over ANSI-C programs with bounded traces
    Jeremy Morse
    Lucas Cordeiro
    Denis Nicole
    Bernd Fischer
    Software & Systems Modeling, 2015, 14 : 65 - 81
  • [47] Model checking LTL properties over ANSI-C programs with bounded traces
    Morse, Jeremy
    Cordeiro, Lucas
    Nicole, Denis
    Fischer, Bernd
    SOFTWARE AND SYSTEMS MODELING, 2015, 14 (01): : 65 - 81
  • [48] A new algorithm for strategy synthesis in LTL games
    Harding, A
    Ryan, M
    Schobbens, PY
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 477 - 492
  • [49] Safraless LTL synthesis considering maximal realizability
    Takashi Tomita
    Atsushi Ueno
    Masaya Shimakawa
    Shigeki Hagihara
    Naoki Yonezaki
    Acta Informatica, 2017, 54 : 655 - 692
  • [50] GR(1) Synthesis for LTL Specification Patterns
    Maoz, Shahar
    Ringert, Jan Oliver
    2015 10TH JOINT MEETING OF THE EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND THE ACM SIGSOFT SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (ESEC/FSE 2015) PROCEEDINGS, 2015, : 96 - 106
12345