Since their inception almost fifty years ago, hidden Markov models (HMMs) have have become the predominant methodology for automatic speech recognition (ASR) systems--today, most state-of-the-art speech systems are HMM-based. There have been a number of ways to explain HMMs and to list their capabilities, each of these ways having both advantages and disadvantages. In an effort to better understand what HMMs can do, this tutorial article analyzes HMMs by exploring a definition of HMMs in terms of random variables and conditional independence assumptions. We prefer this definition as it allows us to reason more throughly about the capabilities of HMMs. In particular, it is possible to deduce that there are, in theory at least, no limitations to the class of probability distributions representable by HMMs. This paper concludes that, in search of a model to supersede the HMM (say for ASR), rather than trying to correct for HMM limitations in the general case, new models should be found based on their potential for better parsimony, computational requirements, and noise insensitivity.

Automated reasoning of inductive theorems is considered important in program verification. To verify inductive theorems automatically, several implicit induction methods like the inductionless induction and the rewriting induction methods have been proposed. In studying inductive theorems on higher-order rewritings, we found that the class of the theorems shown by known implicit induction methods does not coincide with that of inductive theorems, and the gap between them is a barrier in developing mechanized methods for disproving inductive theorems. This paper fills this gap by introducing the notion of primitive inductive theorems, and clarifying the relation between inductive theorems and primitive inductive theorems. Based on this relation, we achieve mechanized methods for proving and disproving inductive theorems.

This paper describes an on-line handwritten Japanese text recognition system that is liberated from constraints on line direction and character orientation. The recognition system first separates freely written text into text line elements, second estimates the line direction and character orientation using the time sequence information of pen-tip coordinates, third hypothetically segment it into characters using geometric features and apply character recognition. The final step is to select the most plausible interpretation by evaluating the likelihood composed of character segmentation, character recognition, character pattern structure and context. The method can cope with a mixture of vertical, horizontal and skewed text lines with arbitrary character orientations. It is expected useful for tablet PC's, interactive electronic whiteboards and so on.

This paper presents a model and its effect for on-line handwritten Japanese text recognition free from line-direction constraint and writing format constraint such as character writing boxes or ruled lines. The model evaluates the likelihood composed of character segmentation, character recognition, character pattern structure and context. The likelihood of character pattern structure considers the plausible height, width and inner gaps within a character pattern that appear in Chinese characters composed of multiple radicals (subpatterns). The recognition system incorporating this model separates freely written text into text line elements, estimates the average character size of each element, hypothetically segments it into characters using geometric features, applies character recognition to segmented patterns and employs the model to search the text interpretation that maximizes likelihood as Japanese text. We show the effectiveness of the model through recognition experiments and clarify how the newly modeled factors in the likelihood affect the overall recognition rate.

This paper incorporates statistical language models into an on-line handwriting recognition system for devices with limited memory and computational resources. The objective is to minimize the error recognition rate by taking into account the sentence context to disambiguate poorly written texts. Probabilistic word n-grams have been first investigated, then to fight the curse of dimensionality problem induced by such an approach and to decrease significantly the size of the language model an extension to class-based n-grams has been achieved. In the latter case, the classes result either from a syntactic criterion or a contextual criteria. Finally, a composite model is proposed; it combines both previous kinds of classes and exhibits superior performances compared with the word n-grams model. We report on many experiments involving different European languages (English, French, and Italian), they are related either to language model evaluation based on the classical perplexity measurement on test text corpora but also on the evolution of the word error rate on test handwritten databases. These experiments show that the proposed approach significantly improves on state-of-the-art n-gram models, and that its integration into an on-line handwriting recognition system demonstrates a substantial performance improvement.

G.Huet (1980) showed that a left-linear term-rewriting system (TRS) is Church-Rosser (CR) if P Q for every critical pair where P Q is a parallel reduction from P to Q. But, it remains open whether it is CR when Q P for every critical pair . In this paper, we give a partial solution to this problem, that is, a left-linear TRS is CR if Q P for every critical pair where Q P is a parallel reduction with the set W of redex occurrences satisfying that if the critical pair is generated from two rules overlapping at an occurrence u, then the length |w| |u| for every w W. We also show that a left-linear TRS is CR if Q P for every critical pair generated from two rules overlapping at an occurrence u. Here, Q P is either Q = P or a reduction whose redex occurrence is not greater than u. This condition is incomparable with the previous one and a partial solution to the open problem of ascertaining whether it is CR when Q P for every critical pair .

