In this paper we propose a method of formal verfication of fault-tolerance of sequential machines using regular temporal logic. In this method, fault-tolerant properties are described in the form of input-output sequences in regular temporal logic formulas and they are formally verified by checking if they hold for all possible input-output sequences of the machine. We concretely illustrate the method of its application for formal verification of fail-safeness with an example of a comparator for redundant system. The result of verification shows effectiveness of the proposed method.

AlGaAs/GaAs HBT ICs for high bit-rate optical transmission systems, such as preamplifier, D-F/F, differential amplifier, and laser driver, have been newly developed using the hetero guard-ring fully self-aligned HBT (HGFST) fabrication process. In this process, the emitter mesa is ECR-RIBE dry etched using a thick emitter-metal system of WSi and Ti-Pt-Au as etching mask, and a hetero guard-ring composed of a depleted AlGaAs layer is fabricated on p GaAs extrinsic base regions. This process results in highly uniform HBT characteristics. The preamplifier IC exhibits a DC to 18.5-GHz transimpedance bandwidth with a transimpedance gain of 49 dBΩ. The rise time and fall time for the D-F/F IC are 30 and 23 ps, respectively. The laser driver IC has a 40-mAp-p output current swing. The differential amplifier exhibits a DC to 12.1-GHz bandwidth with a 14.2-dB power gain.

We describe an approach for modelling a person's face for model-based coding. The goal is to estimate the 3D shape by combining the contour analysis and shading analysis of the human face image in order to increase the quality of the estimated 3D shape. The motivation for combining contour and shading cues comes from the observation that the shading cue leads to severe errors near the occluding boundary, while the occluding contour cue provides incomplete surface information in regions away from contours. Towards this, we use the deformable model as the common level of integration such that a higher-quality measurement will dominate the depth estimate. The feasibility of our approach is demonstrated using a real facial image.

This paper proposes a second order auto-regressive equation with discrete-valued random coefficients. The auto-regressive equation transforms an independent stochastic sequence into a binary sequence, which is a special case of a stationary Markov chain. The power spectrum, correlation function and the transition probability are explicitly obtained in terms of the random coefficients. Some computer results are illustrated in figures.

Manipulation of Boolean functions is one of the most important techniques for implementing of VLSI logic design systems. This paper presents a fast method for generating prime-irredundant covers from Binary Decision Diagrams (BDDs), which are efficient representation of Boolean functions. Prime-irredundant covers are forms in which each cube is a prime implicant and no cube can be eliminated. This new method generates compact cube sets from BDDs directly, in contrast to the conventional cube set reduction algorithms, which commonly manipulate redundant cube sets or truth tables. Our method is based on the idea of a recursive operator, proposed by Morreale. Morreale's algorithm is also based on cube set manipulation. We found that the algorithm can be improved and rearranged to fit BDD operations efficiently. The experimental results demonstrate that our method is efficient in terms of time and space. In practical time, we can generate cube sets consisting of more than 1,000,000 literals from multi-level logic circuits which have never previously been flattened into two-level logics. Our method is more than 10 times faster than ESPRESSO in large-scale examples. It gives quasi-minimum numbers of cubes and literals. This method should find many useful applications in logic design systems.

This paper presents a new high-speed three-dimensional (3-D) object recognition system based on two-dimensional (2-D) chain code matching. An observed 3-D object is precisely represented by a 2-D chain code sequence from the discrete surface points of the 3-D object, so that any complex objects can be recognized precisely. Moreover, the normalization procedures such as translation, rotation of 3-D objects except scale changes can be performed systematically and regularly regardless of the complexity of the shape of 3-D objects, because almost all the normalization procedures of 3-D objects are included in the 2-D chain code matching procedure. As a result, the additional normalization procedure become only the processing time for scale changes which can be performed easily by normalizing the length of the chain code sequence. In addition, the fast fourier transformation (FFT) is applicable to 2-D chain code matching which calculates cross correlation between an input object and a reference model, so that very fast recognition is performed. In fact, it is demonstrated that the total recognition time of a 3-D ofject is estimated at 5.35 (sec) using the 28.5-MIPS SPARC workstation.

A systematic method is proposed to generate a random image with a known correlation function and the modified Laplace distribution; the modified Laplace distribution includes the one-side exponential distribution and the Laplace distribution as a special case. Several random images with an isotropic correlation and the modified Laplace distribution are generated and displayed in figures.

