[敬请读者注意] 本人保留本文的全部著作权利。如果哪位读者使用本文所描述内容，请务必如实引用并明白注明本文出处。如果本人发现任何人擅自使用本文任何部分内容而不明白注明出处，恕本人在网上广泛公布侵权者姓名。敬请各位读者注意，谢谢！

将时态逻辑引入计算机科学的图灵奖获奖者 - 普纽埃利 

程京德

    普纽埃利(Amir Pnueli [Hebrew: אמיר פנואלי, pronounced p’new-EL-ee] April 22, 1941 – November 2, 2009) 是以色列计算机科学家，是将时态逻辑引入计算机科学[1]并且因为开创了时态逻辑在计算机科学领域的应用而获得1996年ACM图灵奖的学者[2]。ACM的表彰词为：“将时序逻辑引入计算科学的开创性工作以及对程序和系统验证的杰出贡献(For seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification)。”[2]   

    普纽埃利于1962年毕业于以色列理工大学(Technion - Israel Institute of Technology)并获得数学学士学位；1967年在魏茨曼科学研究所(Weizmann Institute of Science)获得应用数学博士学位，博士论文题目为“Calculation of Tides in the Ocean”。在美国斯坦福大学做博士后研究期间，普纽埃利的学术兴趣转向计算机科学领域。在1968年回到以色列之后，普纽埃利先在魏茨曼科学研究所应用数学系任职，然后在1973年转到特拉维夫大学(Tel Aviv University)，创立了该校的计算机系并且担任第一任系主任。1981年，普纽埃利回到魏茨曼科学研究所担任教授，从1999年直到他2009年去世，他也一直担任美国纽约大学的教授。1999年，由于“发明了时态逻辑和其他用于设计和验证软件和系统的工具(For the invention of temporal logic and other tools for designing and verifying software and systems.)”，普纽埃利被选为美国工程院外籍院士。2000年，普纽埃利获得以色列国家奖(Israel Prize)。[2-4]

    请读者注意，上述ACM颁发图灵奖给普纽埃利的表彰词是准确的，而美国工程院对普纽埃利之功绩的说明并不准确，现代时态逻辑的创立者是普莱尔[5]而并非普纽埃利，后者仅是将时态逻辑引入了计算机科学领域。实际上，在论文[1]中，普纽埃利明确地说明了他提出的两个时态推理系统是基于并扩展以往的时态逻辑并给出了参考文献。计算机界不少学者和文献将普纽埃利誉为时态逻辑的创始人是对时态逻辑现代史和普纽埃利工作的误解。

    1977年，普纽埃利在FOCS会议上发表了其学术生涯最著名的论文：“The Temporal Logic of Programs”[1]，这是时态逻辑在计算机科学领域的第一篇论文，将时态逻辑引入到计算机科学，开创了时态逻辑在计算机科学领域内的应用，对计算机程序/系统正确性验证方向上的后续工作产生了深远的影响。

    计算机程序文本是对其规定的计算在被计算机执行时呈现出动态行为的静态描述。尽管程序设计语言所提供的三种基本控制结构（顺序执行、条件分支、循环）描述手段足以表达所有算法，但是计算机程序文本中的语句与程序执行过程中的动态行为之间的对应却不是清晰的，这就使得确认计算机程序文本是否保证了算法描述及执行的正确性相当困难。英国的霍尔(Tony Hoare, 1934-, 1980年ACM图灵奖获奖者)于1969年首创了程序设计语言的公理语义（霍尔逻辑，通过对程序语句或程序片段的前置条件和后置条件的描述来规定程序动作的效果），基于经典数理逻辑一阶谓词演算来验证程序正确性的方法论[6]。但是，对于在动态执行中有多条并行控制流/线程的并发程序来说，传统的经典数理逻辑及霍尔逻辑在表达上的局限性使得它们并非理想的形式化验证工具。

    普纽埃利在论文[1]中提出，用线性时态逻辑的形式语言来明晰地表达并发程序动态行为及其与时间和多控制流/线程相关各种性质（安全性、活性、优先性等），基于时态逻辑来验证并发程序是否满足必要的性质。普纽埃利突破了经典数理逻辑难于描述并发程序持续动态行为的局限，提供了一种清晰地基于时间线性序列的程序分析验证方法，开辟了程序验证领域的新方向，从而引发了众多关于时态逻辑在计算机科学中应用的研究，推动了形式化方法的理论发展。

    普纽埃利本人及其同事和学生在这个方向上做了许多重要的奠基性工作[7-27]，使得基于时态逻辑的程序/系统分析验证方法如今已经发展成为计算机科学、计算机工程、软件工程中一个极为重要的方法论[28-34]。

