Real-time and hybrid systems have been studied so far under the assumption of finite variability. In this paper, we consider models in which systems exhibiting finite divergence can also be analysed. In such systems the state of the system can change infinitely often in a finite time. This kind of behaviour arises in many notations of hybrid systems, and also in theories of non-linear systems. The aim, here, is to provide a theory where pathological behaviour such as finite divergence can be analysed -- if only to prove that it does not occur in systems of interes. Finite divergence is studied using the framework of Duration Calculus. Axioms and proof rules are given. Patterns of occurrence of divergence are classified into dense divergence, accumulative divergence and discrete divergence by appropriate axioms. Induction rules are given for reasoning about discrete divergence.
Duration Calculus is a real-time interval logic which can be used to specify and reason about timing and logical constraints on discrete states in a dynamic system. It has been used to specify and verify designs for a number of real-time systems. This paper extends the Duration Calculus with notations to capture properties of piecewise continuous states. This is useful for reasoning about hybrid systems with a mixture of continuous and discrete states. The proof theory of Duration Calculus is extended such that results proven using mathematical analysis can be used freely in the logic. This provides a flexible interface to conventional control theory. {\bf Keywords:}Requirements, software design, hybrid systems, real-time systems, control theory, interval logic, durations.
