In equational theorem proving, convergent term rewriting systems play a crucial role. In order to compute convergent term rewriting systems, the standard completion procedure (KB) was proposed by Knuth and Bendix and has been improved in various ways. The multi-completion system MKB developed by Kurihara and Kondo accepts as input a set of reduction orders in addition to equations and efficiently simulates parallel processes each of which executes the KB procedure with one of the given orderings. Wehrman and Stump also developed a new variant of completion procedure, constraint-based completion, in which reduction orders need not be given by using automated modern termination checkers. As a result, the constraint-based procedures simulate the execution of parallel KB processes in a sequential way, but naive search algorithms sometimes cause serious inefficiency when the number of the potential reduction orders is large. In this paper, we present a new procedure, called a constraint-based multi-completion procedure MKBcs, by augmenting the constraint-based completion with the framework of the multi-completion for suppressing the combinatorial explosion by sharing inferences among the processes. The existing constraint-based system SLOTHROP, which basically employs the best-first search, is more efficient when its built-in heuristics for process selection are appropriate, but when they are not, our system is more efficient. Therefore, both systems have their role to play.

A self-stabilizing protocol is a protocol that achieves its intended behavior regardless of the initial configuration (i.e., global state). Thus, a self-stabilizing protocol is adaptive to any number and any type of topology changes of networks: after the last topology change occurs, the protocol starts to converge to its intended behavior. This advantage makes self-stabilizing protocols extremely attractive for designing highly dependable distributed systems on dynamic networks. While conventional self-stabilizing protocols require that the networks remain static during convergence to the intended behaviors, some recent works undertook the challenge of realizing self-stabilization in dynamic networks with frequent topology changes. This paper introduces some of the challenges as a new direction of research in self-stabilization.

Cluster systems are prevalent infrastructures for offering e-services because of their cost-effectiveness. The objective of our research is to enhance their cost-effectiveness by reducing the minimum number of nodes to meet a given target performance. To achieve the objective, we propose a load balancing algorithm, the Nearest Underloaded algorithm (N algorithm). The N algorithm aims at quick solution of load imbalance caused by request departures while also preventing herd effect. The performance index in our evaluation is the xth percentile capacity which we define based on throughputs and the xth percentile response times. We measured the capacity of 8- to 16-node cluster systems under the N algorithm and existing Least-Loaded (LL) algorithms, which dispatch or transfer requests to the least-loaded node. We found that the N algorithm could achieve larger capacity or could achieve the target capacity with fewer nodes than LL algorithms could.

Mobile IPv6 and Network Mobility (NEMO) have been standardized as IP extensions. While these technologies are planned to be adopted by several communities, such as the vehicle, aviation, and cellular industries, Mobile IPv6 has serious deployment issues such as scalability, protocol resilience, and redundancy. In these technologies, a special router called a home agent is introduced to support the movement of mobile nodes. This home agent introduces overlapping, inefficient routes, and becomes a single point of failure and a performance bottleneck. In this paper, a new concept for scalable and dependable mobility management scheme is proposed. Multiple home agents serve the same set of mobile nodes. The Home Agent Reliability protocol and Home Agent migration are introduced to achieve this concept. We also propose an overlay network named a Global Mobile eXchange (GMX) that efficiently handles data traffic from and to mobile nodes, and operates home agents as would an Internet eXchange Point (IXP).

We have proposed a noise reduction method based on a noise reconstruction system (NRS). The NRS uses a linear prediction error filter (LPEF) and a noise reconstruction filter (NRF) which estimates background noise by system identification. In case a fixed step size for updating tap coefficients of the NRF is used, it is difficult to reduce background noise while maintaining the high quality of enhanced speech. In order to solve the problem, a variable step size is proposed. It makes use of cross-correlation between an input signal and an enhanced speech signal. In a speech section, a variable step size becomes small so as not to estimate speech, on the other hand, large to track the background noise in a non-speech section.

To address the low performance for channel scanning in the DVB-T system, we propose an enhanced front-end algorithm in this paper. The proposed algorithm consists of Auto Scan and Normal Scan, which is a part of the tuning algorithm for front-end (tuner) drivers in the DVB-T receiver. The key idea is that the frequency offset is saved when performing Auto Scan in order to reduce the channel change time for Normal Scan. In addition, the results of a performance evaluation demonstrate that our enhanced front-end algorithm improves the performance of channel scanning significantly, as compared to the generic front-end algorithm.