Simply-typed term rewriting systems (STRSs) are an extension of term rewriting systems. STRSs can be naturally handle higher order functions, which are widely used in existing functional programming languages. In this paper we design recursive and lexicographic path orders, which can efficiently prove the termination of STRSs. Moreover we discuss an application to the dependency pair and the argument filtering methods, which are very effective and efficient support methods for proving termination.

A term rewriting system which effectively preserves recognizability (EPR-TRS) has good mathematical properties. In this paper, a new subclass of TRSs, layered transducing TRSs (LT-TRSs) is defined and its recognizability preserving property is discussed. The class of LT-TRSs contains some EPR-TRSs, e.g., {f(x)f(g(x))} which do not belong to any of the known decidable subclasses of EPR-TRSs. Bottom-up linear tree transducer, which is a well-known computation model in the tree language theory, is a special case of LT-TRS. We present a sufficient condition for an LT-TRS to be an EPR-TRS. Also reachability and joinability are shown to be decidable for LT-TRSs.

G. Huet (1980) showed that a left-linear term-rewriting system (TRS) is Church-Rosser (CR) if P Q for every critical pair < P, Q > where P Q is a parallel reduction from P to Q. This paper shows that Huet's result can be generalized under the assumption that a subsystem K of TRS R (i.e., KR) is CR. That is, we show that R is CR if P K Q for every < P, Q > CP(K,R-K) and P R-K *K*K Q for every < P, Q > CP(R-K,R). Here, CP(R1,R2) is the set of critical pairs obtained from some rule of R1 and one of R2.

We propose a new decidable subclass of term rewriting systems (TRSs) for which strongly normalizing (SN) property is decidable. The new class is called almost orthogonal inverse finite path overlapping TRSs (AO-FPO-1-TRSs) and the class properly includes AO growing TRSs for which SN is decidable. Tree automata technique is used to show that SN is decidable for AO-FPO-1-TRSs.

This paper describes a novel approach to high-level synthesis of complex pipelined circuits, including pipelined circuits with feedback. This approach combines a high-level, modular specification language with an efficient implementation. In our system, the designer specifies the circuit as a set of independent modules connected by conceptually unbounded queues. Our synthesis algorithm automatically transforms this modular, asynchronous specification into a tightly coupled, fully synchronous implementation in synthesizable Verilog.

This paper describes a biometric-based key generation method and its application to a secure communication system. In the proposed method, a personal key which is unique to each user is generated by extracting his/her biometric information. Using the generated personal key, a secure communication system which has the functions of confidentiality and user authentication is realized. As an example of the proposed method, we introduce a personal key generation method based on one's handwriting, and a secure telewriting system which enables the encryption of handwriting information as well as the authentication of a writer. Some simulation results indicate the possibility of realizing the above functions by using a writer's personal key.

Arts and Giesl introduced the notion of dependency pairs, which gives effective methods for proving termination of term rewriting systems (TRSs). In this paper, we extend the notion to AC-TRSs, and introduce new methods for effectively proving AC-termination. It is impossible to directly apply the notion of dependency pairs to AC-TRSs. To avoid this difficulty, we introduce the notion of extended dependency pairs. Finally we define the AC-dependency pair and the AC-dependency chain. Furthermore, we propose approximated AC-dependency graphs, which is very useful for proving AC-termination in practice, using the approximation technique based on Ω-reduction and ΩV-reduction.

We propose a new conditional linearization based on left-right separated conditional term rewriting systems, in which the left-hand side and the right-hand side of a rewrite rule have separate variables. By developing a concept of weight decreasing joinability we first present a sufficient condition for the Church-Rosser property of left-right separated conditional term rewriting systems. Applying this result to conditional linearization, we next show sufficient conditions for the unique normal form property and the Church-Rosser property of non-duplicating (unconditional) term rewriting systems even if they are non-left-linear or overlapping.

We propose an extraction method of personal features based on on-line handwriting information. Most recent research has been focused on signature verification, especially in the field of on-line writer verification. However, signature verification has a serious problem in that it will accept forged handwriting. To solve this problem, we have introduced an on-line writer verification method which uses ordinary characters. In this method, any handwritten characters (i.e., ordinary characters) are accepted as a text in the verification process, and the text used in the verification process can be different from that in the enrollment process. However, in the proposed method, personal features are extracted only from the shape of strokes, and it is still uncertain how efficient other on-line information, such as writing pressure or pen inclination, is for extracting personal features. Therefore, we propose an extraction method of personal features based on on-line handwriting information, including writing-pressure and pen-inclination information. In the proposed method, handwriting information is described by a set of three-dimensional curves, and personal features are described by a set of Fourier descriptors for the three-dimensional curves. We also discuss the reliability of the proposed method with some simulation results using handwritten data. From these simulation results, it is clear that the proposed method effectively extracts personal features from ordinary characters.

