Completeness of higher-order duration calculus

Abstract. In order to describe the real-time behaviour of programs in terms of Duration Calculus (DC), proposed by Zhou Chaochen, C.A.R. Hoare and A.P. Ravn in [3], which can specify real-time requirements of computing systems, quantifications over program variables are inevitable, e.g. to describe local variable declaration, to declare internal channel and so on. So a higher-order duration calculus (HDC) is established in [2]. This paper proves completeness of HDC on abstract domains by encod-ing HDC into a complete first-order two-sorted interval temporal logic (IL2). This idea is hinted by [9]. All results shown in this paper are done under the assumption that all program variables have finite variability