Computing maximal weak and other bisimulations

We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.     

QPSchur: A dual, active-set, Schur-complement method for large-scale and structured convex quadratic programming

We describe an active-set, dual-feasible Schur-complement method for quadratic programming (QP) with positive definite Hessians. The formulation of the QP being solved is general and flexible, and is appropriate for many different application areas. Moreover, the specialized structure of the QP is abstracted away behind a fixed KKT matrix called K_o and other problem matrices, which naturally leads to an object-oriented software implementation. Updates to the working set of active inequality constraints are facilitated using a dense Schur complement, which we expect to remain small. Here, the dual Schur complement method requires the projected Hessian to be positive definite for every working set considered by the algorithm. Therefore, this method is not appropriate for all QPs. While the Schur complement approach to linear algebra is very flexible with respect to allowing exploitation of problem structure, it is not as numerically stable as approaches using a QR factorization. However, we show that the use of fixed-precision iterative refinement helps to dramatically improve the numerical stability of this Schur complement algorithm. The use of the object-oriented QP solver implementation is demonstrated on two different application areas with specializations in each area; large-scale model predictive control (MPC) and reduced-space successive quadratic programming (with several different representations for the reduced Hessian). These results demonstrate that the QP solver can exploit application-specific structure in a computationally efficient and fairly robust manner as compared to other QP solver implementations.     

Deadlock analysis in networks of communicating processes

We use the failures model of CSP to describe the behaviour of a class of networks of communicating processes. This model is well suited to reasoning about the deadlock potential of networks. We introduce a number of simple conditions on networks which aid deadlock analysis either by localizing the analysis required for a proof of deadlock-freedom or by restricting the circumstances in which deadlock could occur. In particular, we formulate some simple theorems which characterize the states in which deadlock can occur, and use them to prove some theorems on the absence of global deadlock in systems. We identify a special class of unidirectional networks and develop specialized results on their deadlock-freedom. We develop more general methods based on (at most) pairwise local deadlock analysis in networks, applicable to the large class of conflict-free networks. We introduce a methodology for proving deadlock-freedom in a large network by decomposing it into subnetworks which can be analysed separately. A variety of examples is given to show the utility of these results. We compare our work with earlier work by several other authors, and make some suggestions for future research. S.D. Brookes received a B.A. in mathematics (1978) and a D.Phil. in computer science (1983), both from Oxford University. His D. Phil supervisor was C.A.R. Hoare. He moved to Carnegie Mellon University in 1981, initially as a Research Computer Scientist and then (1984–1990) as an Assistant Professor in the School of Computer Science at CMU. He is currently an Associate Professor of Computer Science at CMU. His research interests include the mathematical foundations of programming languages, the theory of parallel and sequential computation, programming methodology, programming language design, and the development of semantically based logics for reasoning about program behavior. A.W. Roscoe received a B.A. in mathematics (1978) and a D.Phil. in computer science (1982), both from Oxford University. His D. Phil supervisor was C.A.R. Hoare. He was formerly a Junior Research Fellow at St Edmund Hall, Oxford (1980–1982) and the IBM Research Fellow of the Royal Society (1982–1983). Since 1983 he has been a University Lecturer in Computation at Oxford and a Fellow of University College. His research interests include the theory of parallel computing and its applications (e.g., to VLSI design), domain theory, distributed databases, general topology and the theory of image processing.This research was supported in part by funds from the Computer Science Department of Carnegie Mellon University, and by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 4976, monitored by the Air Force Avionics Laboratory under Contract F33615-87-C-1499. A.W. Roscoe gratefully acknowledges support by ONR Grant N00014-87-G-0242. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the offical policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the US Government.     

Alcohols as fuels—The global picture

A number of countries have programs which encourage the production and use of ethanol and methanol to extend gasoline supplies. These programs are often based on food crops which are subject to wide variations in both cost and availability. Some of the programs are reviewed, and the costs of alcohols are compared to world market prices of gasoline.     

Mycotoxins in breakfast cereals from the Canadian retail market: A 3-year survey

One hundred and fifty-six samples of breakfast cereals were collected from the Canadian retail marketplace over a 3-year period. The samples were analysed for the mycotoxins deoxynivalenol, nivalenol, HT-2 toxin, zearalenone, ochratoxin A, and fumonisins B₁ and B₂ to contribute to dietary exposure estimates in support of the development of Canadian guidelines for selected mycotoxins in foods. The samples included corn-, oat-, wheat- and rice-based cereals, as well as mixed-grain cereals, and were primarily from North American processors. Overall, deoxynivalenol was the most frequently detected mycotoxin  — it was detected in over 40% of all samples analysed. Fumonisins and ochratoxin A were each detected in over 30% of all samples. Zearalenone was detected in over 20% of all samples. Nivalenol and HT-2 toxin were each detected in only one sample. The survey clearly demonstrated regular occurrence of low levels of multiple mycotoxins in breakfast cereals on the Canadian market.     

An Externally Powered, Multichannel, Implantable Stimulator for Versatile Control of Paralyzed Muscle

Through the use of semicustom integrated circuit technology, an implantable muscle stimulator has been developed. The unit is small, lightweight, has low power consumption, and is intended for permanent usage. The stimulator circuitry is externally controlled and powered by a single encoded radio frequency carrier. Up to eight independently controlled stimulus output channels are provided, with output channel selection, stimulus pulse width, and stimulus pulse frequency under external control. A constant current biphasic stimulus pulse is used, in which the stimulus current amplitude can be preset by a single resistor value. The stimulator circuitry has been implemented in thick film hybrid form, and has undergone laboratory evaluation for 48 months.     

The pursuit of deadlock freedom

We introduce some combinatorial techniques for establishing the deadlock freedom of concurrent systems which are similar to the variant/invariant method of proving loop termination. Our methods are based on the local analysis of networks, which is combinatorially far easier than analysing all global states. They are illustrated by proving numerous examples to be free of deadlock, some of which are useful classes of network.     

A Taxonomy of Web Services Using CSP

Terms such as conversational and stateless are widely used in the taxonomy of web services. We give formal definitions of these terms using the CSP process algebra. Within this framework we also define the notion of Service-Oriented Architecture. These definitions are then used to prove important scalability properties of stateless services. The use of formalism should allow recent debates, concerning how and whether web services provide standardized access to state, to progress more rigorously.