We propose a velocity-based bicasting handover scheme for the efficient utilization of backhaul network resources in fourth-generation mobile systems. The original bicasting handover scheme adopts the mechanism of holding the data of a mobile station (MS) in all potential target base stations in advance, before the actual handover execution of the MS. The scheme minimizes the packet transmission delay caused by handover and achieves the goal of seamless connectivity, however, it results in an aggressive consumption of the backhaul network resources. Moreover, as the scheme gets widely adopted for high data rate real-time services and the demand for these services grows, the amount of the resources consumed due to the bicasting will increase tremendously. In this paper, we present a new bicasting handover scheme that reduces the data bicasting time, thereby improving the backhaul network resource utilization. Our scheme exploits the velocity parameter of MS and introduces a novel concept of bicasting threshold determined for the specific mobile speed groups. Simulations prove the efficiency of our scheme over the original one in overcoming the aggressive resource consumption at the backhaul network.

In market-basket analysis, weighted association rule (WAR) discovery can mine the rules that include more beneficial information by reflecting item importance for special products. In the point-of-sale database, each transaction is composed of items with similar properties, and item weights are pre-defined and fixed by a factor such as the profit. However, when items are divided into more than one group and the item importance must be measured independently for each group, traditional weighted association rule discovery cannot be used. To solve this problem, we propose a new weighted association rule mining methodology. The items should be first divided into subgroups according to their properties, and the item importance, i.e. item weight, is defined or calculated only with the items included in the subgroup. Then, transaction weight is measured by appropriately summing the item weights from each subgroup, and the weighted support is computed as the fraction of the transaction weights that contains the candidate items relative to the weight of all transactions. As an example, our proposed methodology is applied to assess the vulnerability to threats of computer systems that provide networked services. Our algorithm provides both quantitative risk-level values and qualitative risk rules for the security assessment of networked computer systems using WAR discovery. Also, it can be widely used for new applications with many data sets in which the data items are distinctly separated.

In this paper, we investigate the transitional dynamics and quasi-periodic solution appearing after the Saddle-Node (SN) bifurcation of a periodic solution in an inductor-coupled asymmetrical van der Pol oscillators with hard-type nonlinearity. In particular, we elucidate, by investigating global bifurcation of unstable manifold (UM) of saddles, that transitional dynamics and quasi-periodic solution after the SN bifurcation appear based on different structure of UM.

In the electromagnetic theory, the vacuum impedance Z0 is a universal constant, which is as important as the velocity of light c0 in vacuum. Unfortunately, however, its significance is not appreciated so well and sometimes the presence itself is ignored. It is partly because in the Gaussian system of units, which has widely been used for long time, Z0 is a dimensionless constant and of unit magnitude. In this paper, we clarify that Z0 is a fundamental parameter in electromagnetism and plays major roles in the following scenes: reorganizing the structure of the electromagnetic formula in reference to the relativity; renormalizing the quantities toward natural unit systems starting from the SI unit system; and defining the magnitudes of electromagnetic units.

In this paper, we propose designing method for separable-denominator two-dimensional Infinite Impulse Response (IIR) filters (separable 2D IIR filters) by Successive Projection (SP) methods using the stability criteria based on the system matrix. It is generally known that separable 2D IIR filters are stable if and only if each of the denominators is stable. Therefore, the stability criteria of 1D IIR filters can be used for separable 2D IIR filters. The stability criteria based on the system matrix are a necessary and sufficient condition to guarantee stability in 1D IIR filters. Therefore, separable 2D IIR filters obtained by the proposed design method have a smaller error ripple than those obtained by the conventional design method using the stability criterion of Rouche's theorem.

Traffic Engineering (TE) is important for improving QoS in forwarding paths by efficient use of network resources. In fact, MPLS allows several detour paths to be (pre-)established for some source-destination pair as well as its primary path of minimum hops. Thus, we focus on a two-phase path management scheme using these two kinds of paths. In the first phase, each primary path is allocated to a flow on a specific source-destination pair if the path is not congested, i.e., if its utilization is less than some predetermined threshold; otherwise, as the second phase, one of the detour paths is allocated randomly if the path is available. Therefore, in this paper, we analytically evaluate this path management scheme by extending the M/M/c/c queueing system, and through some numerical results we investigate the impact of a threshold on the flow-blocking probability. Through some numerical results, we discuss the adequacy of the path management scheme for MPLS-TE.

This letter presents a novel approach for traffic light detection in a video frame captured by an in-vehicle camera. The algorithm consists of rotated principal component analysis (RPCA), modified amplitude thresholding with respect to the histograms of the PC planes and final filtering with a neural network. The proposed algorithm achieves an average detection rate of 96% and is very robust to variations in the image quality.

