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 条

[1] BRANCHING TIME REGULAR TEMPORAL LOGIC FOR MODEL CHECKING WITH LINEAR-TIME COMPLEXITY
HAMAGUCHI, K
HIRAISHI, H
YAJIMA, S
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 253 - 262
[2] The complexity of counting models of linear-time temporal logic
Hazem Torfah
Martin Zimmermann
[J]. Acta Informatica, 2018, 55 : 191 - 212
[3] The complexity of counting models of linear-time temporal logic
Torfah, Hazem
Zimmermann, Martin
[J]. ACTA INFORMATICA, 2018, 55 (03) : 191 - 212
[4] THE COMPLEXITY OF LINEAR-TIME TEMPORAL LOGIC OVER THE CLASS OF ORDINALS
Demri, Stephane
Rabinovich, Alexander
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2010, 6 (04) : 1 - 25
[5] On the computational complexity of stratified negation in linear-time temporal logic programming
Koutras, CD
Nomikos, C
[J]. INTENSIONAL PROGRAMMING II: BASED ON THE PAPERS AT ISLIP'99, 2000, : 106 - 116
[6] On complexity of propositional Linear-time Temporal Logic with finitely many variables
Rybakov, Mikhail
Shkatov, Dmitry
[J]. PROCEEDINGS OF THE ANNUAL CONFERENCE OF THE SOUTH AFRICAN INSTITUTE OF COMPUTER SCIENTISTS AND INFORMATION TECHNOLOGISTS (SAICSIT 2018), 2018, : 313 - 316
[7] Synchronized Linear-Time Temporal Logic
Wansing, Heinrich
Kamide, Norihiro
[J]. STUDIA LOGICA, 2011, 99 (1-3) : 365 - 388
[8] Synchronized Linear-Time Temporal Logic
Heinrich Wansing
Norihiro Kamide
[J]. Studia Logica, 2011, 99
[9] A Paraconsistent Linear-time Temporal Logic
Kamide, Norihiro
Wansing, Heinrich
[J]. FUNDAMENTA INFORMATICAE, 2011, 106 (01) : 1 - 23
[10] THE COMPUTATIONAL-COMPLEXITY OF SATISFIABILITY OF TEMPORAL HORN FORMULAS IN PROPOSITIONAL LINEAR-TIME TEMPORAL LOGIC
CHEN, CC
LIN, IP
[J]. INFORMATION PROCESSING LETTERS, 1993, 45 (03) : 131 - 136

← 1 2 3 4 5 →