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 条

[21] Assume-Guarantee Verification for Probabilistic Systems
Kwiatkowska, Marta
Norman, Gethin
Parker, David
Qui, Hongyang
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2010, 6015 : 23 - +
[22] Composition of Behavioural Assume-Guarantee Contracts
Shali, Brayan M.
van der Schaft, Arjan
Besselink, Bart
[J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2023, 68 (10) : 5991 - 6006
[23] Assume-Guarantee Verification of Strategic Ability
Mikulski, Lukasz
Jamroga, Wojciech
Kurpiewski, Damian
[J]. PRIMA 2022: PRINCIPLES AND PRACTICE OF MULTI-AGENT SYSTEMS, 2023, 13753 : 173 - 191
[24] Counterexample-Guided Assume-Guarantee Synthesis through Learning
Lin, Shang-Wei
Hsiung, Pao-Ann
[J]. IEEE TRANSACTIONS ON COMPUTERS, 2011, 60 (05) : 734 - 750
[25] Monitoring Assumptions in Assume-Guarantee Contracts
Sokolsky, Oleg
Zhang, Teng
Lee, Insup
McDougall, Michael
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (208): : 46 - 53
[26] Assume-guarantee testing for software components
Giannakopoulou, D.
Pasareanu, C. S.
Blundell, C.
[J]. IET SOFTWARE, 2008, 2 (06) : 547 - 562
[27] Decentralized Classification with Assume-Guarantee Planning
Carr, Steven
Quattrociocchi, Jesse
Bharadwaj, Suda
Spencer, Steven J.
Parikh, Anup
Young, Carol C.
Buerger, Stephen P.
Wu, Bo
Topcu, Ufuk
[J]. 2021 IEEE/RSJ INTERNATIONAL CONFERENCE ON INTELLIGENT ROBOTS AND SYSTEMS (IROS), 2021, : 9826 - 9832
[28] ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS
Lomuscio, Alessio
Strulo, Ben
Walker, Nigel
Wu, Peng
[J]. INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2013, 24 (04) : 419 - 444
[29] Compositional Synthesis via a Convex Parameterization of Assume-Guarantee Contracts
Ghasemi, Kasra
Sadraddini, Sadra
Belta, Calin
[J]. PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (HSCC2020) (PART OF CPS-IOT WEEK), 2020,
[30] Assume-Guarantee Contracts and Controller Synthesis for Vehicular Traffic Networks
Kim, Eric S.
Arcak, Murat
Seshia, Sanjit A.
[J]. 2016 AMERICAN CONTROL CONFERENCE (ACC), 2016, : 882 - 882

← 1 2 3 4 5 →