参考文献

[1] A. Pnueli, “The Temporal Logic of Programs,” Proceedings of IEEE 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46-57, 1977.  

[2] “Amir Pnueli - ACM A. M. Turing Award Laureate,” ACM. 

[3] D. Harel and M. Y. Vardi, “Amir Pnueli - 1941–2009,” Memorial Tributes of the Na1onal Academy of Engineering, Volume 16, pp. 239-242, Na1onal Academy of Engineering. 

[4] K. R. Apt and L. D. Zuck, “In Memoriam of Prof. Dr. Amir Pnueli - 1941–2009,” European Association for Theoretical Computer Science (EATCS). 

[5] 程京德，“现代时态逻辑的创始者 - 普莱尔”， 微信公众号“数理逻辑与哲学逻辑”，科学网博客，2025年1月6日。

[6] C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,” Communications of the ACM, Vol. 12, No. 10, pp. 576-580, 1969.

[7] A. Pneuli, “The Temporal Semantics of Concurrent Programs,” Theoretical Computer Science, Vol. 13, pp. 45-60, 1981.

[8] A. Pnueli, “Linear and Branching Structures in the Semantics and Logics of Reactive Systems,” In: W. Brauer (Ed), “Automata, Languages, and Programming, 12th Colloquium, Nafplion, Greece, July 15-19, 1985, Proceedings,” Lecture Notes in Computer Science, Vol 194. pp. 15-32, Springer, 1985.

[9] A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends,” In: J. W. Bakker, W. -P. Roever, and G. Rozenberg (Eds.), “Current Trends in Concurrency: Overviews and Tutorials,” Lecture Notes in Computer Science, Vol 224. pp. 510-584, 1986.

[10] A. Pnueli, “System Specification and Refinement in Temporal Logic,” In: R. Shyamasundar (Ed.), “Foundations of Software Technology and Theoretical Computer Science: 12th Conference, New Delhi, India, December 18–20, 1992, Proceedings,” Lecture Notes in Computer Science, Vol. 652, pp. 1-38, Springer, 1992.

[11] A. Pnueli and H. Eyal, “Applications of Temporal Logic to the Specification of Real Time Systems (Invited Talk),” In: M. Joseph (Ed.), “Formal Techniques in Real-Time and Fault-Tolerant Systems, Proceedings of a Symposium, Warwick, UK, September 22-23, 1988,” Lecture Notes in Computer Science, Vol. 331, pp. 84-98, Springer, 1988.

[12] A. Pnueli and and L. D. Zuck,“Probabilistic Verification,” Information and Computation, Vol. 103, No. 1, pp. 1-29, 1993.

[13] A. Pnueli and A. Zaks, “PSL Model Checking and Run-Time Verification via Testers,” In: J. Misra, T. Nipkow, and E. Sekerinski (Eds.),“FM 2006: Formal Methods: 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings,” Lecture Notes in Computer Science, Vol. 4085, pp. 573-586, Springer, 2006.

[14] D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, “On the temporal analysis of fairness,” Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 163-173, 1980.

[15] M. Ben-Ari, Z. Manna, and A. Pnueli, “The Temporal Logic of Branching Time,” Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 164-176, 1981.

[16] D. Harel and A. Pnueli, “On the Development of Reactive Systems,” In: K. R. Apt (Eds), “Logics and Models of Concurrent Systems,” NATO ASI Series, Vol 13， pp. 477-498, Springer, 1985.

