zbMATH — the first resource for mathematics

Examples
Geometry Search for the term Geometry in any field. Queries are case-independent.
Funct* Wildcard queries are specified by * (e.g. functions, functorial, etc.). Otherwise the search is exact.
"Topological group" Phrases (multi-words) should be set in "straight quotation marks".
au: Bourbaki & ti: Algebra Search for author and title. The and-operator & is default and can be omitted.
Chebyshev | Tschebyscheff The or-operator | allows to search for Chebyshev or Tschebyscheff.
"Quasi* map*" py: 1989 The resulting documents have publication year 1989.
so: Eur* J* Mat* Soc* cc: 14 Search for publications in a particular source with a Mathematics Subject Classification code (cc) in 14.
"Partial diff* eq*" ! elliptic The not-operator ! eliminates all results containing the word elliptic.
dt: b & au: Hilbert The document type is set to books; alternatively: j for journal articles, a for book articles.
py: 2000-2015 cc: (94A | 11T) Number ranges are accepted. Terms can be grouped within (parentheses).
la: chinese Find documents in a given language. ISO 639-1 language codes can also be used.

Operators
a & b logic and
a | b logic or
!ab logic not
abc* right wildcard
"ab c" phrase
(ab c) parentheses
Fields
any anywhere an internal document identifier
au author, editor ai internal author identifier
ti title la language
so source ab review, abstract
py publication year rv reviewer
cc MSC code ut uncontrolled term
dt document type (j: journal article; b: book; a: book article)
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:
68Q60Specification and verification of programs
03B44Temporal logic
68N17Logic 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 · doi:10.1016/0020-0190(91)90122-X
[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 · doi:10.1093/logcom/13.2.195
[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)
[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)
[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)
[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
[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 · doi:10.1002/malq.19630090502
[20]Winskel, G.: The Formal Semantics of Programming Languages. Foundations of Computing. MIT, Cambridge
[21]Holzmann G.J. (1997). The Model Checker Spin. IEEE Trans. Softw. Eng. 23(5): 279–295 · Zbl 05113845 · doi:10.1109/32.588521
[22]McMillan, K.L.: Symbolic Model Checking. Kluwer (1993)
[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 · doi:10.1016/0022-0000(82)90003-4
[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
[25]Moszkowski B. (1986). Executing Temporal Logic Programs. Cambridge University Press, Cambridge
[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 · doi:10.1016/S0303-2647(99)00087-8
[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)
[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)
[32]Wolper P.L. (1983). Temporal logic can be more expressive. Inf. Control 56: 72–99 · Zbl 0534.03009 · doi:10.1016/S0019-9958(83)80051-5