两维时间域上的一种区间逻辑

AN INTERVAL LOGIC IN TWO DIMENSIONAL TIME

为了给超稠密计算模型（Ｓｕｐｅｒ－ｄｅｎｓｅｃｏｍｐｕｔａｔｉｏｎ）建立一种逻辑工具，首先定义了一个两维的超稠密时间域，在这个时间域上定义了一种区间逻辑，并提出了该逻辑的一个推理系统．并用轨道概念定义了两维超稠密空间中的计算、时段等．

The behaviours of reactive systems are more difficult to catch when the factor of time is taken into account. From the practical pointer of view, it is necessary and important. Super dense computation model is an important abstract model of real time reactive systems proposed by Z. Manna and A. Pnueli. In this model, discrete behaviors of the systems are abstracted as instantaneous, ordered actions. This simplifies the reasoning about the systems. For building a logic tool for this computation model, this paper defines first a two dimensional super dense time space, and an interval logic in this space. Then, it proposes an inference system for this logic, including the necessary axioms and inference rules. The concepts of computation and duration are defined with the concept of trajectories in this time space and finite variability. Finally, some relative problems are discussed.