In using a natural language database interface (NLI) to access the contents of a databese, the user queries may contain terms that do not appear at all in both the NLI lexicon and the database. A friendly NLI should not reject user queries with unknown terms, but should be able to handle them, and should be able to learn new lexical items. Such capability increases the usefulness of the NLI, and allows the NLI to more cover the domain of the underlying database. Therefore, a technique to handle unknown terms is decisive in designing a friendly NLI. In this work, we discuss a method that would allow a NLI to identify the meanings of unknown database field values, and terms that are exceeding the conceptual coverage of the database, in the user queries, by engaging the user in clarification dialogues based on a database-domain hierarchy. It will be shown that the method enables the NLI lexicon to learn new lexical items at run time while the clarification dialogues, and it may provide the necessary information for generating informative answers to some particular failing user queries. Moreover, the method is an efficient means to handle queries with insufficience contextual cues. The examples throughout this work are drawn from FIFA 90, an experimental NLI to a soccer database.

The paper considers multiple-valued logic systems having the property that the ambiguity of the system increases as the ambiguity of each component increases. The partial-ordering relation with respect to ambiguity with the greatest element 1/2 and minimal elements 0, 1 or simply the ambiguity relation is introduced in the set of truth values V {0, 1/ (p1), , 1/2, , (p2) / (p1), 1}. A-monotonic p-valued logic functions are defined as p-valued logic functions monotonic with respect to the ambiguity relation. A necessary and sufficient condition for A-monotonic p-valued logic functions is presented along with the proofs, and their logic formulae using unary operators defined in the ambiguity relation are given. Some discussions on the extension of theories to other partial-ordering relations are also given.

The mechanism of environment-dependent self-organization of "positional information" in a coupled nonlinear oscillator system is proposed as a new principle of realtime coordinative control in biological distributed system. By modeling the pattern formation in tactic response of Physarum plasmodium, it is shown that a global phase gradient pattern self-organized by mutual entrainment encodes not only the positional relationship between subsystems and the total system but also the relative relationship between internal state of the system and the environment.

Process and device technologies of CMOS devices for low-voltage operation are described. First, optimum power-supply voltage for CMOS devices is examined in detail from the viewpoints of circuit performance, device reliability and power dissipation. As a result, it is confirmed that power-supply voltage can be reduced without any speed loss of the CMOS device. Based upon theoretical understanding, the author suggests that lowering threshold voltage and reduction of junction capacitance are indispensable for CMOS devices with low-voltage supply, in order to improve the circuit performance, as expected from MOS device scaling. Process and device technologies such as Silicon On Insulator (SOI) device, low-temperature operation and CMOS Shallow Junction Well FET (CMOS-SJET) structure are reviewed for reduction of the threshold voltage and junction capacitance which lead to high-seed operation of the COMS device at low-voltage.

In the PICASSO, a system for the facial caricature generation, as the basic mechanisms to extract the individuality features of faces and to deform the features have been already introduced, it is expected to realize an autonomous mechanism to evaluate facial caricatures. The evaluation should be based on the framework of human visual cognition. In the PICASSO, some visual illusions such as the Wundt-Fick illusion and the Ponzo illusion for example, are applied to evaluate the shapes of the facial parts such as eyebrows, nose, mouth and face contour, in the deformation process. In many cases, as well-deformed caricatures are evaluated to be successful, it is confirmed that the utilization of the visual illusion is effective to evaluate the results of caricatures. In this paper, some experimental results are presented together with the definition of the evaluation measures and the further subjects.

In this paper, we discuss secure protocols for shared computation of algorithms associated with digital signature schemes based on discrete logarithms. Generic solutions to the problem of cooperatively computing arbitraty functions, though formally provable according to strict security notions, are inefficient in terms of communication--bits and rounds of interaction--; practical protocols for shared computation of particular functions, on the other hand, are often shown secure according to weaker notions of security. We propose efficient secure protocols to share the generation of keys and signatures in the digital signature schemes introduced by Schnorr (1989) and ElGamal (1985). The protocols are built on a protocol for non-interactive verifiable secret sharing (Feldman, 1987) and a novel construction for non-interactively multiplying secretly shared values. Together with the non-interactive protocols for shared generation of RSA signatures introduced by Desmedt and Frankel (1991), the results presented here show that practical signature schemes can be efficiently shared.

Formal verification has become an increasing prominent technique towards establishing the correctness of hardware designs. We present a framework to specifying and verifying the design of systolic architectures. Our approach allows users to represent systolic arrays in Z specification language and to justify the design semi-automatically using the verifier. Z is a notation based on typed set theory and enriched by a schema calculus. We describe how a systolic array for matrix-vector multiplication can be specified and justified with respect to its algorithm.