The electrostatic force required for the driving of liquid droplet injected in a microchannel was studied to obtain the guiding principle to reduce the driving voltage of waveguide optical switch based on the movement of droplet. We analytically calculated the relation between the threshold voltage and velocity of droplet and the surface roughness of microchannel, and clarified some unconfirmed parameters by comparing experimental results and aeromechanical analysis. The driving of droplet in a microchannel was best analyzed using the Hagen-Poiseuille flow theory, taking into account the movement of both ends of the droplet. When the droplet is driven by some external force, a threshold of the external force occurs in the starting of movement, and hysteresis occurs in the contact angle of the droplet to the side wall of the microchannel. The hysteresis of contact angle is caused by the roughness of side wall. In our experiment, the threshold voltage ranged from 200 to 350 V and the switching time from 34 to 36 ms. The velocity of droplet was evaluated to be 0.3-0.4 mm/s from these experimental results. On the other hand, the measured angle distribution of side wall roughness ranged from 30 to 110 degrees, and the threshold voltage was evaluated to be 100-320 V, showing a good agreement with experimental results. The reduction of threshold voltage can be realized by smoothing the side wall roughness of microchannel. The switching time of 10 ms, which is required for the optical stream switch, can be obtained by shortening the horizontal spot size down to 1.5 µm.

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.

We propose Adaptive Resource Allocation for the Partial Block MC-CDMA (ARA-PB/MC-CDMA) system. The ARA-PB/MC-CDMA system aims to improve total throughput performance and frequency efficiency across various channel conditions. It adaptively changes the number of blocks to improve the throughput performance and frequency efficiency according to the Signal to Interference Ratio (SIR). Therefore, the proposed system supports various Quality of Service (QoS) requirements for various SIR values.

A detector for space-time block coding is proposed to combat time-selective fading. To suppress both noise and interference, a minimum mean square error (MMSE) based detector is introduced for space-time block coding. It is shown by simulations that the proposed detector outperforms the conventional detectors when the channel is time-selective fading.

In this paper, we propose a computationally efficient method to solve the large dimension Adaptive Subcarrier Assignment and Bit Allocation (ASABA) problem of multiuser orthogonal frequency division multiplexing system. Our algorithm consists of three Ordinal Optimization (OO) stages to find a good enough solution to the considered problem. First of all, we reformulate the considered problem to separate it into subcarrier assignment and bit allocation problem such that the objective function of a feasible subcarrier assignment pattern is the corresponding optimal bit allocation for minimizing the total consumed power. Then in the first stage, we develop an approximate objective function to evaluate the performance of a subcarrier assignment pattern and use a genetic algorithm to search through the huge solution space and select s best subcarrier assignment patterns based on the approximate objective values. In the second stage, we employ an off-line trained artificial neural network to estimate the objective values of the s subcarrier assignment patterns obtained in stage 1 and select the l best patterns. In the third stage, we use the exact objective function to evaluate the l subcarrier assignment patterns obtained in stage 2, and the best one associated with the corresponding optimal bit allocation is the good enough solution that we seek. We apply our algorithm to numerous cases of large-dimension ASABA problems and compare the results with those obtained by four existing algorithms. The test results show that our algorithm is the best in both aspects of solution quality and computational efficiency.

In human-machine systems, a user gets abstracted information of a machine via an interface and operates it referring to a manual. If a manual has an erroneous description leading to automation surprises, the user may be lost in his/her operations so that he/she may make a serious human error. In this paper, we propose an algorithm for generating a manual by which automation surprises never occur. We model the machine and the interface as a discrete event system and a mapping from machine's state to a display of the interface, respectively. First, we represent a manual as a finite language and model behavior of the system operated by the user with the manual as a tree called an operational tree. Next, we characterize three automation surprises using the tree. Finally, we propose an algorithm for generating an operational tree by which the machine reaches a target state.

For developing design environment of various Dynamically Reconfigurable Processor Arrays (DRPAs), the Graph with Configuration Information (GCI) is proposed to represent configurable resource in the target dynamically reconfigurable architecture. The functional unit, constant unit, register, and routing resource can be represented in the graph as well as the configuration information. The restriction in the hardware is also added in the graph by limiting the possible configuration at a node controlled by the other node. A prototype compiler called Black-Diamond with GCI is now available for three different DRPAs. It translates data-flow graph from C-like front-end description, applies placement and routing by using the GCI, and generates configuration data for each element of the DRPA. Evaluation results of simple applications show that Black-Diamond can generate reasonable designs for all three different architectures. Other target architectures can be easily treated by representing many aspects of architectural property into a GCI.