摘要:

AbstractA verification system of asynchronous real‐time software including timing constraints, which supports both model‐checking algorithms and language inclusion algorithms, does not exist. In a language inclusion algorithm, verification specification is described by a timed automaton from the standpoint of both states and behaviors. On the other hand, in a model‐checking algorithm, verification specification is described by real‐time temporal logic from the standpoint of state relation. It is necessary to specify verification property by both timed automaton and real‐time temporal logic. A hybrid verification method, which supports both verification methods, is proposed here. In order to realize it, a timed Kripke structure is generated from timed automaton through an augmented region graph. The method is shown to be effective using the example of a cloc

ISSN:0882-1666    

DOI:10.1002/scj.4690270501

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractBoth predictable interprocessor synchronization and fast interrupt response are required for real‐time systems constructed using asymmetric shared‐memory multiprocessors. This paper points out that conventional spin lock algorithms cannot satisfy both requirements at the same time and describes two spin lock algorithms that have been proposed to solve this problem. These algorithms, extensions of queuing spin locks modified to be preemptable for servicing interrupts, can give upper bounds on the times to acquire and release an interprocessor lock while achieving a fast response to interrupt requests. The performance measurement of the algorithms demonstrates that the algorithms have required properties. To apply the algorithms to real‐time kernels, we also propose an extended algorithm, which is a combination of the two algor

ISSN:0882-1666    

DOI:10.1002/scj.4690270502

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractIn this paper, new methods for providing the correctness of refinement among abstract sequential machine style programs are described. The programs are described in algebraic language ASL using some useful notions, i.e., the extended projection and the valid reachability condition for each transition function. These notions allow a designer to refine a given text (program or specification) to a concrete text more freely than the text that does not use such notions. These notions can also enhance the expressive power of the text.On the other hand, these advantages would have lost half their values, if useful methods to prove the correctness of refinement among the texts using them are not found. Thus new methods for proving the correctness of the texts are proposed, and they do not require much proof loads.First the correctness of refinement among the ASL texts with the extended projection is defined. Second, a method is proposed for proving the correctness of refinement among such texts. Also proposed is a definition of the correctness of refinement among the texts with the valid reachability conditions and a method to prove their correctness. These methods do not require more proof loads than the usual methods for the texts that do not use such notions in the abstract sequential machine style. Therefore, these methods are useful.

ISSN:0882-1666    

DOI:10.1002/scj.4690270503

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractTwo‐phase quasi‐delay‐insensitive circuits control the data‐paths by alternating the working‐phase and idle‐phase. Although the use of Martin's Q‐element simplifies the design of such circuits, sequential execution of idle‐phases, which consume as much time as working‐phases, prevents high‐speed circuit operation. The auto‐sweeping module (ASM) proposed here allows parallel execution of an idle‐phase with the working‐phase of the next stage. A few extra circuits are inserted in order to use ASM for every micro‐operation. A simulation study shows that ASM accelerates the average speed of a multiplier by 58 percent without any increase i

ISSN:0882-1666    

DOI:10.1002/scj.4690270504

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractWhen patterns are stored by using associative learning in a chaotic neural network consisting of chaotic neurons that easily produces chaos, whether dynamic (chaotic) or static (non‐chaotic) remembering occurs can be controlled by varying the parameters of the chaotic neurons. A pattern can be searched by using this dynamic remembering as a sampling procedure. If features of the output pattern of the network become similar to desired features during the search, the chaotic state is changed to a static remembering state so that the output pattern has desired features. In this paper, the state is controlled by using a model of presynaptic inhibition similar to that seen in real nerve cells (not using the parameters of the chaotic neurons). Extraction and comparison of the features are performed by back‐propagation networks. The extraction of features under this method is amenable to visual representation of its trajectory in feature sp

ISSN:0882-1666    

DOI:10.1002/scj.4690270505

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractThe neural chips to speed up the process of a neural network have recently been developed actively. Since a conventional neural chip requires quantized synaptic weights, it is important to know the properties of the network with such weights. Devices for a 2‐layer network with the same number of input and output elements have been well developed, and such a device can be used as an autocorrelation associative memory by feeding its output to its input.This paper investigates theoretically the capacity of an autocorrelation associative memory when its synaptic weights are quantized with a finite number of bits. It also proposes an optimum quantization function. A system with a finite number of elements is computer simulated. The proposed method can be applied to the design of a neural chip for associative memor

ISSN:0882-1666    

DOI:10.1002/scj.4690270506

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractThis paper describes an investigation into the effectiveness of a lookahead model based on recurrent neural networks. An action network and an internal model of the environment are incorporated into the recurrent neural network; lookahead planning is performed while configuring the action network through learning in the internal model.A genetic algorithm is applied to the design of the neural networks. The effectiveness of this model is evaluated by applying it to the game of “tic‐tac‐toe,” and the following result is obtained. It is possibly more effective to perform learning in the internal model by learning algorithms than by memorizing input‐output corres

ISSN:0882-1666    

DOI:10.1002/scj.4690270507

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractThis paper intends to solve problems in the BP learning in the conventional multilayered perceptron, and proposes two methods, the local generalization and the global generalization, improve the generalization ability of the perceptron with the localized representation. In the local generalization, the generalization learning is executed so that the generalization ability function based on the distance between the separating partial hyperplanes and the set of patterns for learning, is maximized under the given order of separation in the learning. A problem then is that the range of adjustment for the separating partial hyperplane is limited depending on the order of separations, which prevents the improvement of the generalization ability.In the global generalization, the generalization ability function is defined considering the order of category separation and the optimal separating partial hyperplanes are determined simultaneously to maximize the function.Simulation experiments are carried out for the learning task on the two‐dimensional plane and the recognition task for the handwritten Chinese characters. It is seen that the generalization ability is improved greatly. It is seen that the local generalization can realize nearly the same generalization ability, and the global generalization can realize a better generalization ability, compared to the BP learnin

ISSN:0882-1666    

DOI:10.1002/scj.4690270508

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractThis paper considers the regularization theory based on the general regression. The general regression does not require the measure for the smoothness, which plays the important role in the standard regularization theory or its extension. The theory is extended so that the regularization can be applied to the case where the data are multivalued. Based on the extended theory, an algorithm is derived which can reconstruct in a deterministic way the discontinuous function from the discrete data, without requiring the conventional line process, by regarding the discontinuity as a boundary between different functions. The effectiveness of the derived algorithm and the robustness against the noise are demonstrated by a computer simulation.

ISSN:0882-1666    

DOI:10.1002/scj.4690270509

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY

摘要:

AbstractThe problem in which the input signal sequence is segmented into multiple signal sources and the signal source is estimated appear in a wide range of problems, such as speech information processing and language processing.In this paper, this kind of problem is called the unknown‐multiple signal source clustering problem, and a solution method is proposed based on the ergodic HMM. In ergodic HMM, the state corresponds to the signal source and the symbol sequence output from the state corresponds to the signal sequence. Then, using the Viterbi decoding and the forward decoding, the segmentation point and the category can simultaneously be estimated. As an application of the problem, the classification of the utterances by multiple speakers is attempted. As a result of the experiment, it is shown that the initial parameter values are important in the ergodic HMM, and the LPC cepstrum with a long‐term window is useful as the feature vector reflecting the speaker individual

ISSN:0882-1666    

DOI:10.1002/scj.4690270510

出版商:Wiley Subscription Services, Inc., A Wiley Company    

年代:1996

数据来源: WILEY