Some plants have air purification ability. This purification ability of plants is considered a promising method for indoor air purification because of the low cost and high purification performance. Therefore, several studies have been carried out to investigate the relationship between the air purification ability of plants and environmental conditions. Nevertheless, the purification mechanism and process have not been clarified yet. In this paper, we investigated the air purification process in plants by bioelectrical potential analysis using linear and nonlinear analysis methods. First, we showed that two types of plants have a high air purification ability; Schefflera and Boston fern. Next, we measured AC bioelectrical potential during the purifying process of plants for pollutant gas. Then, we evaluated the power spectra of time series data of the bioelectrical potential. We found that the power spectra shifted to a lower level after gas injection over all frequencies. Thus, the higher power spectrum came from possible higher physiological activities of the plant. Finally, we introduced a nonlinear analysis method from the dynamical system theory. We transformed the time series data of the potential to a higher dimensional state space using a delay coordinate, which is often used in the field of nonlinear time series analysis. The results show that the orbits in the reconstructed state space have a large variation in gas injection. These experimental results suggest that the measurement of bioelectrical potential could become a useful method for evaluating the air purification ability of plants.

A large memory is typically designed with multiple identical memory blocks for reducing delay and power. The circuit verification of individual memory blocks can be effectively handled by the Symbolic Trajectory Evaluation (STE) approach. However, if multiple memory blocks are integrated into a single system, the STE approach cannot verify it economically. This paper introduces algorithms for verifying block-level connectivity of memories. The verification time of a large memory can be reduced drastically by using bottom-up verification scheme. That is, a memory block is first verified thoroughly, and then only the interconnection between memory blocks of the large memory needs to be verified. The proposed verification algorithms require (3n+2(log2n+1)+3log2m) Read/Write operations for a 2nm-bit memory, where n and m are the address width and data width, respectively. Also, the algorithms can verify 100% of the inter-port and intra-port signal misplaced faults of the address, data input, and data output ports.

Latch-based circuits have advantages for timing and are widely used for high-speed custom circuits. ASIC design flows, however, are based on circuits with flip-flops. This paper describes a new timing optimization algorithm by replacing the flip-flops in high-end ASICs by latches without changing the functionality of the circuits. Timing is optimized by using a fixed-phase retiming minimizing the impact of clock skew and jitter. A formal equivalence verification method that assures the logical correctness of the latch-replaced circuits is also proposed. Experimental results show that the optimization algorithm decreases the delay of benchmark circuits by as much as 17%.

It is novel to apply magnetic field in the indoor air purification by collecting pre-charged suspended particles. Based on experiments and analysis of relative data, the effects of some influential factors (the number of discharge electrode, the polarity and magnitude of discharge voltage, the direction and magnitude of magnetic field, the initial velocity of charged particles, the distance between particle collecting plates) on the efficiency of air purification are discussed. The results indicate that the purification efficiency is improved by applying the proper magnetic field, -6 kV direct current voltage is an optimal voltage and there are optimal magnitudes of the distance between collecting plate and the initial velocity of particles in the purification process.

