From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus

The duration calculus (DC) is a formal, algebraic system for specification and design of realtime systems, where real numbers are used to model time and (Boolean valued) functions to formulate requirements. Since its introduction in 1991 by Chaochen, Hoare and Ravn it has been applied to many case studies and has been extended into several directions. E.g., there is an extension for specifying liveness and safety requirements. In the original duration calculus the authors used knowledge about temporal logics and established a connection with security systems and intervals. In 1997 Hansen and Chaochen showed that DC extends interval logic (IL) based on [Dut95a, Dut95b]. Many times the connection between DC and linear temporal logic have been investigated. In most of the papers with DC-related topics the examples of a leaking gas pipe and of the leaking gas burner are discussed. These examples are also given by Chaochen et al. Von Karger investigated the embedding of the DC in sequential algebras. For these purposes he established the proof principle of engineer’s induction. Independently of DC there is the algebraic structure of Kleene algebra (KA). It is an idempotent semiring with an additional unary operator called the Kleene star. This operation models finite iteration. Kleene algebras are well known structures. E.g., Kozen proved many of their fundamental properties. Möller and Desharnais have also shown various results, applications and algorithms of Kleene algebras. A nearly full survey is given in [DMS03, DMS04]. A first step for combining the two ideas (KA and DC) is given by Dima in 2000. There he developed a Kleene algebra with the power set of real numbers P(R+) as carrier set. Furthermore he pointed out once more that the real numbers are one of the main constructs in time analysis. This report presents the duration calculus on the basis of Kleene algebra. Doing this we will analyse the DC in a new view