The complexity of propositional linear temporal logics in simple cases

被引：74

作者：

Demri, S

Schnoebelen, P

机构：

[1] ENS, Lab Specificat & Verificat, F-94235 Cachan, France

[2] CNRS, UMR 8643, F-94235 Cachan, France

来源：

INFORMATION AND COMPUTATION | 2002年 / 174卷 / 01期

关键词：

logic in computer science; computational complexity; verification; temporal logic; model checking;

D O I：

10.1006/inco.2001.3094

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

It is well known that model checking and satisfiability for PLTL are PSPACE-complete, By contrast, very little is known about whether there exist, some interesting fragments of PLTL with it lower worst-case complexity. Such results would help understand why PLTL model checkers are successfully used in practice. In this article we investigate this issue and consider model checking and satisfiability for all fragments of PLTL obtainable by restricting (1) the temporal connectives allowed. (2) the number of atomic propositions, and (3) the temporal height. (C) 2002 Elsevier Science (USA).

引用

页码：84 / 103

页数：20

共 43 条

[1] Automata based symbolic reasoning in hardware verification
Basin, D
Klarlund, N
[J]. FORMAL METHODS IN SYSTEM DESIGN, 1998, 13 (03) : 255 - 288
[2] BJORNER NS, 1996, LNCS, V1102, P415
[3] CHARACTERIZING FINITE KRIPKE STRUCTURES IN PROPOSITIONAL TEMPORAL LOGIC
BROWNE, MC
CLARKE, EM
GRUMBERG, O
[J]. THEORETICAL COMPUTER SCIENCE, 1988, 59 (1-2) : 115 - 131
[4] Bull R.A., 1965, J SYMBOLIC LOGIC, V30, P58
[5] 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
[6] Another look at LTL model checking
Clarke, EM
Grumberg, O
Hamaguchi, K
[J]. FORMAL METHODS IN SYSTEM DESIGN, 1997, 10 (01) : 47 - 71
[7] Comon H., 2000, LNCS, V1862, P262, DOI DOI 10.1007/3-540-44622-217
[8] Cook S. A., 1971, P 3 ANN ACM S THEOR, P151, DOI [DOI 10.1145/800157.805047, 10.1145/800157.805047]
[9] DALAL M, 1996, P 12 EUR C ART INT E, P355
[10] Dams D., 1999, Log. J. IGPL, V7, P55

← 1 2 3 4 5 →