In this paper, we discuss an abstraction method for Petri nets based on an equivalence of firing sequences of a specified subnet or a specified subset of transitions. Specifically, a method is presented to generate an equivalent net which preserves firing sequences of a specified subnet or a specified subset of transitions. The abstraction can be applied to an efficient behavioral analysis of concurrent systems constructed by composition of modules such as communication networks and Flexible Manufacturing Systems (FMS).

This paper proposes a protocol verification tool where protocols are described in an extended Petri net and Horn clauses. The extended net model contributes to reduce state space in verification with hierarchical description. The model also includes timed and colored net. Horn clause enables protocol designers to grasp a protocol by the declarative semantics. They can describe non critical but mandatory portion of a protocol like error processing or abortion with Horn clauses. Protocols are verified through simulation. Protocol verification includes two methods, all-in-one and hierarchical methods. By the all-in-one method all description is translated into Prolong clause and simulated exhaustively, whereas by the hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the net model. Then the layer is replaced by a simpler net model that is incorporated into the higher layer. The scheme is applied to an illustrative example of the Alternating Bit protocol to discuss its effectiveness.

Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. We have proposed a new flexible description methodology, which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. We have also shown that function requirements can be modeled by a Logical Petri Net (LPN), which is a kind of extended Petri Nets, in order to derive the formal specification. In this paper, we propose a verification method of system requirements that contain some kinds of logical errors. Further, we show a method to decompose and refine a requirement description hierarchically, and discuss how to derive a formal specification from a requirement description flexibly along our refinement method against the changes of the requirement description in the system.

The symbolic model checking algorithm was proposed for the efficient verification of sequential circuits. In this paper, we show that this algorithm is applicable to the verification of concurrent systems described by finite capacity Petri nets. In this algorithm, specifications of the system are given in the form of temporal logic formulas, and the algorithm checks whether these formulas hold in the state space. All logical operations are performed on Binary Decision Diagrams. Since the algorithm does not enumerating each state, the problem of state space explosion can be avoided in many cases.

This paper proposed a practical method of program validation for state-based reactive concurrent systems. The proposed method is of particular relevance to plant control systems. Plant control systems can be represented by extended state transition systems (e.g., communicating asynchronous transition systems). Our validation method is based on state space analysis. Since naive state space analysis causes the state explosion problem, techniques to ease state explosion are necessary. One of the most promising techniques is the partial order method. However, these techniques usually require some structural assumptions and they are not always effective for actual control systems. Therefore, we claim integration and harmonization of verification (i.e., state space analysis based on the partial order method) and simulation (i.e., conventional validation technique). In the proposed method, verification is modeled as exhaustive simulation over the state space, and two types of simulation management techniques are introduced. One is logical selection (pruning) based on the partial order method. The other is heuristic selection based on priority (a priori precedence) specified by the user. In order to harmonize verification (logical selection) and conventional simulation (heuristic selection), we propose a new logical selection mechanism (the default priority method). The default priority method which prunes redundant state generation based on default priority is in harmony with heuristic selection based on the user's priority. We have implemented a practical validation tool, Simulation And Verification Environment for Reactive Concurrent Systems (SAVE/RCS), and applied it to chemical plant control systems.

Rewriting logic has been proposed as a unified model of parallel and concurrent computation, especially concurrent object-oriented computation and agent oriented computation. In this paper, we present a category-theoretic technique in which simulation relation between concurrent processes described by rewriting logic is analyzed. In this technique, simulation relation is represented by morphisms in the category of concurrent processes. Moreover, this technique is shown to be applicable to Petri nets by modeling them by rewriting logic. By this method, it is acknowledged that our technique is applicable to Petri nets including multi-loops whose treatment is limited in other techniques.

In this paper, an approach to derive a logic function of asynchronous circuits from a graph-based model called Signal Transition Graphs (STG) is discussed. STG's are Petri nets, whose transitions are interpreted as a signal transition on the circuit inputs or gate outputs, and its marking represents a binary state of the circuit. STG's can represent a behavior of circuit, to derive logic functions, however, the reachability graph should be constructed. In the verification of STG's some method based on Occurrence nets (OCN) and its prefix, called unfolding, has been proposed. OCN's can represent both causality and concurrency between two nodes by net structure. In this paper, we propose a method to derive a logic function by generating substate space of a given STG using the structural properties of OCN. The proposed method can be seem as a parallel algorithm for deriving a logic function.

