Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

被引：0

作者：

Fijalkow, Nathanael ^{[1
,2
,3
]}

Maubert, Bastien ^{[4
]}

Murano, Aniello ^{[4
]}

Vardi, Moshe ^{[5
]}

机构：

[1] CNRS, Bordeaux, France

[2] LaBRI, Bordeaux, France

[3] Alan Turing Inst Data Sci, London, England

[4] Univ Napoli Federico II, Naples, Italy

[5] Rice Univ, Houston, TX USA

来源：

PROCEEDINGS OF THE TWENTY-NINTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE | 2020年

关键词：

AUTOMATA;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Prompt-LTL extends Linear Temporal Logic with a bounded version of the "eventually" operator to express temporal requirements such as bounding waiting times. We study assume-guarantee synthesis for prompt-LTL: the goal is to construct a system such that for all environments satisfying a first prompt-LTL formula (the assumption) the system composed with this environment satisfies a second prompt-LTL formula (the guarantee). This problem has been open for a decade. We construct an algorithm for solving it and show that, like classical LTL synthesis, it is 2-EXPTIME-complete.

引用

页码：117 / 123

页数：7

共 50 条

[1] Assume-guarantee synthesis
Chatterjee, Krishnendu
Henzinger, Thomas A.
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 261 - +
[2] Compositional Synthesis of Signal Temporal Logic Tasks via Assume-Guarantee Contracts
Liu, Siyuan
Saoud, Adnane
Jagtap, Pushpak
Dimarogonas, Dimos, V
Zamani, Majid
[J]. 2022 IEEE 61ST CONFERENCE ON DECISION AND CONTROL (CDC), 2022, : 2184 - 2189
[3] Assume-Guarantee Distributed Synthesis
Majumdar, Rupak
Mallik, Kaushik
Schmuck, Anne-Kathrin
Zufferey, Damien
[J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2020, 39 (11) : 3215 - 3226
[4] Assume-Guarantee Synthesis of Decentralised Supervisory Control
Mainhardt, Ana Maria
Schmuck, Anne-Kathrin
[J]. IFAC PAPERSONLINE, 2022, 55 (28): : 165 - 172
[5] Assume-guarantee synthesis for digital contract signing
Chatterjee, Krishnendu
Raman, Vishwanath
[J]. FORMAL ASPECTS OF COMPUTING, 2014, 26 (04) : 825 - 859
[6] On the relationship between concurrent separation logic and assume-guarantee reasoning
Feng, Xinyu
Ferreira, Rodrigo
Shao, Zhong
[J]. PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2007, 4421 : 173 - +
[7] Behavioural assume-guarantee contracts for linear dynamical systems
Shah, B. M.
van der Schaft, A. J.
Besselink, B.
[J]. 2021 60TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2021, : 2002 - 2007
[8] Quotient for Assume-Guarantee Contracts
Romeo, Inigo Incer
Sangiovanni-Vincentelli, Alberto
Lin, Chung-Wei
Kang, Eunsuk
[J]. PROCEEDINGS OF THE 2018 16TH ACM/IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN (MEMOCODE), 2018, : 67 - 77
[9] Compositional synthesis for linear systems via convex optimization of assume-guarantee contracts
Ghasemi, Kasra
Sadraddini, Sadra
Belta, Calin
[J]. AUTOMATICA, 2024, 169
[10] Assume-guarantee reasoning for deadlock
Chaki, Sagar
Sinha, Nishant
[J]. PROCEEDINGS OF FORMAL METHODS IN COMPUTER AIDED DESIGN, 2006, : 134 - +

← 1 2 3 4 5 →