Publications

 Reports on the status of UNU-IIST and its activities after the first 6 months of operation 

 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.

Presents the co-ordinates along, and principles according to which UNU-IIST will select and pursue its Programmatic Activities the next couple of years

 Distributed only with authors / publishers permission

 This is a compendium of 4 papers:

• [(a)] Dines Bjørner. Trustworthy Computing Systems: The ProCoS Experience, February, 1992. Published in: 14th International Conf. on Software Engineering, Melbourne, Australia, May 11-15, 1992, pp. 15-34.
• [(b)] Dines Bjørner and Jørgen Fischer Nilsson. Algorithmic & Knowledge Based Methods -- Do they "Unify"? Published in: International Conf. on Fifth Generation Computer Systems: FGCS'92, Tokyo, June 1-5, 1992 (separate folder, pp. 191-198).
• [(c)] Dines Bjørner. From Research to Practice: Self-reliance of the Developing World through Software Technology -- Usage, Education & Training. Published in: IFIP Transaction, IFIP World Congress '92, Madrid, September 7-11, 1992, pp. 65-71.
• [(d)] Dines Bjørner. A Rôle for UNU-IIST: Developing Countries' Access to New Information Technologies. Presented at: Access to Science and Technology, The Rôle of Information Technology, Kyoto University and UNU Symp., Kyoto, May 12-14, 1992; Expected publ. by UNU Press.

Distributed only with publishers permission

 A mean value calculus is presented. It is an extension of the Duration Calculus. The calculus reasons about mean values of durations of Boolean functions instead of integrals. With mean values, we can define integrals and specify point values of functions, and therefore instant actions, including state transitions and events. A state transition of a system determines the system states in a neighbourhood of the transition, and is called a state germ using terminology from topology. State transitions of an automaton are caused by events. Thus the behaviour of an automaton can be formulated by predicates of events and state germs. As an application of the calculus, state germs and their inference rules are introduced and are used to specify and reason about combinational circuits and automata. {\bf Keywords:}Duration Calculus, Mean Value Calculus, State Germs,Combinational Circuit, Automata,Real-Time System.

 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.

 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.

 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 part speculative, part technical, and mostly discursive! The paper is also comprehensive and should be readable by a large fraction of the software community. The conjectures of the paper are based on more than 30 years of extensive experience in computing and software systems development: in the formal, abstract specification of software system architectures, and in their stepwise implementation. The conjecture of the paper is this: For a software house, a producer of products, to be able, in future, to compete effectively it must possess: (i) deep and broad (large scale) problem domain knowledge represented in the form of `mathematical theories of application domains', (ii) ready access to `software devices and mechanisms', and (iii) otherwise pursue development steadily using a large variety of `design calculi'. The paper will define the single-quoted concepts, and will illustrate large-scale applications.

This paper proposes and investigates an approach to deduction in probabilistic logic, using as its medium a language that generalizes the propositional version of Nilsson's probabilistic logic by incorporating conditional probabilities. Unlike many other approaches to deduction in probabilistic logic, this approach is based on inference rules and therefore can produce proofs to explain how conclusions are drawn. We show how these rules can be incorporated into an anytime deduction procedure that proceeds by computing increasingly narrow probability intervals that contain the tightest entailed probability interval. Since the procedure can be stopped at any time to yield partial information concerning the probability range of any entailed sentence, one can make a tradeoff between precision and computation time. The deduction method presented here contrasts with other methods whose ability to perform logical reasoning is either limited or requires finding all truth assignments consistent with the given sentences.

 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.