This paper proposes a hardware architecture of programmable controller based on Petri nets. The suggested architecture achieves sufficiently rapid processing even as demands on PCs become increasingly more complex. The architecture's speed and efficiency are derived from an automatic and dynamic super scalar computing capability that executes bit instructions and data handling instructions simultaneously without preprocessing, due to the properties of Petri nets. Specific characteristics for both architectural memory-based implementation of Petri nets and evolution algorithms are suggested and classified by the net structure. Analysis of the suggested architectures and effects on performance are also given with mathematical formulas and a computer simulation.

In this paper, an analysis of a slotted ring type network, the Pierce type ring network, is carried out and characteristics of the ring are derived. The ring type network is one of the fundamental computer network topologies. It is easy to implement and has many merits such as low cost and expansion flexibility. However, possible hogging, or domination of slots by one station, is one of its drawbacks. At first, when we regard vacant slots as usable, we show how system performance is fairly dependent on traffic patterns. We also show quantitatively that when slots are fixed to each station, domination of the ring can be completely prevented, although the performance of the system will be reduced. We propose a method to control the transmission of packets in which we have positively adopted the insertion of shift registers into the transmission line to prevent the deterioration of the performance. With the insertion of shift registers, we show the feasibility of improving the performance of the fixed slot allocation method at the same time as preventing domination of the ring. We will discuss the merits of the shift register insertion method, which is introduced to improve the fixed slot and semi-fixed slot allocation methods. In the slotted ring type system, four types of slot allocation method including a register insertion method are considered for the improvement of the system performance. The merits and demerits of the methods are discussed. We show how system performance depends on the traffic patterns considered. We analyse the characteristics of the ring system under various conditions.

This paper describes a simulation technique of start-up characteristics that considers a nonlinearity of the drive level of quartz crystal resonators. A nonlinear resonator model for SPICE where the resonant resistance varies with the voltage added to a resonator is proposed. In an examination using a transistor Colpitts oscillator, the simulation using this technique agreed with the experimental results very well.

A fully-differential switched-current (SI) circuit provided with clock-feedthrough (CFT) and common mode rejection and offset compensation schemes is described. Different from a conventional SI memory cell, it takes the difference between two differential inputs to deliver the balanced differential currents. Transistor level simulations and error analyses are given to demonstrate its performance.

A 2-switch node network is one of the most fundamental structure among communication nets such as telephone networks and local area networks etc. In this letter, we prove that a problem of designing a 2-switch node network satisfying capacity conditions of switch nodes and their link, which we call 2-switch node network problem, is NP-complete.

Two method to predict targets which a user is about to point with a mouse on the basis of the trajectory of the mouse cursor were proposed. The effects of the interval between targets, the position of targets, the sampling interval and the number of sampling on the pointing time and the prediction accuracy were investigated. In both methods, the distance between targets had little effects on the pointing time. The prediction accuracy was found to be affected by the position of targets. In both prediction methods, the angle between the cursor movement vector and the vector which connects the current cursor position and the center of each target is calculated every st. As for Prediction Method1 that regards the target which correspond to the minimum angle continuously 5 times as the candidate target, the optimal condition of the sampling interval was found to be 0.06 sec or 0.08 sec. Concerning Prediction Method2 that calculates the angle n times and determines the minimum cumulative value as the candidate, the optimal condition of the number of sampling was 8.

This paper discusses a coding-based selection approach to a communication aid for the severely motor disabled. Several approaches including row-column scanning are briefly described, then we propose a new selection scheme based on the theory of adaptive coding. They are compared each other with respect to average switch activations in generating some text samples.

In this paper, electromagnetic scattering by infinite double two-dimensional periodic array of resistive upper and lower elements is considered. The electric field equations are solved by using the moment method in the spectral domain. Some numerical results are shown and frequency selective properties are discussed.

Recently, some speech recognition methods using fusion of visual and auditory information have been researched. In this paper, a study on the mouth shape image suitable for fusion of visual and auditory information has been described. Features of mouth shape which are extracted from gray level image and binary image are adopted, and speech recognition using linear combination method has been performed. From results of speech recognition, the studies on the mouth shape features which are effective in fusion of visual and auditory information have been performed. And the effectiveness of using two kinds of mouth shape features also has been confirmed.

This paper discusses the reliability of the Modified EBU method compared with the EBU and DSCQS methods where the small and different levels of impairments exist in the coded HDTV sequences. The subjective evaluation tests are carried out in the full and limited impairment ranges. And it is shown that the Modified EBU method is most reliable for both ranges.

