Proofs written in algebraic specification languages are called proof scores. The proof score approach to design verification is attractive because it provides a flexible way to prove that designs for systems satisfy properties. Thus far, however, the approach has focused on safety properties. In this paper, we describe a way to verify that designs for systems satisfy liveness properties with the approach. A mutual exclusion protocol using a queue is used as an example. We describe the design verification and explain how it is verified that the protocol satisfies the lockout freedom property.

The least-squares linear filtering and fixed-point smoothing problems of uncertainly observed signals are considered when the signal and the observation additive noise are correlated at any sampling time. Recursive algorithms, based on an innovation approach, are proposed without requiring the knowledge of the state-space model generating the signal, but only the autocovariance and crosscovariance functions of the signal and the observation white noise, as well as the probability that the signal exists in the observations.

We describe a way to write state machines inductively. The proposed method makes it possible to use the standard techniques for proving theorems on inductive types to verify that state machines satisfy invariant properties. A mutual exclusion protocol using a queue is used to exemplify the proposed method.

We present MobileOBJ, a formal framework for specifying and verifying mobile systems. Based on hidden algebra, the components of a mobile system are specified as behavioral objects or Observational Transition Systems, a kind of transition system, enriched with special action and observation operators related to the distinct characteristics of mobile computing systems. The whole system comes up as the concurrent composition of these components. The implementation of the abstract model is achieved using CafeOBJ, an executable, industrial strength algebraic specification language. The visualization of the specification can be done using CafeOBJ graphical notation. In addition, invariant and behavioral properties of mobile systems can be proved through theorem proving techniques, such as structural induction and coinduction that are fully supported by the CafeOBJ system. The application of the proposed framework is presented through the modeling of a mobile computing environment and the services that need to be supported by the former.

This letter analyzes the performance of statistical cooperative diversity based on space-time block codes (STBC) (Statistical STBC cooperative diversity) considering the effects of quantization and observation noise. Binary quantization is used. The bit error rate (BER) and average mutual information of the statistical STBC cooperative diversity with Alamouti's STBC and two active nodes are derived in the presence of general observation noise. It is shown that the performance of the statistical STBC cooperative diversity depends on the effects of observation noise and the number of cooperating nodes largely. It is also shown how much the communication between sensor nodes or feedback from the fusion center improves the performance of STBC cooperative diversity.

This paper discusses the least-squares linear filtering and smoothing (fixed-point and fixed-interval) problems of discrete-time signals from observations, perturbed by additive white noise, which can be randomly delayed by one sampling time. It is assumed that the Bernoulli random variables characterizing delay measurements are correlated in consecutive time instants. The marginal distribution of each of these variables, specified by the probability of a delay in the measurement, as well as their correlation function, are known. Using an innovation approach, the filtering, fixed-point and fixed-interval smoothing recursive algorithms are obtained without requiring the state-space model generating the signal; they use only the covariance functions of the signal and the noise, the delay probabilities and the correlation function of the Bernoulli variables. The algorithms are applied to a particular transmission model with stand-by sensors for the immediate replacement of a failed unit.

We have proposed in [5] a practical blind channel identification algorithm for the white observation noise. In this paper, we examine the effectiveness of the algorithm given in [5] for the colored observation noise. The proposed algorithm utilizes Gram-Schmidt orthogonalization procedure and estimates (1) the channel order, (2) the noise variance and then (3) the channel impulse response with less computational complexity compared to the conventional algorithms using eigenvalue decomposition. It can be shown through numerical examples that the algorithm proposed in [5] is quite effective in the colored noise case.

The actual sound environment system exhibits various types of linear and non-linear characteristics, and it often contains an unknown structure. Furthermore, the observations in the sound environment are often in the level-quantized form. In this paper, a method for estimating the specific signal for stochastic systems with unknown structure and the quantized observation is proposed by introducing a system model of the conditional probability type. The effectiveness of the proposed theoretical method is confirmed by applying it to the actual problem of psychological evaluation for the sound environment.

This paper discusses the least-squares linear filtering and fixed-lag smoothing problems of discrete-time signals from uncertain observations when the random interruptions in the observation process are modelled by a sequence of not necessarily independent Bernoulli variables. It is assumed that the observations are perturbed by white noise and the autocovariance function of the signal is factorizable. Using an innovation approach we obtain the filtering and fixed-lag smoothing recursive algorithms, which do not require the knowledge of the state-space model generating the signal. Besides the observed values, they use only the matrix functions defining the factorizable autocovariance function of the signal, the noise autocovariance function, the marginal probabilities and the (2,2)-element of the conditional probability matrices of the Bernoulli variables. The algorithms are applied to estimate a scalar signal which may be transmitted through one of two channels.

The problem of signal restoration in the presence of observation space noise has been tackled extensively. However, restoration of degraded signals in the presence of signal space noise leads to considerable complexity because it becomes difficult to distinguish between the original signal and the noise. In this paper, a partial projection filter has been devised for the restoration of signals degraded by both the signal space and the observation space noises. A closed form of the proposed filter has been derived and its performance has been verified experimentally.

This paper treats the least-squares linear filtering and smoothing problems of discrete-time signals from uncertain observations when the random interruptions in the observation process are modelled by a sequence of independent Bernoulli random variables. Using an innovation approach we obtain the filtering algorithm and a general expression for the smoother which leads to fixed-point, fixed-interval and fixed-lag smoothing recursive algorithms. The proposed algorithms do not require the knowledge of the state-space model generating the signal, but only the covariance information of the signal and the observation noise, as well as the probability that the signal exists in the observed values.

