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 条

[11]

DUTERTRE B, 1995, IEEE S LOG, P36, DOI 10.1109/LICS.1995.523242

[12] PROCESS LOGIC - EXPRESSIVENESS, DECIDABILITY, COMPLETENESS [J].

HAREL, D ;

KOZEN, D ;

PARIKH, R .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1982, 25 (02) :144-170

[13]

HOLZMANN J, 2003, IEEE T SOFTWARE ENG, V23, P279

[14]

KONO S, 1993, LECT NOTES ARTIF INT, V897, P40

[15]

Kripke S., 1963, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, V9, P67, DOI [DOI 10.1002/MALQ.19630090502, 10.1002/malq.19630090502]

[16] A relation-based method combining functional and structural testing for test case generation [J].

Liu, Shaoying ;

Chen, Yuting .

JOURNAL OF SYSTEMS AND SOFTWARE, 2008, 81 (02) :234-248

[17] An automated approach to specification animation for validation [J].

Liu, Shaoying ;

Wang, Hao .

JOURNAL OF SYSTEMS AND SOFTWARE, 2007, 80 (08) :1271-1285

[18]

MOSZKOWSKI B, 1995, ENG COMPLEX COMPUTER, P238

[19]

MOSZKOWSKI B, 2004, SPRINGER VERLAG LECT, V2772, P480

[20]

MOSZKOWSKI B, 1983, THESIS STANFORD U

← 1 2 3 →