An interactive painting system for generating calligraphy words is developed. Its significant advantage lies in effective rendering functions that synthesize kasure and nijimi textures due to the effects of brush and absorbent painting paper. The system enables users to generate high quality and realistic calligraphy words.

We investigated perceptual color assimilation of a strip (test field) displayed on a CRT close to a green or red strip (inducing field) with a dark background. The maximal distance to induce assimilation was about 7 for a red inducing field, and 24 for a blue one. The intensity of assimilation was almost inversely proportional to the width of test field.

This paper describes a new intelligent computer assisted instruction (ICAI) system for Japanese beginners to learn Korean composition. This system is supported by speech synthesis which is generated by a new method for arbitrary sentences of Japanese and Korean using the natural speech data-base.

Conventional subband ADF's (adaptive digital filters) using filter banks have shown a degradation in performance because of the non-ideal nature of filters. To solve this problem, we propose a new type of subband ADF incorporating two types of analysis filter bank. In this paper, we show that we can design the optimum filter bank which minimizes the LMSE (least mean squared error). In other words, we can design a subband ADF with less MSE than that of conventional subband ADF's.

A fast pitch search algorithm using the skipping technique is proposed to reduce the computation time in CELP vocoder. Based on the characteristics of the correlation function of speech signal, the proposed algorithm skips over certain ranges in the full pitch search range in a simple way. Though the search range is reduced, high speech quality can be maintained since those lags having high correlation values are not skipped over and are used for search by closed-loop analysis. To improve the efficiency of the proposed method, we develop three variants of the skipping technique. The experimental results show that the proposed and the modified algorithm can reduce the computation time in the pitch search considerably, over 60% reduction compared with the traditional full search method.

Single-reference and multi-reference noise canceller (SRNC and MRNC) performances are investigated based on correlation between signal and noise. Exact relations between these noise canceller performances and signal-noise correlation have not been well discussed yet. In this paper, the above relations are investigated based on theoretical, analysis and computer simulation. The normalized LMS (NLMS) algorithm is employed. Uncorrelate, partially correlated, and correlated signal and noise combinations are taken into account. Computer simulation is carried out, using real speech, white noise, real noise sound, sine wave signals, and their combinations. In the SRNC problem, spectral analysis is applied to derive the canceller output power spectrum. From the simulation results, it is proven that the SRNC performance is inversely proportional to the signal-noise correlation as expected by the theoretical analysis. From the simulation results, the MRNC performance is more sensitive to the signal-noise correlation than that of SRNC. When the signal-noise correlation is high, by using a larger number of adaptive filter taps, the noise is reduced more, and, the signal distortion is increased. This means the signal components included in the noise are canceled exactly.

The disturbance-rejection problem is to find a feedback control law for linear control systems such that the influence of disturbances is completely rejected from the output. In 1970 Wonham and Morse first studied this problem in the framework of the so-called geometric approach. On the other hand, in 1985 Ghosh studied parameter insensitive disturbance-rejection problems with state feedback and with dynamic compensator. In this paper we study the parameter insensitive disturbance-rejection problem with static incomplete-state feedback for linear multivariable systems in the framework of the geometric approach from the mathematical point of view. Necessary conditions and/or sufficient conditions for this problem to be solvable are presented. Finally an illustrative example is presented.

Genetic Algorithm (GA) is the method of approaching optimization problem by modeling and simulating the biological evolution. As the genetic algorithm is rather time consuming, the use of a parallel genetic algorithm can be advantage. This paper describes new methods for fine-grained parallel genetic algorithm using a multiprocessor system FIN. FIN has a VLSI-oriented interconnection network, and is constructed from a viewpoint of fractal geometry so that self-similarity is considered in its configuration. The performance of the proposed methods on the Traveling Salesman Problem (TSP), which is an NP-hard problem in the field of combinatorial optimization, is compared to that of the simple genetic algorithm and the traditional fine-grained parallel genetic algorithm. The results indicate that the proposed methods yield improvement to find better solutions of the TSP.

A graph G = (V, E) with N nodes is called an N-hyper-ring if V = {0, ..., N-1} and E = {(u, v)(u-v) modulo N is power of 2}. We study embeddings of the 2ⁿ-hyper-ring in the n-dimensional hypercube. We first show a greedy embedding with dilation 2 and congestion n+1. We next modify the greedy embedding, and then we obtain an embedding with dilation 4 and congestion 6.