［1］ Pnueli A. The Temporal Logic of Programs ［C］//Proc of FOCS 1977. Providence: IEEE Computer Society, 1977: 46-57.
［2］ Clark E, Emerson E. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic ［C］//Proc of the Workshop on Logic of Programs 1981. Heidelberg: Springer, 1981: 52-71.
［3］ Lamport L. The Temporal Logic of Actions ［J］. ACM Trans on Programming Language and Systems, 1994, 16(3): 872-923.
［4］ Moszkowski B C. Executing Temporal Logic Programs ［M］. Cambridge: Cambridge University Press, 1986.
［5］ Zhou C, Hoare C, Ravn A. A Calculus of Durations ［J］. Information Processing Letters, 1991, 40(5): 269-276.
［6］ Duan Z, Koutny M, Holt C. Projection in Temporal Logic Programming ［C］//Proc of LPAR 1994. Heidelberg: Springer , 1994: 333-344.
［7］ Duan Z, Tian C, Zhang L. A Decision Procedure for Propositional Projection Temporal Logic with Infinite Models ［J］. Acta Informaticae, 2008, 45(1): 43-78.
［8］ Duan Z, Zhang N. A Complete Proof System for Propositional Projection Temporal Logic ［J/OL］. ［2012-01-24］. http://www.sciencedirect.com/science/article/pii/S030439751200062X.
［9］ 杨银堂, 徐阳扬, 周端, 等. 异步超前进位加法器设计 ［J］. 西安电子科技大学学报, 2009, 36(1): 33-37.
 Yang Yintang, Xu Yangyang, Zhou Duan. Design of the Asynchronous CLA Adder ［J］. Journal of Xidian University, 2009, 36(1): 33-37.
［10］ 舒新峰, 段振华. 投影时序逻辑的公理系统与形式验证 ［J］. 西安电子科技大学学报, 2009, 36(4): 680-685.
 Shu Xinfeng, Duan Zhenhua. Axiomatization for the First-order Projection Temporal Logic and Formal Verifications ［J］. Journal of Xidian University, 2009, 36(4): 680-685.