This paper presents the formal analysis of the feature negotiation and connection management procedures of the Datagram Congestion Control Protocol (DCCP). Using state space analysis we discover an error in the DCCP specification, that result in both ends of the connection having different agreed feature values. The error occurs when the client ignores an unexpected Response packet in the OPEN state that carries a valid Confirm option. This provides an evidence that the connection management procedure and feature negotiation procedures interact. We also propose solutions to rectify the problem.

This letter introduces an Energy-Aware LED Light System (EA-LLS) that provides adequate illumination to users according to the analysis of the sun's position, the user's movement, and various environmental factors, without sun illumination detection sensors. This letter presents research using algorithms and scenarios. We propose an EA-LLS that offers not only On/Off and dimming control, but dimming control through daylight, space, and user behavior analysis.

Face verification is the task of determining whether two given face images represent the same person or not. It is a very challenging task, as the face images, captured in the uncontrolled environments, may have large variations in illumination, expression, pose, background, etc. The crucial problem is how to compute the similarity of two face images. Metric learning has provided a viable solution to this problem. Until now, many metric learning algorithms have been proposed, but they are usually limited to learning a linear transformation. In this paper, we propose a nonlinear metric learning method, which learns an explicit mapping from the original space to an optimal subspace using deep Independent Subspace Analysis (ISA) network. Compared to the linear or kernel based metric learning methods, the proposed deep ISA network is a deep and local learning architecture, and therefore exhibits more powerful ability to learn the nature of highly variable dataset. We evaluate our method on the Labeled Faces in the Wild dataset, and results show superior performance over some state-of-the-art methods.

An algorithm for blind signal separation (BSS) of convolutive mixtures is presented. In this algorithm, the BSS problem is treated as multidimensional independent component analysis (ICA) by introducing an extended signal vector which is composed of current and previous samples of signals. It is empirically known that a number of conventional ICA algorithms solve the multidimensional ICA problem up to permutation and scaling of signals. In this paper, we give theoretical justification for using any conventional ICA algorithm. Then, we discuss the remaining problems, i.e., permutation and scaling of signals. To solve the permutation problem, we propose a simple algorithm which classifies the signals obtained by a conventional ICA algorithm into mutually independent subsets by utilizing temporal structure of the signals. For the scaling problem, we prove that the method proposed by Koldovský and Tichavský is theoretically proper in respect of estimating filtered versions of source signals which are observed at sensors.

A robust microphone array for speech enhancement and noise suppression is studied in this paper. To overcome target signal cancellation problem of conventional beamformer caused by array imperfections or reverberation effects of acoustic enclosure, the proposed microphone array adopts an arbitrary model of channel transfer function (TF) relating microphone and speech source. Since the estimation of channel TF itself is often intractable, herein, transfer function ratio (TFR) is estimated instead and used to form a suboptimal beamformer. A robust TFR estimation method is proposed based on signal subspace analysis technique against stationary or slowly varying noise. Experiments using simulated signal and actual signal recorded in a real room illustrate that the proposed method has high performance in adverse environment.

The proposed DOA (Direction Of Arrival) estimation method by integrating the frequency array data generated from microphone pairs in an equilateral-triangular microphone array is extended here. The method uses four microphones located at the apices of regular tetrahedron to enable to estimate the elevation angle from the array plane as well. Furthermore, we introduce an idea for separate estimation of azimuth and elevation to reduce the computational loads.

In this paper, we propose a DOA (Direction Of Arrival) estimation method of speech signal using three microphones. The angular resolution of the method is almost uniform with respect to DOA. Our previous DOA estimation method using the frequency-domain array data for a pair of microphones achieves high precision estimation. However, its resolution degrades as the propagating direction being apart from the array broadside. In the method presented here, we utilize three microphones located at vertices of equilateral triangle and integrate the frequency-domain array data for three pairs of microphones. For the estimation scheme, the subspace analysis for the integrated frequency array data is proposed. Through both computer simulations and experiments in a real acoustical environment, we show the efficiency of the proposed method.

In speech enhancement with adaptive microphone array, the voice activity detection (VAD) is indispensable for the adaptation control. Even though many VAD methods have been proposed as a pre-processor for speech recognition and compression, they can hardly discriminate nonstationary interferences which frequently exist in real environment. In this research, we propose a novel VAD method with array signal processing in the wavelet domain. In that domain we can integrate the temporal, spectral and spatial information to achieve robust voice activity discriminability for a nonstationary interference arriving from close direction of speech. The signals acquired by microphone array are at first decomposed into appropriate subbands using wavelet packet to extract its temporal and spectral features. Then directionality check and direction estimation on each subbands are executed to do VAD with respect to the spatial information. Computer simulation results for sound data demonstrate that the proposed method keeps its discriminability even for the interference arriving from close direction of speech.

In the image recognition problem, it is very important how we represent the image. Considering this, we propose a new representational method of images based on the stability in scale-space. In our method, the image is segmented and represented as a hierarchical region graph in scale-space. The object is represented as feature graph, which is subgraph of region graph. In detail, the region graph is defined on the image with the relation of each segment hierarchically. And the feature graph is determined based on the "life-time" of the graph of the object in scale-space. This "life-time" means how long feature graph lives when the scale parameter is increased. We apply our method to the face detection problem, which is foundmental and difficult problem in face recognition. We determine the feature graph of the frontal human face statistical point of view. We also build the face detection system using this feature graph to show how our method works efficiently.

Generating state spaces is one of important and general methods in the analysis of Petri nets. There are two reasons why state spaces of Petri nets become so large. One is concurrent occurring of transitions, and the other is periodic occurring of firing sequences. This paper focuses on the second problem, and proposes a new algorithm for exploring state spaces of finite capacity Petri nets with large capacities. In the proposed algorithm, the state space is represented in the form of a tree such that a set of markings generated by periodic occurrences of firing sequences is associated with each node, and it is much smaller than the reachability graph.

This paper proposed a practical method of program validation for state-based reactive concurrent systems. The proposed method is of particular relevance to plant control systems. Plant control systems can be represented by extended state transition systems (e.g., communicating asynchronous transition systems). Our validation method is based on state space analysis. Since naive state space analysis causes the state explosion problem, techniques to ease state explosion are necessary. One of the most promising techniques is the partial order method. However, these techniques usually require some structural assumptions and they are not always effective for actual control systems. Therefore, we claim integration and harmonization of verification (i.e., state space analysis based on the partial order method) and simulation (i.e., conventional validation technique). In the proposed method, verification is modeled as exhaustive simulation over the state space, and two types of simulation management techniques are introduced. One is logical selection (pruning) based on the partial order method. The other is heuristic selection based on priority (a priori precedence) specified by the user. In order to harmonize verification (logical selection) and conventional simulation (heuristic selection), we propose a new logical selection mechanism (the default priority method). The default priority method which prunes redundant state generation based on default priority is in harmony with heuristic selection based on the user's priority. We have implemented a practical validation tool, Simulation And Verification Environment for Reactive Concurrent Systems (SAVE/RCS), and applied it to chemical plant control systems.