The Complexity of Linear-Time Temporal Logic Model Repair

被引：1

作者：

Tao, Xiuting ^{[1
]}

Li, Guoqiang ^{[1
]}

机构：

[1] Shanghai Jiao Tong Univ, Sch Software, Shanghai, Peoples R China

来源：

STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2017 | 2018年 / 10795卷

基金：

美国国家科学基金会;

关键词：

D O I：

10.1007/978-3-319-90104-6_5

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We propose the model repair problem of the linear-time temporal logic. Informally, the repair problem asks for a minimum set of states in a given Kripke structure M, whose modification can make the given LTL formula satisfiable. We will examplify the application of the model and study the computational complexity of the problem. We will show the problem can be solved in exponential time but remains NP-hard even if k is a constant.

引用

页码：69 / 87

页数：19

共 50 条

[31] The complexity of the temporal logic with "until" over general linear time
Reynolds, M
[J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2003, 66 (02) : 393 - 426
[32] THE CHECKERS PROBLEM - A SOLUTION WITH LINEAR-TIME COMPLEXITY
TRAUNMULLER, K
[J]. SIGPLAN NOTICES, 1995, 30 (09): : 25 - 32
[33] Verifying Vaccine Supply Chain System in Indonesia Using Linear-Time Temporal Logic
Wikatama, Muhammad Fikri Suyudi
Arzaki, Muhammad
Rusmawati, Yanti
[J]. 2018 6TH INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION TECHNOLOGY (ICOICT), 2018, : 245 - 253
[34] Failure diagnosis of discrete-event systems with linear-time temporal logic specifications
Jiang, SB
Kumar, R
[J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2004, 49 (06) : 934 - 945
[35] Diagnosis of repeated failures for discrete event systems with linear-time temporal logic specifications
Jiang, SB
Kumar, R
[J]. 42ND IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-6, PROCEEDINGS, 2003, : 3221 - +
[36] Modeling and testing object-oriented distributed systems with linear-time temporal logic
Dietrich, F
Logean, X
Hubaux, JP
[J]. CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2001, 13 (05): : 385 - 420
[37] Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming
Jeltsch, Wolfgang
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 286 : 229 - 242
[38] STRONG NORMALIZATION OF A TYPED LAMBDA CALCULUS FOR INTUITIONISTIC BOUNDED LINEAR-TIME TEMPORAL LOGIC
Kamide, Norihiro
[J]. REPORTS ON MATHEMATICAL LOGIC, 2012, 47 : 29 - 61
[39] On the complexity of the linear-time μ-calculus for Petri Nets
Habermehl, P
[J]. APPLICATION AND THEORY OF PETRI NETS 1997, 1997, 1248 : 102 - 116
[40] Failure diagnosis of discrete event systems with linear-time temporal logic fault specifications
Jiang, SB
Kumar, R
[J]. PROCEEDINGS OF THE 2002 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 2002, 1-6 : 128 - 133

← 1 2 3 4 5 →