This paper presents a multipath interference canceller (MPIC) configuration based on multipath interference (MPI) replica generation per transmit antenna (called PTA-MPIC). This configuration is associated with Space Time Transmit Diversity (STTD) for the common control physical channel (CCPCH), which takes advantage of tentative decision data after STTD decoding, and with closed-loop type phase control (PC) transmit diversity for the dedicated physical channel (DPCH) employing tentative decision data after diversity combining, in the W-CDMA forward link. This paper also proposes transmitter carrier phase verification, i.e., an antenna verification method used in PC transmit diversity, that utilizes the dedicated pilot symbols in a DPCH after the PTA-MPIC removes the MPI components. The one-stage PTA-MPIC removes the MPI from the common pilot channel (CPICH), the CCPCH, and the synchronization channel (SCH). The simulation results show that this canceller reduces the required average transmit Eb/N0 of the DPCH at the average BER of 10-3 by approximately 3.0 dB compared to that using a MF-based Rake receiver (the transmit power ratio of each common channel to DPCH is RCPICH/DPCH = 3 dB, RCCPCH/DPCH = 5 dB, and RSCH/DPCH = 3 dB, with TPC and without antenna diversity reception at the user equipment). Furthermore, it is shown that in the two-stage PTA-MPIC with MPI suppression for all channels associated with PC transmit diversity, the required average transmit Eb/N0 employing the proposed antenna verification is reduced by approximately 0.3 dB, 0.5 dB, and 1.2 dB compared to that using the conventional antenna verification when the transmission power ratio of the interfering DPCH to the desired DPCH is RInt/Des = 0 dB, 3 dB, and 6 dB for ten DPCHs. This is because the number of detection errors of the transmitted carrier phase in the second antenna due to feedback information bit decoding error is reduced.

This paper presents a novel design of connected digit patterns to achieve high accuracy text-prompted speaker verification over a cellular phone network. To reduce the error rate, a phoneme-balanced connected digit pattern for enrollment, and digit-sequence-preserving connected digit patterns for verification (i.e. patterns preserving partial digit sequences of the enrollment pattern) are proposed. In addition to these, a decision procedure using multiple patterns has been designed to overcome the low quality of cellular phone speech. Experimental results on cellular phone speech showed the phoneme-balanced patterns for enrollment and digit-sequence-preserving patterns for verification reduced more than 50% of equal error rate compared to the conventional method using randomly-selected and randomly-reordered digit patterns. The decision procedure reduced 60% of the error rate. In addition, this paper shows that verification patterns depending on the pattern of a preceding utterance reduced 10% of the error rate. Overall, the error rate obtained by the proposed method was 1% for 99% of clients and 95% of impostors.

The PLC (Programmable Logic Controller) has been widely used in the industrial world as a controller for manufacturing systems, as a process controller and so on. The conventional PLC has been designed and verified as a pure Discrete Event System (DES) by using an abstract model of a controlled plant. In verifying the PLC, however, it is also important to take into account the physical behavior (e.g. dynamics, shape of objects) of the controlled plant in order to guarantee such important factors as safety. This paper presents a new verification technique for the PLC-based control system, which takes into account these physical behaviors, based on a Hybrid Dynamical System (HDS) framework. The other key idea described in the paper is the introduction of the concept of signed distance which not only measures the distance between two objects but also checks whether two objects interfere with each other. The developed idea is applied to illustrative material handling problems, and its usefulness is demonstrated.

This paper presents an algorithm for fingerprint matching using the Phase-Only Correlation (POC) function. One of the most difficult problems in human identification by fingerprints has been that the matching performance is significantly influenced by fingertip surface condition, which may vary depending on environmental or personal causes. This paper proposes a new fingerprint matching algorithm using phase spectra of fingerprint images. The proposed algorithm is highly robust against fingerprint image degradation due to inadequate fingertip conditions. A set of experiments is carried out using fingerprint images captured by a pressure sensitive fingerprint sensor. The proposed algorithm exhibits efficient identification performance even for difficult fingerprint images that could not be identified by the conventional matching algorithms.

Software applications for the transfer of money or personal information are increasingly common on the Internet. These applications require user authentication for confirming legitimate users. One-time password authentication methods risk a stolen-verifier problem or other steal attacks because the authentication on the Internet server stores the user's verifiers and secret keys. The SAS-2 (Simple And Secure password authentication protocol, ver.2) and the ROSI (RObust and SImple password authentication protocol) are secure password authentication protocols. However, we have found attacks on SAS-2 and ROSI. Here, we propose a new method which eliminates such problems without increasing the processing load and can perform high security level same as S/Key systems without resetting the verifier.

