Duration Calculus and its Treatment for Continuous Time

Prof. Zhou Chaochen
United Nations University/IIST Macau

The Duration Calculus (abbreviated DC) represents a logical approach to formal design of real-time systems. DC is based on interval logic, and uses the real numbers to model continuous time, and Boolean-valued (i.e. {0,1}-valued) functions over time to model states and events of real-time systems. The duration of a state in a time interval is the accumulated presence time of the state in the interval. DC extends interval logic with a calculus to specify and reason about properties of state durations. This talk will give a brief introduction to DC, and explain how DC keeps the essence of discrete time when it adopts continuous time, so that continuous time becomes tractable in terms of computing science. The explanation will refer to the induction rules of DC, its model checking tool and its application to real-time programming.