Abstract
In Propositional Projection Temporal Logic (PPTL), a well-formed formula is generally formed by applying rules of its syntax finitely many times. However, under some circumstances, although formulas such as ones expressed by index set expressions, are constructed via applying rules of the syntax infinitely many times, they are possibly still well-formed. With this motivation, this paper investigates the relationship between formulas specified by index set expressions and concise syntax expressions by means of fixed-point induction approach. Firstly, we present two kinds of formulas, namely \(\bigvee_{i\in N_0}\bigcirc^i P\) and \(\bigvee_{i\in N_0}P^i\), and prove they are indeed well-formed by demonstrating their equivalence to formulas \(\Diamond P\) and P + respectively. Further, we generalize \(\bigvee_{i\in N_0}\bigcirc^i Q\) to \(\bigvee_{i\in N_0}P^{(i)} \wedge \bigcirc^i Q\) and explore solutions of an abstract equation \(X \equiv Q \vee P \wedge \bigcirc X\). Moreover, we equivalently represent ‘U’ (strong until) and ‘W’ (weak until) constructs in Propositional Linear Temporal Logic within PPTL using the index set expression techniques.
This research is supported by the NSFC Grant Nos. 61133001, 61272118, 61272117, 61202038, 91218301 and National Program on Key Basic Research Project (973 Program) Grant No. 2010CB328102.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Clarke, E.M., Allen Emerson, E.: Design and synthesis of synchronization skeletons using branching timed temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Massachusetts (2000)
Duan, Z.: An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming. PhD thesis, University of Newcastle Upon Tyne (May 1996)
Duan, Z.: Temporal Logic and Temporal Logic Programming Language. Science Press, Beijing (2006)
Duan, Z., Koutny, M., Holt, C.: Projection in temporal logic programming. In: Pfenning, F. (ed.) LPAR 1994. LNCS (LNAI), vol. 822, pp. 333–344. Springer, Heidelberg (1994)
Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45, 43–78 (2008)
Duan, Z., Zhang, N., Koutny, M.: A complete proof system for propositional projection temporal logic. Theoretical Computer Science (2012), doi:10.1016/j.tcs.2012.01.026
Gordon, M.: Twenty years of theorem proving for hols past, present and future. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 1–5. Springer, Heidelberg (2008)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of ACM 12, 576–583 (1969)
Kleene, S.C.: Mathematical logic. John Wiley (1967)
Manna, Z., Pnueli, A.: Temporal Logic of Reactive and Concurrent Systems. Springer, Berlin (1992)
Moszkowski, B.C.: Executing Temporal Logic Programs. PhD thesis, Cambridge Uniersity (1986)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annal IEEE Symp. on Foudations of Computer Science, pp. 46–57. IEEE Computer Society (1977)
Tarski, A.: A lattic-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics 5, 285–309 (1955)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. The MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Duan, Z., Ma, Q., Tian, C., Zhang, N. (2013). Some Fixed-Point Issues in PPTL. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol 8051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39698-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-39698-4_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39697-7
Online ISBN: 978-3-642-39698-4
eBook Packages: Computer ScienceComputer Science (R0)