Progress in deriving concurrent programs: Emphasizing the role of stable guards

We present some techniques to obtain smooth derivations of concurrent programs that address both safety and progress in a formal manner. Our techniques form an extension to the calculational method of Feijen and van Casteren using a UNITY style progress logic. We stress the role of stable guards, and we illustrate the derivation techniques on some examples in which progress plays an essential role.

Trace Semantics for the Owicki-Gries Theory Integrated with the Progress Logic from UNITY

The theory of Owicki and Gries has been used as a platform for safety-based verifcation and derivation of concurrent programs. It has also been integrated with the progress logic of UNITY which has allowed newer techniques of progress-based verifcation and derivation to be developed. However, a theoretical basis for the integrated theory has thus far been missing. In this paper, we provide a theoretical background for the logic of Owicki and Gries integrated with the logic of progress from UNITY. An operational semantics for the new framework is provided which is used to prove soundness of the progress logic.

Probabilistic Action System Trace Semantics

Action systems are a construct for reasoning about concurrent, reactive systems, in which concurrent behaviour is described by interleaving atomic actions. Sere and Troubitsyna have proposed an extension to action systems in which actions may be expressed and composed using discrete probabilistic choice as well as demonic nondeterministic choice. In this paper we develop a trace-based semantics for probabilistic action systems. This semantics provides a simple theoretical base on which practical refinement rules for probabilistic action systems may be justified.

Measurement and state preparation via ion trap quantum computing