The partial projection filter gives optimal signal restoration in the presence of both the signal space and the observation space noises. In this paper, the filter has been characterized from the point of view of its signal restoration and noise suppression capabilities. The filter is shown to suppress the noise component in the restored signal while retaining the signal component, thus maximizing the signal-to-noise ratio. Further, a digital implementation of the filter is presented in matrix form in contrast to its original operator based derivation, for practical applications.

This paper presents recursive algorithms for the least mean-squared error linear filtering and fixed-interval smoothing estimators, from uncertain observations for the case of white and white plus coloured observation noises. The estimators are obtained by an innovation approach and do not use the state-space model, but only covariance information about the signal and the observation noises, as well as the probability that the signal exists in the observed values. Therefore the algorithms are applicable not only to signal processes that can be estimated by the conventional formulation using the state-space model but also to those for which a realization of the state-space model is not available. It is assumed that both the signal and the coloured noise autocovariance functions are expressed in a semi-degenerate kernel form. Since the semi-degenerate kernel is suitable for expressing autocovariance functions of non-stationary or stationary signal processes, the proposed estimators provide estimates of general signal processes.

This paper considers the least-squares linear estimation problem of signals from randomly delayed observations when the additive white noise is correlated with the signal. The delay values are treated as unknown variables, modelled by a binary white noise with values zero or one; these values indicate that the measurements arrive in time or they are delayed by one sampling time. A recursive one-stage prediction and filtering algorithm is obtained by an innovation approach and do not use the state-space model of the signal. It is assumed that both, the autocovariance functions of the signal and the crosscovariance function between the signal and the observation noise are expressed in a semi-degenerate kernel form; using this information and the delay probabilities, the estimators are recursively obtained.

AFM/STM observations were performed on sub nm thick C-Au-S film by co-operation process of plasma CVD and sputtering with using CH4, SF6 and Ar mixture gas and Au plate discharge electrode. From the refractive index values, the conductive granular molecules with a size of 0.4-0.6 nm were expected to exist in the film. For the film at thickness similar to the molecular size, Ra (arithmetic mean departures of roughness profile from the mean line) values were measured to be 0.712/6.10 nm by AFM/STM measurement, respectively. The one order large STM Ra value compared to the AFM Ra value suggests that the film contains conductive granular molecules.

Least-squares second-order polynomial filter and fixed-point smoother are derived in systems with uncertain observations, when the variables describing the uncertainty are non-independent. The proposed estimators do not require the knowledge of the state-space model of the signal. The available information is only the moments, up to the fourth one, of the involved processes, the probability that the signal exists in the observations and the (2,2) element of the conditional probability matrices of the sequence describing the uncertainty.

The locally optimum rank detector achieves a simpler detector structure when reference observations, in addition to regular observations, are available. Without reference observations, we have to use the sign statistics of regular observations, and using the sign statistics results in a complex detector structure. Instead, more computations are necessary to deal with additional reference observations.

In order to assess the possible impacts of meteors with spacecraft, which is among major hazard in the space environment, it is essential to establish an accurate statistics of their mass and velocity. We developed a radar-optical combined system for detecting faint meteors consisting of a powerful VHF Doppler radar and an ICCD video camera. The Doppler pulse compression scheme is used to enhance the S/N ratio of the radar echoes with very large Doppler shifts, as well as to determine their range with a resolution of 200 m. A very high sensitivity of more than 14 magnitude and 9 magnitude for radar and optical sensors, respectively, has been obtained. Instantaneous direction of meteor body observed by the radar is determined with the interferometry technique. We examined the optimum way of the receiving antenna arrangements, and also of the signal processing. Its absolute accuracy was confirmed by the optical observations with background stars as a reference. By combining the impinging velocity of meteor bodies derived by the radar with the absolute visual magnitude determined by the video camera simultaneously, the mass of each meteor body was estimated. The developed observation system will be used to create a valuable data base of the mass and velocity information of faint meteors, on which very little is known so far. The data base is expected to play a vital role in our understanding of the space environment needed for designing large space structures.

In this paper, we study nonblocking supervisory control of discrete event systems under partial observation. We introduce a weak normality condition defined in terms of a modified natural projection map. The weak normality condition is weaker than the original one and stronger than the observability condition. Moreover, it is preserved under union. Given a marked language specification, we present a procedure for computing the supremal sublanguage which satisfies Lm(G)-closure, controllability, and weak normality. There exists a nonblocking supervisor for this supremal sublanguage. Such a supervisor is more permissive than the one which achieves the supremal Lm(G)-closed, controllable, and normal sublanguage.

A speaker adaptation technique that maximizes the observation probability of an input speech is proposed. It is applied to semi-continuous hidden Markov model (SCHMM) speech recognizers. The proposed algorithm adapts the mean µ and the covariance Σ iteratively by the gradient search technique so that the features of the adaptation speech data could achieve maximum observation probabilities. The mixture coefficients and the state transition probabilities are adapted by the model interpolation scheme. The main advantage of this scheme is that the means and the variances, which are common to all states in SCHMM, are adapted independently from the other parameters of SCHMM. It allows fast and precise adaptation especially when there is a large acoustic mismatch between the reference model and a new speaker. Also, it is possible that this scheme could be adopted to other areas which use codebook. The proposed adaptation algorithm was evaluated by a male speaker-dependent, a female speaker-dependent, and a speaker-independent recognizers. The experimental results on the isolated word recognition showed that the proposed adaptation algorithm achieved 46.03% average enhancement in the male speaker-dependent recognizer, 52.18% in the female speaker-dependent recognizer, and 9.84% in the speaker-independent recognizer.