用高阶逻辑表达时态逻辑及其应用

EXPRESSING TEMPORAL LOGIC IN HIGHER-ORDER LOGIC AND ITS APPLICATIONS

硬件设计的形式化验证技术开辟了对复杂的超大规模集成电路设计进行验证的新途径,高阶逻辑和时态逻辑在形式化验证技术中均得到成功的应用,本文介绍用高阶逻辑表达线性时态逻辑和区间时态逻辑的方法,并以几个简单实例说明它在硬件设计验证中的应用,这种方法的优点是既利用高阶逻辑系统HOL的机械化定理证明手段,又发挥了时态逻辑的表达硬件的动态性质的能力。

This paper presents a method of expressing linear temporal logic and interval temporal logic in higher-order logic and gives some examples of proving the correctness of simple circuits.The method takes the advantages of both mechanized HOL facilities and expressing power of temporal logic.It can be used to deal with the timing problems of VLSI system.