We investigate in detail the effects of a QND vibrational number measurement made on single ions in a recently proposed measurement scheme for the vibrational state of a register of ions in a linear rf trap [C. D'HELON and G. J. MILBURN, Phys Rev. A 54, 5141 (1996)]. The performance of a measurement shows some interesting patterns which are closely related to searching.

Expokit: A software package for computing matrix exponentials

Expokit provides a set of routines aimed at computing matrix exponentials. More precisely, it computes either a small matrix exponential in full, the action of a large sparse matrix exponential on an operand vector, or the solution of a system of linear ODEs with constant inhomogeneity. The backbone of the sparse routines consists of matrix-free Krylov subspace projection methods (Arnoldi and Lanczos processes), and that is why the toolkit is capable of coping with sparse matrices of large dimension. The software handles real and complex matrices and provides specific routines for symmetric and Hermitian matrices. The computation of matrix exponentials is a numerical issue of critical importance in the area of Markov chains and furthermore, the computed solution is subject to probabilistic constraints. In addition to addressing general matrix exponentials, a distinct attention is assigned to the computation of transient states of Markov chains.

Utilizing encoding in scalable linear optics quantum computing

We present a scheme which offers a significant reduction in the resources required to implement linear optics quantum computing. The scheme is a variation of the proposal of Knill, Laflamme and Milburn, and makes use of an incremental approach to the error encoding to boost probability of success.

Unitary R-matrices for topological quantum computing

The main problem with current approaches to quantum computing is the difficulty of establishing and maintaining entanglement. A Topological Quantum Computer (TQC) aims to overcome this by using different physical processes that are topological in nature and which are less susceptible to disturbance by the environment. In a (2+1)-dimensional system, pseudoparticles called anyons have statistics that fall somewhere between bosons and fermions. The exchange of two anyons, an effect called braiding from knot theory, can occur in two different ways. The quantum states corresponding to the two elementary braids constitute a two-state system allowing the definition of a computational basis. Quantum gates can be built up from patterns of braids and for quantum computing it is essential that the operator describing the braiding-the R-matrix-be described by a unitary operator. The physics of anyonic systems is governed by quantum groups, in particular the quasi-triangular Hopf algebras obtained from finite groups by the application of the Drinfeld quantum double construction. Their representation theory has been described in detail by Gould and Tsohantjis, and in this review article we relate the work of Gould to TQC schemes, particularly that of Kauffman.

Impairments of movement kinematics in patients with Huntington's disease: A comparison with and without a concurrent task

This study aimed to quantify the efficiency and smoothness of voluntary movement in Huntington's disease (HD) by the use of a graphics tablet that permits analysis of movement profiles. In particular, we aimed to ascertain whether a concurrent task (digit span) would affect the kinematics of goal-directed movements. Twelve patients with HD and their matched controls performed 12 vertical zig-zag movements, with both left and right hands (with and without the concurrent task), to large or small circular targets over long or short extents. The concurrent task was associated with shorter movement times and reduced right-hand superiority. Patients with HD were overall slower, especially with long strokes, and had similar peak velocities for both small and large targets, so that controls could better accommodate differences in target size. Patients with HD spent more time decelerating, especially with small targets, whereas controls allocated more nearly equal proportions of time to the acceleration and deceleration phases of movement, especially with large targets. Short strokes were generally less force inefficient than were long strokes, especially so for either hand in either group in the absence of the concurrent task, and for the right hand in its presence. With the concurrent task, however, the left hand's behavior changed differentially for the two groups; for patients with HD, it became more force efficient with short strokes and even less efficient with long strokes, whereas for controls, it became more efficient with long strokes. Controls may be able to divert attention away from the inferior left hand, increasing its automaticity, whereas patients with HD, because of disease, may be forced to engage even further online visual control under the demands of a concurrent task. Patients with HD may perhaps become increasingly reliant on terminal visual guidance, which indicates an impairment in constructing and refining an internal representation of the movement necessary for its. effective execution. Basal ganglia dysfunction may impair the ability to use internally generated cues to guide movement.

Cervical mobilisation: concurrent effects on pain, sympathetic nervous system activity and motor activity

Recent findings that spinal manual therapy (SMT) produces concurrent hypoalgesic and sympathoexcitatory effects have led to the proposal that SMT may exert its initial effects by activating descending inhibitory pathways from the dorsal periaqueductal gray area of the midbrain (dPAG). In addition to hypoalgesic and sympathoexcitatory effects, stimulation of the dPAG in animals has been shown to hal e a facilitatory effect on motor activity. This study sought to further investigate the proposal regarding SMT and the FAG by including a test of motor function in addition to the variables previously investigated, Using a condition randomised, placebo-controlled, double blind, repeated measures design, 30 subjects with mid to lon er cervical spine pain of insidious onset participated in the study. The results indicated that the cervical mobilisation technique produced a hypoalgesic effect as revealed by increased pressure pain thresholds on the side of treatment (P = 0.0001) and decreased resting visual analogue scale scores (P = 0.049). The treatment technique also produced a sympathoexcitatory effect with an increase in skin conductance (P < 0.002) and a decrease in skin temperature (P = < 0.02). There was a decrease in superficial neck flexor muscle activity (P < 0.0002) at the lower levels of a staged cranio-cervical flexion test. This could imply facilitation of the deep neck flexor muscles with a decreased need for co-activation of the superficial neck flexors, The combination of all findings,would support the proposal that SMT may, at least initially, exert part of its influence via activation of the PAG, (C) 2000 Harcourt Publishers Ltd.

Development, reliability, and concurrent validity of the modified inventory of potential reconstructive needs

Documentation of burn sequelae can be a difficult and time-consuming task. To date a reliable and systematic format for recording postburn trauma is lacking. The purpose of this research was two-fold: first, to develop a Modified Inventory of Potential Reconstructive Needs from the original Inventory of Potential Reconstructive Needs to allow methodical documentation of functional and cosmetic burn sequelae in all body surface areas of children with burns and, second, to establish interrater reliability and concurrent validity of the instrument, thus allowing its clinical application. Two raters scored the Modified Inventory of Potential Reconstructive Needs on 41 children with a range of burns types and severity. Excellent interrater reliability was demonstrated for both total (intraclass correlation coefficient = 0.996) and subsection inventory scores. Concurrent validity was also established with total scores showing strong positive correlations (0.73-0.76) with three indicators of burn severity. These findings provide initial support for the tool's clinical applicability, particularly in relation to rehabilitative planning and documentation.