# zbMATH — the first resource for mathematics

A decision procedure for propositional projection temporal logic with infinite models. (English) Zbl 1141.68039
Summary: This paper investigates the satisfiability of Propositional Projection Temporal Logic (PPTL) with infinite models. A decision procedure for PPTL formulas is given. To this end, Normal Form and Labeled Normal Form Graph (LNFG) for PPTL formulas are defined, and algorithms for transforming a formula to its normal form and constructing the LNFG for the given formula are presented. Further, the finiteness of LNFGs is proved in details. Moreover, the decision procedure is extended to check the satisfiability of the formulas of Propositional Interval Temporal Logic. In addition, examples are also given to illustrate how the decision procedure works.

##### MSC:
 68Q60 Specification and verification (program logics, model checking, etc.) 03B44 Temporal logic 68N17 Logic programming
SPIN
Full Text:
##### References:
  Moszkowski, B.C.: Reasoning about digital circuits. PhD Thesis, Stanford University. TRSTAN-CS-83-970 (1983)  Rosner, R., Pnueli, A.: A choppy logic. In: First annual IEEE symposium on logic in computer science, LICS, pp. 306–314 (1986)  Moszkowski, B.C.: A complete axiomatization of interval temporal logic with infinite time. In: 15th Annual IEEE symposium on logic in computer science (LICS’00), LICS, p. 241, (2000)  Chaochen Z., Hoare C.A.R. and Ravn A.P. (1991). A calculus of duration. Inf. Process. Lett. 40(5): 269–275 · Zbl 0743.68097  Bowman H. and Thompson S. (2003). A decision procedure and complete axiomatization of interval temporal logic with projection. J. Logic Comput. 13(2): 195–239 · Zbl 1050.03012  Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Proceedings of LICS’95, pp. 36–43 (1995)  Wang, H., Xu, Q.: Temporal logics over infinite intervals. Technical Report 158, UNU/IIST, Macau (1999) · Zbl 1040.03012  Halpern, J., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: Proceedings of the 10th international conlloquium on automata, Languages and Programming, vol. 154. Springer, LNCS, Barcelona (1983) · Zbl 0534.68025  Kono, S.: A combination of clausal and non-clausal temporal logic programs. In: Lecture notes in artificial intelligence, vol. 897, pp. 40–57. Springer, Heidelberg (1995)  Bowman, H., Thompson, S.: A Tableau method for interval temporal logic with projection. In: de Swart, H. (ed.) TABLEAUX98, LNAI 1397, Springer, Berlin (1998) · Zbl 0903.03014  Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle Upon Tyne (1996)  Duan Z. (2006). Temporal Logic and Temporal Logic Programming Language. Science press, Beijing  Duan, Z., Koutny, M., Holt, C.: Projection in temporal logic programming. In: Pfenning, F. (ed.) Proceedings of logic programming and automatic reasoning, Lecture Notes in Artificial Intelligence, vol. 822, pp. 333–344. Springer, Heidelberg (1994)  Duan Z. and Koutny M. (2004). A framed temporal logic programming language. J. Comput. Sci. Technol. 19: 333–344  Duan, Z., Yang, X., Kounty, M.: Semantics of framed temporal logic programs. In: Proceedings of ICLP 2005, vol. 3668, pp. 256–270. LNCS, Barcelona (2005)  Moszkowski, B.C.: Compositional reasoning about projected and infinite time. In: Proceeding of the first IEEE international conference on engineering of complex computer systems (ICECCS’95), pp. 238–245. IEEE Computer Society Press (1995)  Manna Z. and Pnueli A. (1992). The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg · Zbl 0753.68003  Duan, Z., Zhang, L.: A decision procedure for propositional projection temporal logic. Technical Report No.1, Institute of computing Theory and Technology, Xidian University, Xi’an, People’s Republic of China, http://www.paper.edu.cn/en/paper.php?serial_number=200611-427 (2005)  Kripke S.A. (1963). Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math. 9: 67–96 · Zbl 0118.01305  Winskel, G.: The Formal Semantics of Programming Languages. Foundations of Computing. MIT, Cambridge · Zbl 0919.68082  Holzmann G.J. (1997). The Model Checker Spin. IEEE Trans. Softw. Eng. 23(5): 279–295 · Zbl 05113845  McMillan, K.L.: Symbolic Model Checking. Kluwer (1993) · Zbl 0784.68004  Harel D., Kozen D. and Parikh R. (1982). Process logic: expressiveness, decidability, completeness. J. Comput. Syst. Sci. 25(2): 144–170 · Zbl 0494.03016  Chandra A., Halpern J., Meyer A. and Parikh R. (1985). Equations between regular terms and an application to process logic. SIAM J. Comput. 14(4): 935–942 · Zbl 0587.68031  Moszkowski B. (1986). Executing Temporal Logic Programs. Cambridge University Press, Cambridge · Zbl 0565.68003  Duan Z. (2005). Modelling and Analysis of Hybrid Systems. Science Press, Beijing  Duan Z., Holcombe M. and Bell A. (2000). A logic for biosystems. Biosystems 55(1-3): 93–105  Paech, B.: Gentzen-systems for propositional temporal logics. In: Borger, E., Kleine Buning, H., Richter, M.M. (eds.) Proceedings of the 2nd workshop on computer science logic, Duisburg (FRG), vol. 385, pp. 240–253. Springer, Heidelberg (1988) · Zbl 0712.03015  Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE symposium on foundations of computer science, pp. 46–57 (1977)  Tian, C., Duan, Z.: Model Checking Propositional Projection Temporal Logic Based on SPIN, ICFEM 2007, LNCS4789, pp. 246-265, Springer, Heidelberg (2007)  Kröger, F.: Temporal Logic of Programs. EATCS Monographs on Theoretical Computer Science, vol. 8. Springer, Heidelberg (1987) · Zbl 0609.03007  Wolper P.L. (1983). Temporal logic can be more expressive. Inf. Control 56: 72–99 · Zbl 0534.03009
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.