A computational model for security verification of cryptographic protocols is proposed. Until most recently, security verification of cryptographic protocols was left to the protocol designers' experience and heuristics. Though some formal verification methods have been proposed for this purpose, they are still insufficient for the verification of practical real-time cryptographic protocols. In this paper we propose a new formalism based on a term rewriting system approach that we have developed. In this model, what and when the saboteur can obtain is expressed by a first-order term of a special form, and time-related concepts such as the passage of time and the causality relation are specified by conditional term rewriting systems. By using our model, a cryptographic protocol which was shown to be secure by the BAN-logic is shown to be insecure.

Segmenting the images obtained from magnetic resonance imaging (MRI) is an important process for visualization of the human soft tissues. For the application of MR, we often have to introduce a reasonable segmentation technique. Neural networks may provide us with superior solutions for the pattern classification of medical images than the conventional methods. For image segmentation with the aid of neural networks of a reasonable size, it is important to select the most effective combination of secondary indices to be used for the classification. In this paper, we introduce a vector quantized class entropy (VQCCE) criterion to evaluate which indices are effective for pattern classification, without testing on the actual classifiers. We have exploited a newly developed neural tree classifier for accomplishing the segmentation task. This network effectively partitions the feature space into subregions and each final subregion is assigned a class label according to the data routed to it. As the tree grows on, the number of training data for each node decreases, which results in less weight update epochs and decreases the time consumption. The partitioning of the feature space at each node is done by a simple neural network; the appropriateness of which is measured by newly proposed estimation criterion, i. e. the measure for assessment of neuron (MAN). It facilitates the obtaining of a neuron with maximum correlation between a unit's value and the residual error at a given output. The application of this criterion guarantees adopting the best-fit neuron to split the feature space. The proposed neural classifier has achieved 95% correct classification rate on average for the white/gray matter segmentation problem. The performance of the proposed method is compared to that of a multilayered perceptron (MLP), the latter being widely exploited network in the field of image processing and pattern recognition. The experiments show the superiority of the introduced method in terms of less iterations and weight up dates necessary to train the neural network, i. e. lower computational complexity; as well as higher correct classification rate.

This letter derives the theoretical lower bound on image correlation coefficient that judges the extent of image degradation. It is shown that the correlation coefficient depends on phase-error variance in antenna aperture domain. Thereby, one can predict image quality before image formation. The theoretical bound is verified by experimental data where the dominant scatterer algorithm (DSA) is used for phase synchronization.

In scheduling problem for automatic assembly, planning of task sequence is closely related with resource allocation. However, they have been separately carried out with little interaction in previous work. In assembly planning problem, there are many feasible sequences for one mechanical product. In order to find the best assembly sequence, we have to decide the cost function for each task a priori and make decision based on summation of costs in sequence. But the cost of each task depends on the machine which executes the allocated task and it becomes difficult to estimate an exact cost of each task at planning stage. Moreover, no concurrent operation is taken into account at planning stage. Therefore, we must consider the sequence planning and the machine allocation simultaneously. In this paper, we propose a new scheduling method in which sequence planning and machine allocation are considered simultaneously. First of all, we propose a modeling method for an assembly sequence including a manufacturing environment. Secondly, we show a guideline in order to determine the estimate function in A* algorithm for assembly scheduling. Thirdly, a new search method based on combination of A* algorithm and supervisor is proposed. Fourthly, we propose a new technique which can take into consider the repetitive process in manufacturing system so as to improve the calculation time. Finally, numerical experiments of proposed scheduling algorithm are shown and effectiveness of proposed algorithm is verified.

A formal necessary and sufficient condition on the general Petri net reachability problem is presented by eliminating all spurious solutions among known nonnegative integer solutions of state equation and unifying all the causes of those spurious solutions into a maximal-strongly-connected and siphon-and-trap subnet Nw. This result is based on the decomposition of a given net (N, Mo) with Md and the concepts of "no immature siphon at the reduced initial marking Mwo" and "no immature trap at the reduced end marking Mwd" on Nw which are both extended from "no token-free siphon at the initial marking Mo" and "no token-free trap at the end marking Md" on N, respectively, which have been both effectively, explicitly or implicitly, used in the well-known fundamental and simple subclasses.

