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.

Multiply-stacked structures of Si quantum dots (Si-QDs) in gate oxide are attracting much attention because of their potential importance to improve retention characteristics in a high density charge storage. In this work, we have fabricated 6-fold stacked Si-QDs with 2 nm-thick SiO2 interlayers, whose areal dot density and average dot size were 5.71011 cm-2 in each dot layer and 5 nm in height, and studied progress on electron distribution in 6-fold stacked Si-QDs with 2 nm-thick SiO2 interlayers from the measurements of temporal changes in the surface potential after electron charging and discharging locally at room temperature using an AFM/Kelvin probe technique in clean room air. First, by scanning an area of 22 µm2 with the AFM tip biased at +3 V with respect to the substrate in a tapping mode, the area was negatively charged due to electron injection from the substrate to the dot through the bottom tunnel oxide and subsequently, the central part of 100100 nm2 in the pre-charged area was scanned with the tip biased at -3 V to emit the electrons from the Si-QDs to the substrate. As a result, the negative charging level was markedly reduced in the central part in comparison to its peripheral region. And then, the surface potential of the negatively-charged peripheral region was decay monotonously with time as a result of progressive electron tunneling to the substrate. In contrast to this, the temporal change in the surface potential of the central part shows that the electron charging proceeds with time until the surface potential becomes almost the same as that in the peripheral region. This result can be interpreted in terms of lateral spreading of electrons stored in the Si-QDs layer due to the potential difference between the central part and its peripheral region more negatively charged.

The MOS switch with bootstrapped technique is widely used in low-voltage switched-capacitor circuit. The switched-capacitor circuit with the bootstrapped technique could be a dangerous design approach in the nano-scale CMOS process due to the gate-oxide transient overstress. The impact of gate-oxide transient overstress on MOS switch in switched-capacitor circuit is investigated in this work with the sample-and-hold amplifier (SHA) in a 130-nm CMOS process. After overstress on the MOS switch of SHA with unity-gain buffer, the circuit performances in time domain and frequency domain are measured to verify the impact of gate-oxide reliability on circuit performances. The oxide breakdown on switch device degrades the circuit performance of bootstrapped switch technique.

This paper discusses the input range limitation problem in a track-and-hold circuit and the compensation method using a bootstrapped switch. A bootstrapped switch with an additional control circuit is proposed to compensate charge loss in conventional bootstrapped switch circuit. Simulation results using 0.18-µm CMOS process parameters show that the proposed circuit reduces the bootstrap capacitance down to 25% for the conventional circuit.

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.

In this paper, a high-speed logic circuitry using bootstrapped and low-temperature polysilicon (LTPS) technologies for TFT-LCD panels is proposed. The new circuitry realizes high-speed operation owing to the application of a logic-swing voltage that is wider than the power-supply voltage using bootstrapped technology. As a result, the new logic circuitry can be operated at an operational frequency around 3-10 times higher than that of the conventional circuitry under the conditions of a 0.5 pF load capacitor at the output of a noninverting buffer and +10 V power-supply voltages. The new circuit is named "BST-TFT logic circuitry."

In this letter, we elucidate the ergodic capacity of multiple-input multiple-output (MIMO) systems with M-ary phase-shift keying (MPSK) modulation and time-multiplexed pilots in frequency-flat Rayleigh fading environment. With linear minimum mean square error (LMMSE) channel estimation, the optimal pilots design is presented. For mathematical tractability, we derive an easy-computing closed-form lower bound of the channel capacity. Based on the lower bound, the optimal power allocation between the data and pilots is also presented in closed-form, and the optimal training length is investigated by numerical optimization. It is shown that the transmit scheme with equal training and data power and optimized training length provides suboptimal performance, and the transmit scheme with optimized training length and training power is optimal. With the latter scheme, in most situations, the optimal training length equals the number of the transmit antennas and the corresponding optimal power allocation can be easily computed with the proposed formula.

In difficult classification problems of the z-dimensional points into two groups giving 0-1 responses due to the messy data structure, we try to find the denser regions for the favorable customers of response 1, instead of finding the boundaries to separate the two groups. Such regions are called the bumps, and finding the boundaries of the bumps is called the bump hunting. The main objective of this paper is to find the largest region of the bumps under a specified ratio of the number of the points of response 1 to the total. Then, we may obtain a trade-off curve between the number of points of response 1 and the specified ratio. The decision tree method with the Gini's index will provide the simple-shaped boundaries for the bumps if the marginal density for response 1 shows a rather simple or monotonic shape. Since the computing time searching for the optimal trees will cost much because of the NP-hardness of the problem, some random search methods, e.g., the genetic algorithm adapted to the tree, are useful. Due to the existence of many local maxima unlike the ordinary genetic algorithm search results, the extreme-value statistics will be useful to estimate the global optimum number of captured points; this also guarantees the accuracy of the semi-optimal solution with the simple descriptive rules. This combined method of genetic algorithm search and extreme-value statistics use is new. We apply this method to some artificial messy data case which mimics the real customer database, showing a successful result. The reliability of the solution is discussed.

