A higher-order duration calculus and its completeness  

作　　者：詹乃军 

机构地区：[1]Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China

出　　处：《Science China(Technological Sciences)》2000年第6期625-640,共16页中国科学（技术科学英文版）

摘　　要：This paper studies how to describe the real-time behaviour of programs using duration calculus. Since program variables are interpreted as functions over time in real-time programming, and it is inevitable to introduce quantifications over program variables in order to describe local variable declaration and declare local channel and so on. Therefore to establish a higher-order duration calculus (HDC) is necessary. We first establish HDC, then show some real-time properties of programs in terms of HDC, and then, prove that HDC is complete on abstract domains under the assumption that all program variables vary finitely.This paper studies how to describe the real-time behaviour of programs using duration calculus. Since program variables are interpreted as functions over time in real-time programming, and it is inevitable to introduce quantifications over program variables in order to describe local variable declaration and declare local channel and so on. Therefore to establish a higher-order duration calculus (HDC) is necessary. We first establish HDC, then show some real-time properties of programs in terms of HDC, and then, prove that HDC is complete on abstract domains under the assumption that all program variables vary finitely.

关 键 词：DURATION CALCULUS HIGHER-ORDER LOGICS real-time programs super-dense computation completeness. 

分 类 号：O172[理学—数学]