|
1. |
PQL: Modal logic for compositional verification of concurrent programs |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 1-16
Naoshi Uchihira,
Preview
|
PDF (1031KB)
|
|
摘要:
AbstractThe temporal logic model checking method is very useful for verification of concurrent programs that can be expressed by finite state transition systems. However, a major drawback to using this method is that as the scale of the programs increases, the computation costs for verification increase exponentially. An effective solution for this problem is compositional verification. Compositional verification is a method in which the bisimulation equivalence of concurrent programs is used to extract from each construction element (subprocess) only that abstract information necessary to verify each query, thereby avoiding an explosion in cost.In this paper, PQL (Process Query Language) is proposed as an improved method in the solution of this problem. PQL is based on modal logic which is the union of temporal and process logic. Also in this paper, the compositional verification method is proposed by using PQL with consideration of the “divergence by internal transition
ISSN:0882-1666
DOI:10.1002/scj.4690250101
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
2. |
Parallel processing on the multi‐PSI computer and its evaluation — a programming paradigm based on a small‐grain highly concurrent object model |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 17-36
Kazuo Taki,
Nobuyuki Ichiyoshi,
Preview
|
PDF (1930KB)
|
|
摘要:
AbstractMulti‐PSI is a distributed‐memory MIMD (multiple‐instruction, multiple‐data) computer that has 64 processors. Problems of knowledge processing, which are the object of the Multi‐PSI, must be divided into many partial problems in order to achieve a favorable load balance because a characteristic of the computation is the dynamic loss of uniformity. This, however, has the danger of increasing the communication overhead. Therefore, in order to constrain the communication overhead and achieve a favorable load balance, in this paper, we propose a programming method oriented to the above problem. In this methodology, the problem is formulated as multiple communicating objects and the degrees of freedom in the load allocation are maintained. On the other hand, when the load is allocated, the communication objects are estimated from the system performance and the objects' characteristics, and the processing granularity is adjusted so that it is within the tolerance. This program methodology was applied to the three program developments of the shortest path problem, the LSI routing problem, and logic simulation; each was implemented with high efficiency. For example, in the shortest path program, 260,000 small‐grained objects were distributed over 64 processors and reached about 75% efficiency. In addition, in the logic simulation composed of 12,000 objects (gates), a high absolute efficiency of 99 thousand events/second and a 48‐fold increase in speed with 64 processors were obtained. Along with confirming the effectiveness of this programming methodology, these results demonstrated. that high efficiency can be realized in parallel processing for some degree of granularity even in a distributed‐memory pa
ISSN:0882-1666
DOI:10.1002/scj.4690250102
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
3. |
Predictor codebook for speaker‐independent speech recognition |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 37-46
Takeshi Kawabata,
Preview
|
PDF (752KB)
|
|
摘要:
AbstractThis paper discusses a method to handle the diversified dynamic features of speech by representing the dynamic features of speech by spectrum predictors and constructing the codebook containing predictors as the elements. The effectiveness of the method for speaker‐independent speech recognition is examined. Three kinds of predictor structures, i.e., the forward predictor, the backward predictor and the interpolator, are examined. The predictor codebook is constructed by the predictor quantization procedure, which is a small modification of the LBG algorithm. For the evaluation of the phoneme recognition level, two kinds statistical evaluation quantities and the phoneme recognition rate have been considered. It is seen as a result that the predictor codebook can realize a high phoneme separation capability and the robustness against the speaker variation. By combining the process actually into the phrase recognition system, the performance at the continuous speech recognition level is evaluated. In either case, the codebook with the backward predictor as the elements exhibited the highest performanc
ISSN:0882-1666
DOI:10.1002/scj.4690250103
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
4. |
Geometric reasoning with quantitative physical models |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 47-56
Yoshinori Okamota,
Preview
|
PDF (778KB)
|
|
摘要:
AbstractThis paper proposes a method of reasoning and of planning space and motion based on quantitative physical models.First, the particle‐collection representation (PCR) is proposed as a method of representing objects, and the robust simulation method of rigid‐body dynamics using PCR is discussed.Next, as a system which reasons and plans dynamic actions of rigid bodies based on this rigid‐body simulation, a planner (PCP) using physical simulation is proposed.For the planning method of PSP, the action improvement method is proposed which carries out a plan by gradually improving an original plan.To solve the problem of adjusting parameters for action in the action improvement method, the general parameter adjuster (GPA) is proposed. Moreover, the motion of bodies and carriage plannings by PSP are simulated. Furthermore, the robustness and extensibility of the PSP are investi
ISSN:0882-1666
DOI:10.1002/scj.4690250104
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
5. |
A speaker‐independent word recognition based on HMM using orthogonalized phonetic segment codebook |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 57-66
Hiroshi Matsuura,
Tsuneo Nitta,
Preview
|
PDF (832KB)
|
|
摘要:
AbstractMatrix quantization (MQ) is a method which directly quantizes the spectrum‐time pattern. However, it has a problem in that the quantization error is relatively large compared to the vector quantization (VQ), since the dimension is large and the pattern variation is less.From such a viewpoint, this paper introduces the acoustic/phonetic structure called phonetic segment as the unit of MQ. The statistical matrix quantization (SMQ) is applied to the calculation of the error measure, where the subspace method, i.e., a statistical pattern recognition technique, is employed. The purpose of SMQ is to consider effectively the pattern variation by constructing the Orthogonalized phonetic segment codebook based on the eigenvector set representing the pattern variation for each phonetic segment. The training of HMM using the phonetic segment code sequence also is considered.The K‐best learning is proposed, where from the first to theK‐th phonetic segment sequences are equally handled. Even though the K‐best learning is much simpler than VQ, it has equal or better output probability smoothing power, and can suppress the effect of the error in the conversion of the speech to the phonetic segment code sequence.Using the (SMQ/HMM + K‐best learning) method, a high speaker‐independent word recognition performance of 96.0 percent is obtained for the 100 word data set containing similar word pairs uttered by 10 unkno
ISSN:0882-1666
DOI:10.1002/scj.4690250105
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
6. |
A perfect separation of discrete sample points by four‐layered perceptron with localized representation |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 67-77
Takahumi Oohori,
Naoyuki Nagao,
Kazuhisa Watanabe,
Preview
|
PDF (847KB)
|
|
摘要:
AbstractThe distributed representation‐type three‐layered perceptron with backpropagation has such problems as the local minimum, long learning time, and ambiguity in internal representation. As a method to cope with those problems, this paper proposes the four‐layered perceptron, together with the learning algorithm, where a hidden layer is added, so that each discrete sample point can perfectly be represented by the corresponding output of the upper hidden layer.First, the learning algorithm of the perceptron is applied successively to the sample points, and the learning is executed so that the input sample points are separated perfectly by the piecewise sets of hyperplanes. In this mechanism, the output matrix of the lower bidder layer output is nonsingular. Consequently, the following four‐layered perceptron can be constructed, where the output matrix of the upper hidden layer is an identity matrix, and any discrete value can be produced as the output from the output layer by adjusting the network coefficients. Computational experiments are made for the realization of the three‐valued logic function, which is a learning problem on the two‐dimensional plane, as well as the pattern recognition problem by the representative sample points. As a result, it is shown that the learning converges in less than 1/100 computation time, compared to the three‐layered perceptron with the ba
ISSN:0882-1666
DOI:10.1002/scj.4690250106
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
7. |
Acceleration by prediction for error back‐propagation algorithm of neural network |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 78-87
Arihiro Kanda,
Satoshi Fujita,
Tadashi Ae,
Preview
|
PDF (686KB)
|
|
摘要:
AbstractThis paper proposes a speed improvement of the error back propagation algorithm, which is employed widely in the multilayered neural network, by introducing the prediction. The idea is to realize a larger acceleration by introducing the differential factor for the moment terms in the error back‐propagation algorith
ISSN:0882-1666
DOI:10.1002/scj.4690250107
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
8. |
Interactive 3‐dimensional segmentation method based on region growing method |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 88-97
Hiroyuki Sekiguchi,
Koichi Sano,
Tetsuo Yokoyama,
Preview
|
PDF (1111KB)
|
|
摘要:
AbstractIt has become easy to obtain three‐dimensional (3D) data of the inside of the human body because of developments in X‐ray computed tomography (CT) and magnetic resonance imaging (MRI). The 3D images of internal organs constructed from these data are useful in understanding the 3D shapes and positional relationships of the organs and are expected to be the diagnostic images of the next generation. However, many problems remain to be solved in making them practical, such as, improving the display speed of 3D images and implementing a 3D interface. For MRI, in particular, the difficulty in segmenting the display image is becoming a major impediment to the practical use of 3D MRI images. In this paper, we propose a practical segmentation method in which interactive corrective operations for 3D images are included in 3D region growing. To implement this method, we developed a 3D monitoring function for the segmentation process and an automatic function for removing the leaks generated during region growing. This method was applied to several 3D MRI data of the head and its effectiveness was confir
ISSN:0882-1666
DOI:10.1002/scj.4690250108
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
9. |
High speed display algorithm for 3D medical images using multilayer range image |
|
Systems and Computers in Japan,
Volume 25,
Issue 1,
1994,
Page 98-110
Hideyuki Ban,
Ryuuichi Suzuki,
Preview
|
PDF (1019KB)
|
|
摘要:
AbstractWe propose a high‐speed, three‐dimensional display method for objects represented by voxels intended for three‐dimensional image diagnostic systems that can be operated interactively. The method extends the concept of the conventional range image and introduces the multilayer range image that stores the distance from the projection plane to the object regardless of whether the object is visible or not. A range image is generated on the surface of any projection plane from the multilayer range images of 6 projection planes perpendicular to the coordinate axes and displayed in three dimensions after shading. Fast speeds are achieved by selecting the multilayer range images that correspond to the projection direction for processing and by eliminating operations on voxels which are not needed in the processing. We were able to display a 2563—voxel object on a 22 MIPS workstation in about 0.5 seconds. Moreover, we anticipate a response of less than one second on the next generation of 100 MIPS works
ISSN:0882-1666
DOI:10.1002/scj.4690250109
出版商:Wiley Subscription Services, Inc., A Wiley Company
年代:1994
数据来源: WILEY
|
|