Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus - Formal Methods and Hybrid Real-Time Systems - page 170

Specifying Various Time Models with Temporal
Propositional Variables in Duration Calculus

Dang Van Hung

The United Nations University
International Institute for Software Technology
P.O. Box 3058, Macau
[e-mail]

Abstract. Many extensions of Duration Calculus (DC) have been pro-
posed for handling different aspects of real-time systems. For each exten-
sion several different semantics are defined for different time structures
which are suitable for different applications and achieve low complexity
for the decidability of some properties. Hence, different proof systems
have to be developed for reasoning in different calculi. We demonstrate
that with temporal propositional letters, many useful time structures
and operators can be completely described in the original DC with con-
tinuous time. Hence, we can use the proof system for original DC and
the specification of the specific time structure to reason in that time
structure without the need of introducing a new calculus.

1 Introduction

Since it was introduced in 1992 by Zhou, Hoare and Ravn [3], Duration Calculus
(DC) has attracted a great deal of attentions. Details on DC are presented in
Zhou and Hansen's monograph [2]. Many extensions of Duration Calculus have
been proposed for handling different aspects of real-time systems [15,5]. For
each extension several different semantics are defined for different time struc-
tures which are suitable for different applications and have low complexity for
the decidability of some properties [13,9]. Among the different time structures,
the abstract time domain makes the calculus complete when it is abstracted
away from dedicated properties of real numbers or natural numbers [6], and
the discrete time domain makes the calculus decidable, able to carry out model
checking, and suitable for the specification of digital systems [14,13,8]. When
proposing a new time domain, one has to give semantics and develop a proof
system for the calculus within the given semantics. This sometimes makes the
calculus inconvenient to use. We found that in most cases, the proof system for
the calculus on special domains is the original one with some small modification.
Therefore, it would be convenient if we can use the original calculus without any
modification for different applications which can still capture special aspects of
the application domains. From our earlier works on specification and reasoning
about real-time systems with Duration Calculus [10,11], we found that it is very
convenient to use temporal propositional letters with specific meaning to specify