In this paper, we propose a new structure of the frequency domain adaptive filter (FDAF). The proposed structure is based on the modified DFT pair which consists of the FIR filters, so that un-delayed output signal can be obtained with stable convergence and without accumulated error which are problems for the conventional FDAFs. The convergence performance of the proposed FDAF is examined through the computer simulations in the adaptive line enhancer (ALE) comparing with the conventional FDAF and the DCT domain adaptive filter. Furthermore, in order to improve the error performance of the FDAF, we propose a composite algorithm which consists of the normalized step size algorithm for fast convergence and the variable step size one for small estimation error. The advantage of the proposed algorithm is also confirmed through simulations in the ALE. Finally, we propose a reduction method of the computational complexity of the proposed FDAF. The proposed method is to utilize a part of the FFT flow-graph, so that the computational complexity is reduced to O(N log N).

The umbrella cell system, where the same radio system is used for microcells and overlaying macrocells, is a promising strategy for deploying microcell service to cope with the locally increased radio traffic. The interference at microcells due to macrocells can be compensated by increasing the transmit power of microcell. In this paper, a practical method to implementing a microcell system overlaid with an existing macrocell system is proposed. In order to engineer the radio resource planning for the underlaid microcells, transmit power design and application of Channel Segregation, a self-organized dynamic channel assignment, are proposed. By these techniques, the system channels are reused automatically while minimizing interference between macrocell and microcell systems, thereby communication quality of umbrella cell system can be improved. Furthermore, the prime advantage of the proposed method is that locally increased traffic is handled by the underlaid microcells without any extra effort for channel management.

In this paper we consider a parallel and distributed computation of genetic algorithms on loosely-coupled multiprocessor systems. Loosely-coupled ones are more suitable for massively parallel processing and also more easily VLSI implementation than tightly-coupled ones. However, communication overhead on parallel processing is more serious for loosely-coupled ones. We propose in this paper a parallel and distributed execution method of genetic algorithm on loosely-coupled multiprocessor systems of fixed network topologies in which each processor element carries out genetic operations on its own chromosome set and communicates with only the neighbors in order to save communication overhead. We evaluate the proposed method on the multiprocessor systems with ring, torus, and hypercube topologies for benchmark problem instances. From the results, we find that the ring topology is more suitable for the proposed parallel and distributed execution since variety of chromosomes in the ring is kept much more than that in the others. Moreover, we also propose a new network topology called cone which is a hierarchical connection of ring topologies. We show its effectiveness by experimental evaluation.

