A decision procedure for propositional projection temporal logic with infinite models. (English) Zbl 1141.68039

Duan, Zhenhua; Tian, Cong; Zhang, Li

Acta Inf. 45, No. 1, 43-78 (2008).

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

Software:

SPIN

References:

[1]	Moszkowski, B.C.: Reasoning about digital circuits. PhD Thesis, Stanford University. TRSTAN-CS-83-970 (1983)
[2]	Rosner, R., Pnueli, A.: A choppy logic. In: First annual IEEE symposium on logic in computer science, LICS, pp. 306–314 (1986)
[3]	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)
[4]	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
[5]	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
[6]	Dutertre, B.: Complete proof systems for first order interval temporal logic. In: Proceedings of LICS’95, pp. 36–43 (1995)
[7]	Wang, H., Xu, Q.: Temporal logics over infinite intervals. Technical Report 158, UNU/IIST, Macau (1999) · Zbl 1040.03012
[8]	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
[9]	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)
[10]	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
[11]	Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle Upon Tyne (1996)
[12]	Duan Z. (2006). Temporal Logic and Temporal Logic Programming Language. Science press, Beijing
[13]	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)
[14]	Duan Z. and Koutny M. (2004). A framed temporal logic programming language. J. Comput. Sci. Technol. 19: 333–344
[15]	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)
[16]	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)
[17]	Manna Z. and Pnueli A. (1992). The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg · Zbl 0753.68003
[18]	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)
[19]	Kripke S.A. (1963). Semantical analysis of modal logic I: normal propositional calculi. Z. Math. Logik Grund. Math. 9: 67–96 · Zbl 0118.01305
[20]	Winskel, G.: The Formal Semantics of Programming Languages. Foundations of Computing. MIT, Cambridge · Zbl 0919.68082
[21]	Holzmann G.J. (1997). The Model Checker Spin. IEEE Trans. Softw. Eng. 23(5): 279–295 · Zbl 05113845
[22]	McMillan, K.L.: Symbolic Model Checking. Kluwer (1993) · Zbl 0784.68004
[23]	Harel D., Kozen D. and Parikh R. (1982). Process logic: expressiveness, decidability, completeness. J. Comput. Syst. Sci. 25(2): 144–170 · Zbl 0494.03016
[24]	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
[25]	Moszkowski B. (1986). Executing Temporal Logic Programs. Cambridge University Press, Cambridge · Zbl 0565.68003
[26]	Duan Z. (2005). Modelling and Analysis of Hybrid Systems. Science Press, Beijing
[27]	Duan Z., Holcombe M. and Bell A. (2000). A logic for biosystems. Biosystems 55(1-3): 93–105
[28]	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
[29]	Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE symposium on foundations of computer science, pp. 46–57 (1977)
[30]	Tian, C., Duan, Z.: Model Checking Propositional Projection Temporal Logic Based on SPIN, ICFEM 2007, LNCS4789, pp. 246-265, Springer, Heidelberg (2007)
[31]	Kröger, F.: Temporal Logic of Programs. EATCS Monographs on Theoretical Computer Science, vol. 8. Springer, Heidelberg (1987) · Zbl 0609.03007
[32]	Wolper P.L. (1983). Temporal logic can be more expressive. Inf. Control 56: 72–99 · Zbl 0534.03009