×

zbMATH — the first resource for mathematics

Complexity of propositional projection temporal logic with star. (English) Zbl 1161.03008
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.)
PDF BibTeX Cite
Full Text: DOI
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)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.