Publications

 We extend Duration Calculus to a logic which allows description of Discrete Processes where several steps of computation can occur at the same time point. Moreover, the order of occurrence of these steps is relevant. The resulting logic is called Duration Calculus of Weakly Monotonic Time (WDC). It allows effects such as true synchrony and digitisation to be modelled. As an example, We formulate a new semantics of Timed CSP assuming that the communication and computation take no time. We also outline a semantics of shared variable concurrency under similar assumptions. We introduce a notion of deformation of time in (WDC). We study the duration calculus properties which remain invariant under such deformation of time.

 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 (or DC in short) presents a formal notation to specify properties of real-time systems and a calculus to formally prove such properties. Decidability is the underlying foundation to automated reasoning. But, excepting some of its simple fragments, DC has been shown to be undecidable. DC takes the set of real numbers to represent time. The main reason of undecidability comes from the assumption that, in a real-time system, state changes can occur at any time point. But an implementation of a specification is ultimately executed on a computer, and there states change according to a system clock. Under such an assumption, it has been shown that the decidability results can be extended to cover relatively richer subsets of DC. In this report, we extend such decidability results to still richer subsets of DC. Under the assumption that states change at real-numbered points, it has been shown that a propositional fragment of DC is undecidable. We also show that the same set still remains undecidable, even if we restrict that states change at points as designated by rational numbers.

 A hybrid system is a system containing both of time-evolving components and event-driven components. A formal approach is explored in this paper, based on Extended Duration Calculus (EDC), for the development of hybrid systems. A typical example of hybrid system from modern control theory, a two-level adaptive control system is used for illustrating our approach. Its high level consists of an event-driven supervisor which reacts to the change of plant structure, and its time-evolving low level consists of adaptive controllers and other components. Firstly performance specifications and system specification of the case are formulated in EDC; then they are refined stepwisely into specifications of the supervisor and the low level components. Our approach emphasizes the interface between the two kinds of components in the hybrid system.