中介时序逻辑系统MTL的模型论性质

The Model Characters of Medium Temporal Logic

时序逻辑作为一种把时间概念直接引入其形式系统的逻辑系统,它具有较强的表达能力,近年来在计算机科学领域获得了广泛的应用.基于中介逻辑对时序逻辑进行多值扩充,建立了一种中介时序逻辑系统MTL(Medium Temporal Logic).讨论了它的形式系统和语义解释,但未论及其完备性.本文对MTL系统作进一步的讨论.在一可传结构下,讨论了它的可传、连通和过滤等模型论性质,为进一步讨论MTL系统的完备性作了理论上的准备.

Temporal logic, as a system of logic in which the concept of time is directly built in-to the formalism, has a good expression as a specification language for programs. It has beenwidely used in the field of computer science in recent years. The authors have extended tempo-ral logic to a system of MTL (Medium Temporal Logic) based on the medium logic. The for-mal system had been discussed about MTL and the semantics of MTL had been studied lastyear, but it didn't show its completeness. This paper continuously discusses the system ofMTL. Based on a transtive frame, it study some model characters of MTL which aretranstive, connected and filtration. Making use of these model characters, the completeness ofMTL will be able to be proved.