This letter handles symbolic simulation for high-level hardware design descriptions including uninterpreted functions. Two new heuristics are introduced, which are named "symbolic function table" and "synchronization". In the experiment, the equivalence of a hardware/software codesign was checked up to a given finite number of cycles, which is composed of a behavioral design, that is, a small DSP program written in C, and its register-transfer-level implementation, a VLIW architecture with an assembly program. Our symbolic simulator succeeded in checking the equivalence of the two descriptions which were not tractable without the heuristics.

This paper describes a comprehensive simulation and test environment for prototype LSI verification. We develop a Perl package, ST, for simulation & test of digital circuits. A designer can describe a testbench with the Perl syntax, which can be converted to various kinds of simulators and LSI testers. Parameters such as a target simulator/tester, cycle time and voltage levels can be changed very easily just modifying arguments of subroutines. We also develop DUT boards which consist of a tester-dependent mother board and a package-dependent daughter board. Using ST and the DUT boards, a designer can start verification just after getting fabricated LSIs.

Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines a level oriented formal model based on time Petri nets, and then proposes a partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.

Relative time-stamping schemes prove the chronological sequence of digital documents and their integrity. Since the chronological sequence is verified by tracing the link between two timestamps, it is desirable that the length of the verification path is short. Buldas, Laud, Lipmaa, and Villemson have proposed the relative time-stamping scheme based on the binary link. In this paper, we extend the binary link to the ternary link, and apply it to the relative time-stamping scheme. We show that the maximum length of the verification path of the proposed scheme is shorter than that of the previous scheme. Moreover, we show that the average length of the proposed scheme is shorter than that of the previous scheme. Thus, the proposed time-stamping schemes is more efficient than the previous scheme.

Software certification is a notoriously difficult problem. From software reliability engineering perspective, certification process must provide evidence that the program meets or exceeds the required level of reliability. When certifying the reliability of a high assurance system very few, if any, failures are observed by testing. In statistical estimation theory the probability of an event is estimated by determining the proportion of the times it occurs in a fixed number of trials. In absence of failures, the number of required certification tests becomes impractically large. We suggest that subjective reliability estimation from the development lifecycle, based on observed behavior or the reflection of one's belief in the system quality, be included in certification. In statistical terms, we hypothesize that a system failure occurs with the hypothesized probability. Presumed reliability needs to be corroborated by statistical testing during the reliability certification phase. As evidence relevant to the hypothesis increases, we change the degree of belief in the hypothesis. Depending on the corroboration evidence, the system is either certified or rejected. The advantage of the proposed theory is an economically acceptable number of required system certification tests, even for high assurance systems so far considered impossible to certify.

NK-Landscapes are stochastically generated fitness functions on bit strings, parameterized with N bits and K epistatic interactions between bits. The term epistasis describes nonlinearities in fitness functions due to changes in the values of interacting bits. Empirical studies have shown that the overall performance of random bit climbers on NK-Landscapes is superior to the performance of some simple and enhanced genetic algorithms (GAs). Analytical studies have also lead to suggest that NK-Landscapes may not be appropriate for testing the performance of GAs. In this work we study the effect of selection, drift, mutation, and recombination on NK-Landscapes for N = 96. We take a model of generational parallel varying mutation GA (GA-SRM) and switch on and off its major components to emphasize each of the four processes mentioned above. We observe that using an appropriate selection pressure and postponing drift make GAs quite robust on NK-Landscapes; different to previous studies, even simple GAs with these two features perform better than a random bit climber (RBC+) for a broad range of classes of problems (K 4). We also observe that the interaction of parallel varying mutation with crossover improves further the reliability of the GA, especially for 12 < K < 32. Contrary to intuition, we find that for small K a mutation only evolutionary algorithm (EA) is very effective and crossover may be omitted; but the relative importance of crossover interacting with varying mutation increases with K performing better than mutation alone (K > 12). This work indicates that NK-Landscapes are useful for testing each one of the major processes involved in a GA and for assessing the overall behavior of a GA on complex non-linear problems. This study also gives valuable guidance to practitioners applying GAs to real world problems of how to configure the GA to achieve better results as the non-linearity and complexity of the problem increases.

