Publications

 In 1996, Zhou Chaochen and Michael Hansen proposed a first order interval logic called Neighbourhood Logic (NL) which can specify liveness and fairness of computing systems and also define notions of real analysis in terms of expanding modalities introduced therein. Here, we first show that NL forms a sound and complete system. Next, we extend NL by introducing two more expanding modalities in the upward and downward directions and propose a Two Dimensional Neighbourhood Logic (NL$^2$), which can be used to specify super-dense computation. Finally, we also prove completeness of this new NL$^2$ .

 The super-dense computation model provides an abstraction of real-time behaviour of computing systems. Logics to deal with this model are being studied. In the paper, we propose a combination of a linear temporal logic and an interval logic, and demonstrate how this combination can be used to specify a real-time semantics of an OCCAM-like programming language and its real-time properties, where the super-dense computation model is adopted.

 This paper is a sequel of [FYZ95]. It presents a geometric approach to solving the inverse kinematics for all 3-joint placeable robotic manipulators. The distinct feature of this approach is that it uses geometric variables such as length, area ratio and Pythagoras difference to find the closed form solutions. It is proved in the paper that for any 3-joint placeable manipulator there exists a geometric variable which keeps constant during the evolution of the manipulator. With this invariant a characteristic equation of the manipulator can be derived and can be transformed into a polynomial equation with degree four. Therefore the closed form solution of the 3-joint placeable manipulator can be obtained. A characteristic equation of the 3-revolute-joint manipulator produced by this approach with assistance of Maple is listed in the Appendix of the paper. The possible application of this geometric approach for 6-joint manipulator is also discussed in the paper.

 This paper is a sequel of [FYZ95]. It presents a geometric approach to solving the inverse kinematics for all 3-joint placeable robotic manipulators. The distinct feature of this approach is that it uses geometric variables such as length, area ratio and Pythagoras difference to find the closed form solutions. It is proved in the paper that for any 3-joint placeable manipulator there exists a geometric variable which keeps constant during the evolution of the manipulator. With this invariant a characteristic equation of the manipulator can be derived and can be transformed into a polynomial equation with degree four. Therefore the closed form solution of the 3-joint placeable manipulator can be obtained. A characteristic equation of the 3-revolute-joint manipulator produced by this approach with assistance of Maple is listed in the Appendix of the paper. The possible application of this geometric approach for 6-joint manipulator is also discussed in the paper.

 Inspired by [He94], a language to describe hybrid systems, i.e. networks of communicating discrete and continuous processes, is proposed. A semantics of the language is given in Extended Duration Calculus [ZRH93], a real-time interval logic with a proof system that allows reasoning in mathematical analysis about continuous processes to be embedded into the logic. The semantics thus provides a secure link to hybrid system models based on a general theory of dynamical systems.

 This paper introduces infinite intervals into the Duration Calculus. The extended calculus defines a state duration over an infinite interval by a property which specifies the limit of the state duration over finite intervals, and excludes the description operator. Thus the calculus can be established without involvement of unpleasant calculation of infinity. With limits of state durations, one can treat conventional liveness and fairness, and can also measure out liveness and fairness by properties of limits. Including both finite and infinite intervals, the calculus can, in a simple manner, distinguish between terminate behaviour and nonterminate behaviour, and therefore directly specify and reason about sequentiality.

 This paper presents a geometric method to solve the inverse kinematics for a class of 3-joint placeable robotic manipulators. A distinct feature of the method is that a mechanical geometric reasoning process is used for replacing conventional algebraic calculations. The conventional algebraic method solves the problem by finding analytic solutions of arm equations of robotic manipulators. Arm equations are usually polynomial equations, algebraic calculations in finding the solutions are always very complicated, and even fail for some cases of 3-joint non-loose placeable manipulators [P91]. The geometric method presented in this paper specifies manipulators in terms of vectors, instead of arm equations, and employ reasonings about geometric variables such as volume, area, length and Pythagoras difference, instead of algebraic calculations. It can decide whether a 3-joint placeable manipulator is loose, and can mechanically find out analytic solutions of the inverse kinematics for any non-loose one. The method is therefore simple and understandable.

 In this paper, a hybrid system design method, based on cooperation between two disciplines -- control theory and computing science, is presented. The method suggests to decompose a hybrid system into control loops and decision loops. The external behaviour of control loops are specified in a notation, which is understandable by the two disciplines, while designs of control loops employ theory of differential equations. The correctness of the designs of control loops is guaranteed by control engineers analytically or experimentally. Decision loops are designed by computing engineers, and, based on the specifications of control loops, the verification of system requirements can be done by a reasoning mechanism of the notation. Two examples of the problem of inverted pendulum are given for illustration, and the Mean Value Calculus is chosen as the formal notation for specifying control loops and designing decision loops.

 This paper addresses the problem of modeling railway systems. We use both Mean Value Calculus and Extended Duration Calculus to specify railway systems. For railway line, signal system is discussed and a simple scheduling strategy is presented, which result in safety and liveness of railway line; For linear railway region, both running map and feasibility conditions are described. The framework to verify correctness of scheduling, i.e. the running map satisfies feasibility conditions, is also presented.

 This paper deals with dependability of imperfect implementations concerning given requirements. The requirements are assumed to be written as formulas in Duration Calculus. Implementations are modeled by continuous semi-Markov processes with finite state space, which are expressed in the paper as finite automata with stochastic delays of state transitions. A probabilistic model for Duration Calculus formulas is introduced, so that the satisfaction probabilities of Duration Calculus formulas with respect to semi-Markov processes can be defined, reasoned about and calculated through a set of axioms and rules of the model.

 The research on hybrid control systems attracts many scientists both in computer science and control theories and applications. The study should be carried out on a general framework abstracted from various hybrid control systems. This paper analyses the drawbacks of the present frameworks used by most researchers and proposes a new framework to overcome these shortcomes. The new framework consists of a discrete time box, a discrete event box and a digital-symbol interface. The new framework shows the crucial nature of the hybridity of time envolving variables and event driven variables in hybrid control systems. The new framework is easy to integrate the knowledges of computer science and control theories and applications. Two examples, a gas burner and an inverse pendulum are given to show the fitness of the new framework. The design and analysis aspects of hybrid control systems related to the new framework are also discussed.

 Most results obtained in the research of hybrid control systems are related to the description and analysis of hybrid control systems. But it is doubtless that how to design a hybrid control system is of great significance in the research of hybrid control systems. This paper is devoted to discuss the design methodology of hybrid control systems. After an introduction of a new framework of hybrid control systems, a top-down design approach is proposed which is consistent to the framework. The approach consists of decomposition of system performance specifications, the design of discrete event driven decision maker and the design of digital control loops. Two examples, a gas burner and an inverse pendulum are systematically designed to show the goodness of the top-down design approach. Finally, a bottom-up analysis approach which is consistent to the new framework is proposed and then applied to these examples.

 This paper presents an approach to formalizing and proving real-time properties of schedulers. The formal logic that we propose to use is the Duration Calculus, and the scheduler that we select here to serve as an example is the Deadline Driven Scheduling Algorithm. The specification and proof of the algorithm are formulated abstractly by using the Duration Calculus. The result may encourage others to formally treat more real-time aspects of operating systems which are conventionally a piece of ad hoc territory in computer science.

 In this paper we formulate the design of digital dynamic systems using a programming notation, called Hybrid CSP. A continuous specification of such a system under some performance requirements is decomposed and digitized using Hybrid CSP, whose correctness is guaranteed by the control principles such as Shannon's Sampling Theorem. Therefore, a digital dynamic system can be specified and refined in a framework of formal development approach.

 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.

 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.

 This paper is to present an algorithm to decide whether a real-time system satisfies a set of invariants which are constructed from linear inequalities of integrated durations of system states. Real-time systems in the paper are taken to be real-time automata which set up for each of state transitions a lower time bound and an upper time bound. The satisfaction problem can be translated into a family of {\em linear programming problems}. The algorithm is, according to the invariants, to reduce the infinite family of linear programming problems to an equivalent one with only finite members, and then to solve each of linear programming problems efficiently. The algorithm is so simple that no prerequisite of linear programming theory is assumed.

 The Duration Calculi are calculi for designing real-time software embedded systems. The Calculi overviewed in the paper include the Duration Calculus, the Extended Duration Calculus, the Mean Value Calculus and the Probabilistic Duration Calculus. They are extensions of an Interval Temporal Logic, and can accommodate some concepts of mathematical analysis such as integrals, mean values, piecewise continuity and differentiability of functions over continuous time. The Calculi can be used to capture and refine real-time requirements for hybrid systems, to define real-time behaviour/semantics of computing systems, and to calculate system dependability in terms of requirement satisfaction probability.