In this work, a new algorithm for tracking the directions-of-arrival (DOA's) of moving targets by introducing a linear approximation is proposed. The targets are assumed to move with constant angular velocities within a short time and emitting continuously narrow-band signals that impinge on an array of sensors. Therefore the trajectories of targets can be approximated by linear functions of time, which consist of the DOA's and the angular velocities, within the short time. In the condition that the number of targets is known and the outputs vector of the sensors including the additive white complex Gaussian noises is observed continuously, a cost function which consists of the squared residual error vectors is defined. The estimation of the DOA's and the angular velocities of targets is performed by minimizing this cost function. By estimating both the DOA's and the angular velocities at the same time, the proposed algorithm is able to improve the tracking performance for rapidly moving targets. In computer simulations, the performance of the proposed algorithm is compared with the ESPRIT method, which is one of the typical subspace methods with super resolution.

In this paper, we discuss ferroelectric materials suitable for a metal ferroelectric metal insulator semiconductor FET (MFMIS FET). It is important for a ferroelectric material to have a low dielectric constant to enable the application of sufficient electric field to a ferroelectric layer. Films of Sr2Nb2O7 (SNO) and Sr2(Ta1-xNbx)2O7 (STNO) were prepared by the sol-gel method on Pt/IrO2 electrodes for an MFMIS FET. The ferroelectricities of STNO films were confirmed in the range of x=0. 1-0. 3. In case of x=0. 3, the largest remanent polarization was obtained in the hysteresis loop. The remanent polarization and the coercive field are 0. 5 µ C/cm2 and 44 kV/cm, respectively. The film had a low dielectric constant (ε=53). It is considered that the characteristics of STNO thin films are suitable for MFMIS FET.

In indoor optical channels, intersymbol interference (ISI) due to multipath propagation prevents high data rate transmission. In this paper, a new Optical Multi-Wavelength Modulation technique has been investigated for improving the quality of transmission. In this technique, parallel transmission is used, which lowers the data rate per channel and thus reduces the effects of ISI. Furthermore, parallel coding is used in predetermined parallel branches, so that coding can correct errors without changing the system data rate. Simulation results show that a combination of these methods can achieve high quality transmission without reduction of the total data rate.

Degradation of ferroelectricity in PZT (Pb(Zr0. 52, Ti0. 48)O3) thin-film capacitors caused by heat treatment in a reductive ambience is investigated. We have found that the degradation of ferroelectricity depends upon the metal used for the top electrode of the PZT capacitor. The increased degradation in the case of a PZT capacitor with Pt electrodes can be explained by a catalytic reaction on the Pt surface. With the use of an IrO2 non-catalytic top electrode, we have made the ferroelectricity of an IrO2/PZT/Pt capacitor retained even after the H2 annealing at 400, or above.

It is important to test the various kinds of interconnect faults between chips on a card/module. When boundary scan design techniques are adopted, the chip to chip interconnection test generation and application of test patterns is greatly simplified. Various test generation algorithms have been developed for interconnect faults. A new interconnect test generation algorithm is introduced. It reduces the number of test patterns by half over present techniques. It also guarantees the complete diagnosis of multiple interconnect faults.

In a distributed concurrent system such as a computer communication network, the system components communicate with each other via communication links in order to accomplish a desired distributed application. If the links are dynamically established among the components, the system configuration as well as its behavior becomes complex. In this paper, we give formal specification of such a dynamically reconfigurable system in which the components are modeled by communicating finite state machines executed concurrently with the communication links which are dynamically established and disconnected. We also present an algorithm to validate the safety and link-related properties in the specified behavior. Finally, we design and implement a simulator and a validator that enables execution and validation of the given specification, respectively.

This paper proposes a new method to improve cooperation in concurrent systems within the framework of Multi-Agent Systems (MAS). Since subsystems work concurrently, achieving appropriate cooperation among them is important to improve the effectiveness of the overall system. When subsystems are modeled as agents, it is easy to explicitly deal with the interactions among them since they can be modeled naturally as communication among agents with intended information. Contrary to previous approaches which provided the syntax of communication protocols without semantics, we focus on the semantics of cooperation in MAS and aim at allowing agents to exploit the communicated information for cooperation. This is attempted by utilizing more coarse-grained communication based on the different perspective for the balance between formality and richness of communication contents so that each piece of communication contents can convey more meaningful information in application domains. In our approach agents cooperate each other by giving feedbacks based on the metaphor of explanation which is widely used in human interactions, in contrast to previous approaches which use direct orders given by the leader based on the pre-defined cooperation strategies. Agents show the difference between the proposal and counter-proposals for it, which are constructed with respect to the former and given as the feedbacks in the easily understandable terms for the receiver. From the comparison of proposals agents retrieve the information on which parts are agreed and disagreed by the relevant agents, and reflect the analysis in their following behavior. Furthermore, communication contents are annotated by agents to indicate the degree of importance in decision making for them, which contributes to making explanations or feedbacks more understandable. Our cooperation method was examined through experiments on the design of micro satellites and the result showed that it was effective to some extent to facilitate cooperation among agents.

Verification of responsive communication protocols is to determine whether they can recover to a normal state within a predetermined time, even when they enter an abnormal state due to any fault. In this paper, we propose a new verification method for responsive communication protocols using virtual system states, each of which represents several system states. Next, in order to evaluate the effectiveness of the new method, we develop a verification tool based on the proposed method. Then we apply the tool to a broadcasting protocol and measure several metrics on the tool. The experimental results show that (1) the number of system states, (2) the amount of memory used by the tool, and (3) the execution time of the tool, can be drastically reduced.

In this article, we propose a square wave generator whose switching threshold values are switched by external inputs. This circuit is designed to simulate the synchronized luminescence of coupled fireflies. We investigate the behavior of the solutions in two coupled oscillators. The dynamics are demonstrated by a linear autonomous equation piecewisely, therefore, a one-dimensional return map is derived. We also prove the existence of stable in-phase synchronization in the coupled oscillator by using the return map, and we show the existence of regions of periodic solutions within a parameter space. Some theoretical results are confirmed by laboratory measurements.

By treating each different output pattern as a state, we propose a low power architecture for pipelined circuits using bipartition. It is possible that the output of a pipelined circuit transit mainly among some of different states. If some few states dominate most of the time, we could partition the combinational portion of a pipelined circuit into two blocks: one that contains the few states with high activity is small and the other that contains the remainder with low activity is big. The original pipelined circuit is bipartitioned into two individual pipelined circuits. An additional combination logic block is introduced to control which of the two partitioned blocks to work. Power reduction is based on the observation that most time the small block is at work and the big one is at idle. In order to minimize the power consumption of this architecture, we present an algorithm that can improve the efficiency of this additional control block. Experiments with MCNC benchmarks show high percentage of power saving by using our new architecture for low power pipelined circuit design.

It is well known that PZT material properties are strongly dependent on the Zr/Ti ratio. The reliability characteristics, such as the retention and imprint properties, of PZT thin film correlate with the reliability of FRAM(R). PZT films with various Zr/Ti ratios, 60/40, 52/48, 45/55, 40/60 and 30/70 were prepared on Pt/IrO2 and Pt/Ti electrodes by a sol-gel process. With lower Zr/Ti ratio, the grain size becomes smaller and the film was highly oriented to (111) crystallographic plane. But, pyrochlore phase in the PZT films on Pt/IrO2 electrode was detected by SEM and XRD. Hysteresis and pulse responses were measured on the capacitors. With lower Zr/Ti ratio, Pr and Vc become larger. It was found that the preferential (111) orientation played an important role in determining Pr. Voltage shifts which are related to imprint are dependent on the Zr/Ti compositional ratio. Increasing the Ti concentration causes the voltage shift to increase due to more oxygen vacancies. But, this tendency was not in accordance with the results of Qos which were measured by capacitor test simulation of imprint properties for FRAM operation, because the results of Qos did not change monotonically with Ti concentration. However, the capacitor for 45/55 film grown on Pt/IrO2 had good imprint property, similar to the capacitor for sputtered PLZT. In addition, H2 degradation of PZT capacitor with Pt/IrO2 was studied. It was found that H2 annealing degraded the PZT capacitors even at temperatures as low as 150. Thus, imprint and H2 degradation are serious problems for PZT capacitors and these will be a key issue in the reliability of FRAM.

Using transmission electron microscopy (TEM), we studied structural defects in a Sr0. 7Bi2. 3Ta2O9 (SBT) thin film to be used for ferroelectric memory devices. We examined the effects of the substrate, crystal continuity, and dislocations in crystals as major causes of defects. For this study, we used an SBT thin film grown from an alkoxide solution. Since crystal growth was hardly influenced by the substrate, the substrate had little influence on the occurrence of defects resulted in misfit of lattice constant. Regions of partially low crystal continuity were observed in the SBT thin film. In these regions, the orientation was still uniform, but the continuity of the crystal grain was low because of the defects. In addition, variation in contrast was observed in the crystals, however, no obvious variation in chemical composition was found in this region of varying contrast. Therefore, the contrast variation is considered to be attributed to the dislocation. Such a dislocation was found to be occurred in the direction of the (2010) plane in many instances. The defects in the SBT film were also confirmed by the TEM observation.