On the completeness and decidability of Duration Calculus with iteration. Theoretical Computer Science

The extension of the Duration Calculus (DC) by iteration, which is also known as Kleene star, enables the straightforward specification of repetitive behaviour in DC and facilitates the translation of design de-scriptions between DC, timed regular expressions and timed automata. In this paper we present axioms and a proof rule about iteration in DC. We consider abstract-time DC and its extension by a state-variable bind-ing existential quantifier known as higher-order DC (HDC). We show that the ω-complete proof systems for DC and HDC known from our ear-lier work can be extended by our axioms and rule in various ways in order to axiomatise iteration completely. The additions we propose include ei-ther the proof rule or an induction axiom. We also present results on the decidability of a subset of the extension DC ∗ of DC by iteration