In this paper, we describe a bootstrapped nMOS switch that is modified to reduce leakage current for nMOS reversible energy recovery logic (nRERL) [1]. Conventional bootstrapped switches are not suitable for nRERL because they have nonadiabatic loss due to leakage current that flows while boosted. Therefore, we lowered the gate voltage of the isolation transistor in each bootstrapped switch to reduce this leakage current. With detailed analysis and simulation, we determined the range of the bias voltage, in which the switches can transfer full-swing input signals. We implemented a simple 8-bit nRERL microprocessor into silicon and measured its energy consumption to confirm our analysis. For the supply voltage of 1.8 V and the operating frequency of 880 kHz, we found that the microprocessor consumed about 8.5 pJ/cycle for 1.3 V < Vbias <1.6 V, which was just about a half of its energy consumption when Vbias = 1.7 V.

Recently, various decoding algorithms with Low Density Parity Check (LDPC) codes have been proposed. Most algorithms can be divided into a hard decision algorithm and a soft decision algorithm. The Weighted Bit Flipping (WBF) algorithm that is between a hard decision and a soft decision algorithms has been proposed. The Bootstrapped WBF and Modified WBF algorithms have been proposed to improve the error rate performance and decoding complexity of the WBF algorithm. In this letter, we apply the Bootstrap step to the Modified WBF algorithm. We show that the Bootstrapped modified WBF algorithm outperforms the WBF, Bootstrapped WBF, and Modified WBF algorithms. Moreover, we show that the Bootstrapped modified WBF algorithm has the lowest decoding complexity.

This paper concerns the design, implementation and subsequent experimental validation of a low-voltage analog CMOS switch based on a gate-bootstrapped method. The main part of the proposed circuit is a new low-voltage and low-stress CMOS clock voltage doubler. Through the use of a dummy switch, the charge injection induced by the bootstrapped switch is greatly reduced resulting in improved sample-and-hold accuracy. An important attribute of the design is that the ON-resistance is nearly constant. A test chip has been designed and fabricated using a TSMC 0.18 µm CMOS process (single poly, n-well) to confirm the operation of the circuit for a supply voltage of down to 0.65 V.

We propose a cell library development methodology for throughput enhancement of character projection equipment. First, an ILP (Integer Linear Programming)-based cell selection is proposed for the equipment for which both of the CP (Character Projection) and VSB (Variable Shaped Beam) methods are available, in order to minimize the number of electron beam (EB) shots, that is, time to fabricate chips. Secondly, the influence of cell directions on area and delay time of chips is examined. The examination helps to reduce the number of EB shots with a little deterioration of area and delay time because unnecessary directions of cells can be removed. Finally, a case study is shown in which the numbers of EB shots are shown for several cases.

Cross-document personal name resolution is the process of identifying whether or not a common personal name mentioned in different documents refers to the same individual. Most previous approaches usually rely on lexical matching such as the occurrence of common words surrounding the entity name to measure the similarity between documents, and then clusters the documents according to their referents. In spite of certain successes, measuring similarity based on lexical comparison sometimes ignores important linguistic phenomena at the semantic level such as synonym or paraphrase. This paper presents a semantics-based approach to the resolution of personal name crossover documents that can make the most of both lexical evidences and semantic clues. In our method, the similarity values between documents are determined by estimating the semantic relatedness between words. Further, the semantic labels attached to sentences allow us to highlight the common personal facts that are potentially available among documents. An evaluation on three web datasets demonstrates that our method achieves the better performance than the previous work.

The enormous capacity potential of multiple-input multiple-output (MIMO) is based on some unrealistic assumptions, such as the complete channel state information (CCSI) at the receiver and Gaussian distributed data. In this paper, in frequency-flat Rayleigh fading environment, we investigate the ergodic capacity of MIMO systems with M-ary phase-shift keying (MPSK) modulation and superimposed pilots for channel estimation. With linear minimum mean square error (LMMSE) channel estimation, the optimal pilots design is presented. For the mathematical tractability, we also derive an easy-computing closed-form lower bound of the channel capacity. Furthermore, the optimal power allocation between the data and pilots is investigated by numerical optimization. It is shown that more power should be devoted to the data in low SNR environments and to the pilots in high SNR environments.

