TDL——一种适于研究并发控制问题的逻辑

TDL——一种适于研究并发控制问题的逻辑 TDL—A LOGIC FOR STUDYING CONCURRECY CONTROL PROBLEM 刘玉珍 Liu Yuzhen Li Qiongzhang 1 first-author 李琼章 1 武汉大学计算机科学系 武汉大学计算机科学系 Department of Computer Science,Wuhan University Department of Computer Science,Wuhan University 本文讨论适于研究并发控制问题的逻辑。由于现有某些逻辑（如动态逻辑、时态逻辑）的缺陷,因此我们提出了程序逻辑 TDL,它是时态逻辑的扩展,它易于研究并发程序,能表达程序的输入一输出性质和时态性质,并提供合成的开发证明方法。本文先讨论时态逻辑TL 和程序集 PG,然后定义程序逻辑 TDL 及证明系统 PT 并讨论它的表达能力,最后说明PT 的相对合理性和完全性。 This article discusses a logic for studying concurrency control problem. Because of some shortages of logics,such as dynamic logic and temporal logic,we present the program logic TDL.It is an extension of temporal logic and suited to study concurrent programs.It can express the input-output and temporal properties of program and provide a compositional development and proof method.First,we discuss the temporal logic TL and program set PG, then we define the program logic TDL and its proof system PT,and discuss its expressive power Finally we prove the relative soundness and completeness of the PT. 时态逻辑 动态逻辑 合理性 完全性 并发控制 temporal logic dynamic logic soundness completeness concurrency control 1990-02-01 2021-04-01 2