This paper investigates the accepting powers of deterministic, Las Vegas, self-verifying nondeterministic, and nondeterministic one-way multi-counter automata with time-bounds. We show that (1) for each k1, there is a language accepted by a Las Vegas one-way k-counter automaton operating in real time, but not accepted by any deterministic one-way k-counter automaton operating in linear time, (2) there is a language accepted by a self-verifying nondeterministic one-way 2-counter automaton operating in real time, but not accepted by any Las Vegas one-way multi-counter automaton operating in polynomial time, (3) there is a language accepted by a self-verifying nondeterministic one-way 1-counter automaton operating in real time, but not accepted by any deterministic one-way multi-counter automaton operating in polynomial time, and (4) there is a language accepted by a nondeterministic one-way 1-counter automaton operating in real time, but not accepted by any self-verifying nondeterministic one-way multi-counter automaton operating in polynomial time.

This paper describes the effects of system LSI design with C language-based behavioral synthesis following several trials of design period reduction and quality improvement for a variety of circuit types. The results of these trials are analyzed from the viewpoints of description productivity, verification productivity, reusability and design flexibility as well as hardware and software co-verification. First the C-based design flow proposed by the authors is described, and the design productivity and verification productivity under this design flow is compared to RTL design. The reusability of the behavioral IP core and its efficiency with HW/SW co-verification are also shown using design examples. Next, using the example of an MPEG-4 video decoder design, a typical design process in a C-based design is shown with considerations regarding verification efficiency, reusability of the IP core and HW/SW co-verification. Finally, the authors' perspectives regarding future directions of system LSI design are discussed.

This paper investigates a new method for creating robust speaker models to cope with inter-session variation of a speaker in a continuous HMM-based speaker verification system. The new method estimates session-independent parameters by decomposing inter-session variations into two distinct parts: session-dependent and -independent. The parameters of the speaker models are estimated using the speaker adaptive training algorithm in conjunction with the equalization of session-dependent variation. The resultant models capture the session-independent speaker characteristics more reliably than the conventional models and their discriminative power improves accordingly. Moreover we have made our models more invariant to handset variations in a public switched telephone network (PSTN) by focusing on session-dependent variation and handset-dependent distortion separately. Text-independent speech data recorded by 20 speakers in seven sessions over 16 months was used to evaluate the new approach. The proposed method reduces the error rate by 15% relatively. When compared with the popular cepstral mean normalization, the error rate is reduced by 24% relatively when the speaker models were recreated using speech data recorded in four or more sessions.

In the last three decades of the 20th Century, research in speech recognition has been intensively carried out worldwide, spurred on by advances in signal processing, algorithms, architectures, and hardware. Recognition systems have been developed for a wide variety of applications, ranging from small vocabulary keyword recognition over dial-up telephone lines, to medium size vocabulary voice interactive command and control systems for business automation, to large vocabulary speech dictation, spontaneous speech understanding, and limited-domain speech translation. Although we have witnessed many new technological promises, we have also encountered a number of practical limitations that hinder a widespread deployment of applications and services. On one hand, fast progress was observed in statistical speech and language modeling. On the other hand only spotty successes have been reported in applying knowledge sources in acoustics, speech and language science to improving speech recognition performance and robustness to adverse conditions. In this paper we review some key advances in several areas of speech recognition. A bottom-up detection framework is also proposed to facilitate worldwide research collaboration for incorporating technology advances in both statistical modeling and knowledge integration into going beyond the current speech recognition limitations and benefiting the society in the 21st century.

We use the Monte Carlo method to simulate electron transport in a zig-zag single-walled carbon nanotube with a wrapping index of n=10. Results show large low-field mobility, negative differential mobility, and large peaks in the drift velocity reaching 3.5107 cm/s.