This paper aims at challenging Bernstein's problem called the "Degrees-of-Freedom problem," which remains unsolved from both the physiological and robotics viewpoints. More than a half century ago A.N. Bernstein observed that "dexterity" residing in human limb motion emerges from accumulated involvement of multi-joint movements in surplus DOF. It is also said in robotics that redundancy of DOFs in robot mechanisms may contribute to enhancement of dexterity and versatility. However, kinematic redundancy incurs a problem of ill-posedness of inverse kinematics from task-description space to joint space. In the history of robotics research such ill-posedness problem of inverse-kinematics has not yet been attacked directly but circumvented by introducing an artificial performance index and determining uniquely an inverse kinematics solution by minimizing it. Instead of it, this paper introduces two novel concepts named "stability on a manifold" and "transferability to a submanifold" in treating the case of human multi-joint movements of reaching and shows that a sensory feedback from task space to joint space together with a set of adequate dampings enables any solution to the overall closed-loop dynamics to converge naturally and coordinately to a lower-dimensional manifold describing a set of joint states fulfilling a given motion task. This means that, without considering any type of inverse kinematics, the reaching task can be accomplished by a sensory feedback with adequate choice of a stiffness parameter and damping coefficients. It is also shown that these novel concepts can cope with annoying characteristics called "variability" of redundant joint motions seen typically in human skilled reaching. Finally, it is pointed out that the proposed control signals can be generated in a feedforward manner in case of human limb movements by referring to mechano-chemical characteristics of activation of muscles. Based on this observation, generation of human skilled movements of reaching can be interpreted in terms of the proposed "Virtual-Spring" hypothesis instead of the traditional "Equilibrium-Point" hypothesis.

The process of evaluating and selecting Commercial Off-The-Shelf (COTS) products is complicated because of conflicting priorities of the stakeholders, complex interdependences among the evaluation criteria, multiple evaluation objectives, changing system requirements, and a large number of similar COTS products with extreme capability differences. Numerous COTS evaluation and selection methods have been proposed to address the complexity of the process. Some of these methods have been successfully applied in industry. However, negotiation to resolve stakeholder conflicts is still an ad hoc process. In this paper, we present a systematic model that assists the COTS selection stakeholders in identifying conflicts, as well as in determining and evaluating conflict resolution options. Our model is facilitated by an agent-based decision support system, which has user agents that assist the stakeholders in the COTS evaluation and negotiation process. The agents utilize a hybrid of analytic and artificial intelligence techniques to identify conflicts and the corresponding agreement options. Moreover, each user agent analyzes the agreement options in detail before advising its client about which goals to optimize, and which goals to compromise in order to reach agreement with the other stakeholders. Finally, the community of agents facilitates information sharing among stakeholders in a bid to improve the quality of their COTS selection decisions.

We observed the optically forbidden energy transfer between cubic CuCl quantum dots coupled via an optical near-field interaction using time-resolved near-field photoluminescence (PL) spectroscopy. The energy transfer time and exciton lifetime were estimated from the rise and decay times of the PL pump-probe signal, respectively. We found that the exciton lifetime increased as the energy transfer time fell. This result strongly supports the notion that near-field interaction between QD makes the anti-parallel dipole coupling. Namely, a quantum-dots pair coupled by an optical near field has a long exciton lifetime which indicates the anti-parallel coupling of QDs forming a weakly radiative quadrupole state.

Footsteps, with different shoes of heels, sneakers, leathers or even bare footed, will appear in different grounds of concrete, wood, etc. If a footstep is discriminable, the application to various fields can be considered. In this paper, the feature extraction of a footstep is investigated. We focus on the recognizing a certain kind of footstep waveforms under the restricted condition. We propose a new methodology using the feature parameter such as the peak frequency set by the mel-cepstrum analysis, the walking intervals and the similarity of spectrum envelope. It is shown for personal identification that the performance of the proposed method is effective.

An important issue in applying machine learning algorithms to Natural Language Processing areas such as Named Entity Recognition tasks is to overcome the lack of tagged corpora. Several bootstrapping methods such as co-training have been proposed as a solution. In this paper, we present a different approach using the Web resources. A Named Entity (NE) tagged corpus is generated from the Web using about 3,000 names as seeds. The generated corpus may have a lower quality than the manually tagged corpus but its size can be increased sufficiently. Several features are developed and the decision list is learned using the generated corpus. Our method is verified by comparing it to both the decision list learned on the manual corpus and the DL-CoTrain method. We also present a two-level classification by cascading highly precise lexical patterns and the decision list to improve the performance.

A hybrid method-of-moments (MoM) and immittance approach for efficient and accurate analysis of printed slots and strips of arbitrary shape in layered waveguide for various applications has been proposed. An impedance-type MoM is formulated from the electric field integral equation (EFIE) for printed strip case and an admittance-type MoM is formulated from the magnetic field integral equation (MFIE) for the printed slot case, using the Galerkin's technique. Immittance approach has been used to calculate spectral dyadic Green's functions for the layered waveguide. For efficient analysis of large and complex structures, equivalent circuit parameters of a block are first extracted and complete structure is analyzed through cascaded ABCD matrices. The equivalent circuit characterization of printed strip and slot in layered waveguide has been done for the first time. Finite periodic structure loaded with printed strips has been investigated and it shows the electromagnetic bandgap (EBG) behavior. The electromagnetic (EM) program hence developed is checked for its numerical accuracy and efficiency with results generated with High-frequency structure simulator (HFSS) and shows good performance.