反应式和并发系统指实时运行的计算系统，如操作系统、控制系统、交互系统和并发系统。这些系统很难规约、实现和验证，主要原因是系统与其环境之间及系统本身的并行进程之间交互的复杂性，在交互时间上的微小变化可能导致完全不同的行为。 时序逻辑是一种形式化规约语言，可用于刻画和分析反应式系统中有关时间和行为方面的属性。它提供了一种简单、自然但精确的方式来讨论交互发生的顺序，而无须采用绝对时间度量。 本书全面介绍了时序逻辑和作者开发的反应式程序的计算模型。 本书是国际著名计算机科学家Zohar Manna和Amir Pnueli（图灵奖得主）的代表作，适合作为计算机、软件工程、人工智能、自动化等专业高年级本科生、研究生的教材或参考书，也可供相关领域的研究人员和技术开发人员参考。