Hostname: page-component-8448b6f56d-qsmjn Total loading time: 0 Render date: 2024-04-18T08:57:39.877Z Has data issue: false hasContentIssue false
  • English
  • Français

Complexity of propositional projection temporal logic with star†

Published online by Cambridge University Press:  01 February 2009

CONG TIAN  and
ZHENHUA DUAN
CONG TIAN
Affiliation:
Institute of Computing Theory and Technology, Xidian University, Xi'an, 710071, P. R. China
ZHENHUA DUAN*
Affiliation:
Institute of Computing Theory and Technology, Xidian University, Xi'an, 710071, P. R. China
*
‡Corresponding author.
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Special Issue 1: Theory and Applications of Models of Computation (TAMC) , February 2009 , pp. 73 - 100
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

This research is supported by the NSFC Grant No. 60433010, and Defence Pre-Research Project of China, No. 51315050105, and NSFC Grant No. 60873018 jointly sponsored by Microsoft Asia Research Academy.

References

Barringer, H., Kuiper, R. and Pnueli, A. (1984) Now You May Compose Temporal Logic Specification. In: Proc. 16th STOC 51–63.CrossRefGoogle Scholar
Bowman, H. and Thompson, S. (2003) A decision procedure and complete axiomatization of interval temporal logic with projection. Journal of logic and Computation 13 (2)195–239.CrossRefGoogle Scholar
Chandra, A., Halpern, H., Meyer, A. and Parikh, R. (1985) Equations between Regular Terms and an Application to Process Logic. SIAM J. Computing 14 932–942.Google Scholar
Duan, Z. (2006) Temporal Logic and Temporal Logic Programming, Science Press of China.Google Scholar
Duan, Z. and Koutny, M. (2004) A Framed Temporal Logic Programming Language. Journal of Computer Science and Technology 19 (3)341–351.CrossRefGoogle Scholar
Duan, Z. and Tian, C. (2007) Decidability of Propositional Projection Temporal Logic with Infinite Models. In: Proceedings, Theory and Applications of Models of Computation 2007. Springer-Verlag Lecture Notes in Computer Science 4484 521–532.CrossRefGoogle Scholar
Duan, Z., Koutny, M. and Holt, C. (1994) Projection in temporal logic programming. In: Logic Programming and Automatic Reasoning. Springer-Verlag Lecture Notes in Artificial Intelligence 822 333–344.Google Scholar
Duan, Z., Yang, X. and Koutny, M. (2008a) Framed Temporal Logic Programming. Science of Computer Programming 70 31–61.CrossRefGoogle Scholar
Duan, Z., Tian, C. and Zhang, L. (2008b) A Decision Procedure for Propositional Projection Temporal Logic with Infinite Models. Acta Informatica 45 (1)43–78.CrossRefGoogle Scholar
Dutertre, B. (1995) Complete proof systems for first order interval temporal logic. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society 36–43.CrossRefGoogle Scholar
Harel, D., Kozen, D. and Parikh, R. (1982) Process logic: Expressiveness, decidability, completeness. J. Comput. System Sci. 25 144–170.CrossRefGoogle Scholar
Holzmann, J. (2003) The Model Checker Spin. IEEE Trans. on Software Engineering 23 (5)279–295.CrossRefGoogle Scholar
Kono, S. (1993) A combination of clausal and non-clausal temporal logic programs. Springer-Verlag Lecture Notes in Artificial Intelligence 897 40–57.Google Scholar
Kripke, S. (1963) Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math 9 67–96.CrossRefGoogle Scholar
Liu, S. and Wang, H. (2007) An automated approach to specification animation for validation. The Journal of Systems and Software 80 (8)1271–1285.CrossRefGoogle Scholar
Liu, S. and Chen, Y. (2008) A relation-based method combining functional and structural testing for test case generation. The Journal of Systems and Software 81 (2)234–248.CrossRefGoogle Scholar
Manna, Z. and Pnueli, A. (1992) The temporal logic of reactive and concurrent systems, Springer-Verlag.CrossRefGoogle Scholar
Moszkowski, B. (1983) Reasoning about digital circuits, Ph. D. Thesis, Department of Computer Science, Stanford University.Google Scholar
Moszkowski, B. (1995) Compositional reasoning about projected and infinite time. Engineering of Complex Computer Systems, IEEE Computer Society Press 238–245.Google Scholar
Moszkowski, B. (2004) A hierarchical completeness proof for propositional temporal logic. In: Dershowitz, N. (ed.) Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday. Springer-Verlag Lecture Notes in Computer Science 2772 480–523.CrossRefGoogle Scholar
Rosner, R. and Pnueli, A. (1986) A choppy logic. In: Proceedings, Symposium on Logic in Computer Science, IEEE Computer Society 306–314.Google Scholar
Stockmeyer, L. (1974) The Complexity of Decision Problems in Automata Theory and Logic, Ph. D. thesis, MIT (available as Project MAC Technical Report 133).Google Scholar
Tarski, A. (1955) A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific J. Math 5 285–309.CrossRefGoogle Scholar
Tian, C. and Duan, Z. (2007) Model Checking Propositional Projection Temporal Logic Based on SPIN. In: ICFEM 2007. Springer-Verlag Lecture Notes in Computer Science 4789 246–265.CrossRefGoogle Scholar
Tian, C. and Duan, Z. (2008) Propositional Projection Temporal Logic, Büchi Automata and ω-Regular Expressions. In: Proceedings, Theory and Applications of Models of Computation 2008. 4978 47–58.Google Scholar
Wang, H. and Xu, Q. (2004) Completeness of Temporal Logics over Infinite Models. Discrete Applied Mathematics 136 87–103.CrossRefGoogle Scholar
Wolper, P. (1983) Temporal logic can be more expressive. Information and Control 56 72–99.CrossRefGoogle Scholar
Zhou, C., Hoare, C. A. R. and Ravn, A. P. (1991) A calculus of duration. Information Processing Letters 40 (5)269–275.Google Scholar