Complexity of propositional projection temporal logic with star. (English) Zbl 1161.03008

Tian, Cong; Duan, Zhenhua

Math. Struct. Comput. Sci. 19, No. 1, 73-100 (2009).

Summary: 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.

MSC:

03B44	Temporal logic
03B25	Decidability of theories and sets of sentences
68Q60	Specification and verification (program logics, model checking, etc.)

Keywords:

temporal logic; complexity; satisfiability; emptiness problem; decidability; algorithm

References:

[1]	Moszkowski, Engineering of Complex Computer Systems pp 238– (1995)
[2]	Moszkowski, Springer-Verlag Lecture Notes in Computer Science 2772 pp 480– (2004)
[3]	DOI: 10.1016/j.jss.2007.05.036 · Zbl 05434403
[4]	DOI: 10.1016/j.jss.2006.12.540 · Zbl 05434188
[5]	DOI: 10.1007/s00236-007-0062-z · Zbl 1141.68039
[6]	DOI: 10.1002/malq.19630090502 · Zbl 0118.01305
[7]	DOI: 10.1016/j.scico.2007.09.001 · Zbl 1131.68036
[8]	Kono, Springer-Verlag Lecture Notes in Artificial Intelligence 897 pp 40– (1993)
[9]	Duan, Springer-Verlag Lecture Notes in Artificial Intelligence 822 pp 333– (1994)
[10]	DOI: 10.1109/32.588521 · Zbl 05113845
[11]	Duan, Springer-Verlag Lecture Notes in Computer Science 4484 pp 521– (2007) · Zbl 1198.68167
[12]	DOI: 10.1016/0022-0000(82)90003-4 · Zbl 0494.03016
[13]	DOI: 10.1007/BF02944904 · Zbl 02179589
[14]	Duan, Temporal Logic and Temporal Logic Programming (2006)
[15]	DOI: 10.1137/0214049 · Zbl 0603.68100
[16]	DOI: 10.1093/logcom/13.2.195 · Zbl 1050.03012
[17]	DOI: 10.1016/0020-0190(91)90122-X · Zbl 0743.68097
[18]	DOI: 10.1016/S0019-9958(83)80051-5 · Zbl 0534.03009
[19]	DOI: 10.1016/S0166-218X(03)00201-4 · Zbl 1040.03012
[20]	Tian, Springer-Verlag Lecture Notes in Computer Science 4789 pp 246– (2007) · Zbl 05277262
[21]	Tarski, Pacific J. Math 5 pp 285– (1955) · Zbl 0064.26004
[22]	Manna, The temporal logic of reactive and concurrent systems (1992)