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 [J].
Basin, D ;
Klarlund, N .
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 [J].
BROWNE, MC ;
CLARKE, EM ;
GRUMBERG, O .
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 [J].
CHEN, CC ;
LIN, IP .
INFORMATION PROCESSING LETTERS, 1993, 45 (03) :131-136
[6]   Another look at LTL model checking [J].
Clarke, EM ;
Grumberg, O ;
Hamaguchi, K .
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
12345