This paper describes a novel but simple method of implementing waveform relaxation technique for bipolar circuits involving ECL gates. This method performs gate level partitioning of ECL circuits not only during the cutoff state of the input transistor but also when the input transistor is in its active state. Partitioning at all times has become possible due to the favorable property of input and output stages of ECL gates. It is shown that this method is faster than direct method even when the circuits containing only few gates is simulated. Further, it is shown that the present method is applicable to the case where the interconnections between the ECL gates is treated as lossy transmission lines.

In conventional trellis coded modulation (TCM), a bit rate of m/m+1 convolutional encoder is employed for n information bits (mn), where 2n+1 signal points are required. In this paper, we propose a novel TCM system using totally overlapped signal sets (TO-TCM), i.e., each signal point is used twice. Thus, TO-TCM can realize only half signal points (2n) comparing with those of a conventional TCM system (2n+1), and it is possible to implement a coded modulation system without doubling the signal points by an insertion of redundant bits. The cases of the proposed schemes which have a process to extend the minimum free distances between the signal points can achieve a considerable coding gain in comparison to the traditional uncoded systems with 2n signal points. Moreover, as the proposed scheme needs only half signal points (2n) of those of conventional TCM, the average power is lower and it is less sensitive to the carrier phase offset.

This paper discusses a formulation of a basic theory of the information systems, where information is not only transmitted, but is also processed and memorized during the transmission. A deterministic procedure applied by an information system is defined as a logical work, and two measurements with information X, information quantity I(X) and information vitality T(X), are introduced. A system with the ability of transmitting, processing and memorizing information is called an information engine. A system of interconnected information engines is called an information network. The power of an information engine is defined as the maximum capacity of the logical works performed by the engine, and important properties of total power of information network are derived. Response time characteristics and cost minimizing problems of an information network are also discussed.

The properties of the Haar Transform (HT) are discussed based on the Wavelet Transform theory. A system with two channels at resolution 2-1 and 2-2 for detecting paroxysm-spike in human's EEG is presented according to the multiresolution properties of the HT. The system adopts a coarse-to-fine strategy. First, it performs the coarse recognition on the 2-2 channel for selecting the candidate of spike in terms of rather relaxed criterion. Then, if the candidate appears, the fine recognition on the 2-1 channel is carried out for detecting spike in terms of stricter criterion. Three features of spike are extracted by investigating its intrinsic properties based on the HT. In the case of having no knowledge of prior probability of the presence of spike, the Neyman-Pearson criteria is applied to determining thresholds on the basis of the probability distribution of background and spike obtained by the results of statistical analysis to minimize error probability. The HT coefficients at resolution 2-2 and 2-1 can be computed individually and the data are compressed with 4:1 and 2:1 respectively. A half wave is regarded as the basic recognition unit so as to be capable of detecting negative and positive spikes simultaneously. The system provides a means of pattern recognition for non-stationary signal including sharp variation points in the transform domain. It is specially suitable and efficient to recognize the transient wave with small probability of occurrence in non-stationary signal. The practical examples show the performance of the system.

A method for the recognition of Arabic printed scripts entered from an image scanner is presented. The method uses the Hough transformation (HT) to extract features, Dynamic programming (DP) matching technique, and a topological classifier to recognize the characters. A process of characters recognition is further divided into four parts: preprocessing, segmentation of a word into characters, features extraction, and characters identification. The preprocessing consists of the following steps: smoothing to remove noise, baseline drift correction by using HT, and lines separation by making an horizontal projection profile. After preprocessing, Arabic printed words are segmented into characters by analysing the vertical and the horizontal projection profiles using a threshold. The character or stroke obtained from the segmentation process is normalized in size, then thinned to provide it skeleton from which features are extracted. As in the procedure of straight lines detection, a threshold is applied to every cell and those cells whose count is greater than the threshold are selected. The coordinates (R, θ) of the selected cells are the extracted features. Next, characters are classified in two steps: In the first one, the character main body is classified using DP matching technique, and features selected in the HT space. In the second one, simple topological features extracted from the geometry of the stress marks are used by the topological classifier to completely recognize the characters. The topological features used to classify each type of the stress mark are the width, the height, and the number of black pixels of the stress marks. Knowing both the main group of the character body and the type of the stress mark (if any), the character is completely identified.

In this paper, we will define Kleene-Stone logic functions which are functions F: [0, 1]n[0, 1] including the intuitionistic negation into fuzzy logic functions, and they can easily represent the concepts of necessity and possibility which are important concepts of many-valued logic systems. A set of Kleene-Stone logic functions is one of the models of Kleene-Stone algebra, which is both Kleene algebra and Stone algebra, as same as a set of fuzzy logic functions is one of the models of Kleene algebra. This paper, especially, describes some algebraic properties and representation of Kleene-Stone logic functions.