[17] D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot, “Statemate: A Working Environment for the Development of Complex Reactive Systems,” IEEE Transactions on Software Engineering, Vol. 16, No. 4, pp. 403-414, 1990. 

[18] D. Peled, S. Katz, and A. Pnueli, “Specifying and Proving Serializability in Temporal Logic,” Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science (LICS91), pp. 232-244, 1991.

[19] Y. Kesten, Z. Manna, and A. Pnueli, “Temporal Verification of Simulation and Refinement,” In: J. W. de Bakker, G. Rozenberg, and W. -P. de Roever (Eds.), “A Decade of Concurrency: Reflections and Perspectives: REX School/Symposium, Noordwijkerhout, The Netherlands, June 1993, Proceedings,” Lecture Notes in Computer Science, Vol. 803, pp. 273-346, Springer, 1994.

[20] Y. Kesten, A. Pnueli, and L. Raviv, “Algorithmic Verification of Linear Temporal Logic Specifications,” In: K. G. Larsen, S. Skyum, and G. Winskel (Eds.), “Automata, Languages and Programming: 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13–17, 1998, Proceedings,”Lecture Notes in Computer Science, Vol. 1443, pp. 1-16, Springer, 1998.

[21] Z. Manna and A. Pnueli, “Verification of Concurrent Programs: Temporal Proof Principles.” In: D. Kozen (Ed.), “Logics of Programs: Workshop, Yorktown Heights, New York, May 1981,” Lecture Notes in Computer Science, Vol. 131, pp. 1-38, Springer, 1982.

[22] Z. Manna and A. Pnueli, “The Anchored Version of the Temporal Framework,”In: J. W. Bakker, W. -P. Roever, and G. Rozenberg (Eds.), “Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency: School/Workshop, Noordwijkerhout, The Netherlands May 30–June 3, 1988,” Lecture Notes in Computer Science, Vol. 354, pp. 201-284, Springer, 1989.

[23] Z. Manna and A. Pnueli, “A Hierarchy of Temporal Properties (invited paper 1989),” Proceedings of the 9th Annual ACM Symposium on Principles of Distributed COmputing (PODC), pp. 377-410, 1990. 

[24] Z. Manna and A. Pnueli, “Verification of Parameterized Programs,” In: E. Börger (Ed.), “Specification and Validation Methods,” pp. 167-230, Oxford University Press, 1993.

[25] Z. Manna and A. Pnueli, “The Temporal Logic of Reactive and Concurrent Systems: Specifications,” Springer, 1992. 

[26] Z. Manna and A. Pnueli, “Temporal Verification of Reactive Systems: Safety,” Springer, 1995. 

[27] Z. Manna and A. Pnueli, “Temporal Verification of Reactive Systems: Response,” In： Z. Manna and D. A. Peled (Eds), “Time for Verification: Essays in Memory of Amir Pnueli,” Lecture Notes in Computer Science, Vol. 6200, pp. 279-361, Springer, 2010. 

[28] J. D. Gannon, “Verification and Validation,” In A. B. Tucker (Ed.), “Computer Science Handbook,” Chapman&Hall and ACM, 1997, 2004(2nd Edition). 

[29] V. S. Alagar and K. Periyasamy, “Specification of Software Systems,” Springer, 1998, 2011(2nd Edition). 

[30] C. Baier and J. -P. Katoen, “Principles of Model Checking,” MIT Press, 2008.

[31] M. Fisher, “An Introduction to Practical Formal Methods Using Temporal Logic,” John Wiley & Sons, 2011.

[32] E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem (Eds.), “Handbook of Model Checking,” Springer, 2018. 

[33] R. Drechsler (Ed.), “Formal System Verification: State of the Art and Future Trends,” Springer, 2018.

[34] M. Huisman and A. Wijs, “Concise Guide to Software Verification: From Model Checking to Annotation Checking,” Springer, 2023.

微信公众号“数理逻辑与哲学逻辑”