A new data-I/O scheme with a hidden writing-recovery architecture has been developed for the megabit-class high operating frequency SRAMs. Read-out nodes in the memory cell are separated from bitline-connected writing nodes so as not to delay sensing initiation due to uncompleted bitline recovery. The data stored in a memory cell are read-out by sensing the differential current signal on a double-rail virtual-GND line along bitlines. Each pair of virtual-GND lines is imaginarily short-circuited by a sense amplifier, so that the read-out circuitry would have large immunity against virtual-GND-line noises. The critical noise level associated with data destruction is analyzed at various supply voltages. The virtual-GND-line-sensed memory cell with the squashed topology, the swing-suppression-type low-power writing circuitry, and the current-sense amplifier with extra negative feedback loops, --which are used in the data-I/O scheme are also mentioned. Assuming a sub array in megabit-class SRAMs, 4 K-words 6 -bits test chip was fabricated with a 0.5-µm CMOS process. The SRAM achieved 180-MHz operation at a typical 3.3-V, 25 condition. The power dissipation at the practical operating frequency of 133-MHz was 50-mW.

Given two terms and their rewriting rules, an unreachability problem proves the non-existence of a reduction sequence from one term to another. This paper formalizes a method for solving unreachability problems by abstraction; i. e. , reducing an original concrete unreachability problem to a simpler abstract unreachability problem to prove the unreachability of the original concrete problem if the abstract unreachability is proved. The class of rewriting systems discussed in this paper is called β rewriting systems. The class of β rewriting systems includes very important systems such as semi-Thue systems and Petri Nets. Abstract rewriting systems are also a subclass of β rewriting systems. A β rewriting system is defined on axiomatically formulated base structures, called β structures, which are used to formalize the concepts of "contexts" and "replacement," which are common to many rewritten objects. Each domain underlying semi-Thue systems, Petri Nets, and other rewriting systems are formalized by a β structure. A concept of homomorphisms from a β structure (a concrete domain) to a β structure (an abstract domain) is introduced. A homomorphism theorem (Theorem1)is established for β rewriting systems, which states that concrete reachability implies abstract reachability. An unreachability theorem (Corollary1) is also proved for β rewriting systems. It is the contraposition of the homomorphism theorem, i. e. , it says that abstract unreachability implies concrete unreachability. The unreachability theorem is used to solve two unreachability problems: a coffee bean puzzle and a checker board puzzle.

Detecting security flaws is important in order to keep the database secure. A security flaw in object-oriented databases means that a user can infer the result of an unpermitted method only from permitted methods. Although a database management system enforces access control by an authorization, security flaws can occur under the authorization. The main aim of this paper is to show an efficient decision algorithm for detecting a security flaw under a given authorization. This problem is solvable in polynomial time in practical cases by reducing it to the congruence closure problem. This paper also mentions the problem of finding a maximal subset of a given authorization under which no security flaw exists.

Simplification orderings, like the recursive path ordering and the improved recursive decomposition ordering, are widely used for proving the termination property of term rewriting systems. The improved recursive decomposition ordering is known as the most powerful simplification ordering. Recently Jouannaud and Rubio extended the recursive path ordering to higher-order rewrite systems by introducing an ordering on type structure. In this paper we extend the improved recursive decomposition ordering for proving termination of higher-order rewrite systems. The key idea of our ordering is a new concept of pseudo-terminal occurrences.

Multi-lingual handwriting means the script written with more than one language. In this paper, a hierarchical hidden Markov model network-based approach is proposed for on-line recognition of multi-lingual cursive handwritings. Basic characters of language, language network, and intermixed use of language are modeled with hierarchical relations. Since recognition corresponds to finding an optimal path in such a network, recognition candidates of each language are combined with probability without special treatment. Character labels of handwriting, language modes, and segmentation are obtained simultaneously. However, several difficulties caused by multiple language occurred during recognition. Applied heuristic methods are Markov chain for language mode transitions, pairwise discrimination for confusing pairs, and constrained routines for side effects by language related preprocessing methods. In spite of the addition of other language, recognition accuracy of each language drops negligibly on experimental results of multi-lingual with Hangul, English, and Digit case.