Complexity of propositional projection temporal logic with star

被引：24

作者：

Tian, Cong ^{[1
]}

Duan, Zhenhua ^{[1
]}

机构：

[1] Xidian Univ, Inst Comp Theory & Technol, Xian 710071, Peoples R China

来源：

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | 2009年 / 19卷 / 01期

基金：

中国国家自然科学基金;

关键词：

DECISION PROCEDURE; COMPLETENESS;

D O I：

10.1017/S096012950800738X

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper investigates the complexity of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Propositional Projection Temporal Logic (PPTL) is first extended to include projection star. Then, by reducing the emptiness problem of star-free expressions to the problem of the satisfiability of PPTL* formulas, the lower bound of the complexity for the satisfiability of PPTL* formulas is proved to be non-elementary. Then, to prove the decidability of PPTL*, the normal form, normal form graph (NFG) and labelled normal form graph (LNFG) for PPTL* are defined. Also, algorithms for transforming a formula to its normal form and LNFG are presented. Finally, a decision algorithm for checking the satisfiability of PPTL* formulas is formalised using LNFGs.

引用

页码：73 / 100

页数：28

共 27 条

[1]

[Anonymous], 1992, TEMPORAL LOGIC REACT, DOI DOI 10.1007/978-1-4612-0931-7

[2]

[Anonymous], 1984, PROC 16 ACM S THEORY, DOI DOI 10.1145/800057.808665

[3] A decision procedure and complete axiomatization of finite interval temporal logic with projection [J].

Bowman, H ;

Thompson, S .

JOURNAL OF LOGIC AND COMPUTATION, 2003, 13 (02) :195-239

[4]

CHANDRA A, 1985, SIAM J COMPUT, V14, P932

[5] A CALCULUS OF DURATIONS [J].

CHAOCHEN, Z ;

HOARE, CAR ;

RAVN, AP .

INFORMATION PROCESSING LETTERS, 1991, 40 (05) :269-276

[6]

DUAN Z, 1994, LECT NOTES ARTIF INT, V822, P333

[7] A framed temporal logic programming language [J].

Duan, ZH ;

Koutny, M .

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2004, 19 (03) :341-351

[8] A decision procedure for propositional projection temporal logic with infinite models [J].

Duan, Zhenhua ;

Tian, Cong ;

Zhang, Li .

ACTA INFORMATICA, 2008, 45 (01) :43-78

[9] Framed temporal logic programming [J].

Duana, Zhenhua ;

Yanga, Xiaoxiao ;

Koutnyb, Maciej .

SCIENCE OF COMPUTER PROGRAMMING, 2008, 70 (01) :31-61

[10]

DUANE A, 1905, OPHTHALMOLOGY, V2, P1

← 1 2 3 →