Abstract:XYZ system is a software engineering system based on linear time temporal logic designed and implemented by the Institute of Software, The Chinese Academy of Sciences for one and a half decades. It has reached its last stage of development in application to solve some high technical engineering problems. In this paper, the goal, meaning, effect and applications of this system are introduced.

Abstract:This paper summarizes the research of mental state model for agent, which is a major subject in the research on multi-agent system. Most references are published after 1990. From different perspectives, covering informal analysis, formal models, architectures, cooperation researches, and applications, many important results are introduced in this paper, such as Bratman's analysis, Cohen and Levesque's intention model, Rao and Georgeff's BDI model, etc. Finally, some prosperous works are introduced as well. We hope that this presentation can help readers deepen their understanding of agent.

Abstract:Domain-specific frameworks have received considerable attention from researchers and developers and will become one of the future trends in object-oriented framework research area. In this paper, based on the deep understanding and analysis of the object-oriented application framework techniques, the existing problems in oil and gas exploration software are studied, and a specific framework for the interactive seismic processing application is proposed. Meanwhile, a set of design-pattern-oriented components are introduced so that the software extensibility and the code reusability are enhanced.

Abstract:Recent advances in computing and communication technologies have made VOD （video-on-demand） technically feasible and economically. The VOD system needs massive storage server because of the characteristic of the continuous media. Hierarchical storage is a good solution for the system under low cost. In this article, the authors first propose a hierarchical architecture model and the concept of disk cache, then develop a replacement algorithm based on access frequency by the model, finally analyse and simulate the algorithm. The results show that the algorithm avoids cache pollution problem in LFU (least frequently used) algorithm and well suits the applications of the continuous media data objects.

Abstract:The Petri net models of the clauses for logical inference using fixpoint are studied and the four-valued logic and the conflict transition concept are introduced. The authors can construct the Petri net models of non-Horn clauses based on the models of Horn clauses. Finding the fixpoint of logical values is one of the fundamental methods for logical inference. In this paper, an algorithm for the fixpoint based on the Petri net models of values is presented, and it is more efficient than the previous ones.

Abstract:Lacking an effective and feasible algorithm to compute the valid unimodular matrix for parallelizing of the outer loops, previous parallelizing researches can not automatically reveal the parallelism in such sequential nested-loops as have n-dimension distance matrix. In this paper, the authors discuss a general outer-loop parallelizing method by valid unimodular transformations, prove the existence of such a valid unimodular transformation, and suggest several practical computing algorithms through the constructive proofs. This discovered unimodular transformation can have the maximal number of parallelizable outer-loops transformed. Thus, the application scope of the algorithms can be enlarged to non-perfect or non-constant dependence distance loops.

Abstract:In this paper, on the basis of comparison of speaker verification and speaker identification, a novel speaker verification method is proposed. Compared to the conventional method, the speakerindependent speaker model is established to represent the universal feature of speech, and is used during the verification phase so that the decision threshold is adapted to different input speech and decided during verification phase. The difficulties of setting the decision threshold for the conventional method are al...

Abstract:According to Chinese speech feature, the authors can sum up the errors that consist in the Chinese characters sequence for continuous Chinese speech recognition, and write the lexical, syntactic and semantic rules for checking and confirming correction. Taking advantage of analysis method of Lexical Semantic Driven, the authors can check out the errors in Chinese characters sequence, then debug them. At last, correct Chinese characters sequence is obtained.

Abstract:A heterogeneous data integration system can integrate semistructured data which usually have large and changeable metadata, and generation of metadata is very time consuming. The metadata of Versatile are expressed in the form of templates. An incremental strategy for maintenance of templates is proposed, which can update the templates based on the changes (or delta in this paper) of the template rather than regeneration of all the templates from scratch. Different from deltas used for traditional incremental maintenance of materialized views,template deltas are able to describe the differences between not only the structures but also the behaviors of objects.It can express the differences between templates in virious data sources more easily.

Abstract:In this paper, a segmentation method is proposed, with which texture information is integrated. Based on this method, the authors design a subregionbased region growing algorithm and apply this method to medical image segmentation. This method is made use of gray and texture information, and the experiment results show that this method can produce good segmentation result when applied to certain images.

Abstract:The nature of the stock market data is briefly discussed first. It follows a brief discussion on the nature of the methodology of computational intelligence and their application perspectives for data mining. An experimental system for discovering the trend of market price changing and the prediction model from the stock exchange data records are proposed, in which, the training parameters of a neural network are optimized and defined by running the genetic algorithm along with the training procedure of the neural network.The ideas of design and the techniques of implementation are described in detail in this paper.Taking arbitrary the Shanghai First Department Store for case study,the experimental results are given finally.

Abstract:Flexible expressing mechanism is an important factor influencing system performance in contentbased retrieval, the simple mechanisms current systems employed can not express complex content queries. In this paper, an intermediate query expressing mechanismCbExpr is proposed. The mechanism first maps each content query to a similarity distribution function in feature space, then approximates this function using basic single feature queries. Basic thoughts and examples are given, also with implementation on Internet/Navigator platforms.

Abstract:In this paper, the authors study the relationship between the class of languages generated by grammars with production repetitions set and the class of adherence of languages, and prove that the class of adherence of contextfree languages is the proper subclass of contextfree languages and the class of adherence of regular languages is the proper subclass of regular languages. As a proper class of contextfree languagesthe class of linear languages, its adherence is the proper class of regular languages.

Abstract:In order to pick up the complementary benefits of formal and informal design methods,and overcome their shortcomings to ensure the quality and reliability of software design,an approach to the combination of formal methods and informal objectoriented design methodsHOOD is proposed in this paper. The design and implementation of a mechanical supported environment for the approach is also introduced. Based on the necessary improvement on HOOD, a hierarchical objectoriented design method, the approach integrates the Z notation and other formal specification techniques.The supported environment provides the users with the convenient and flexible tools for constructing graphics,syntax-directed editors of formal notations and text,and facilities of automatic verification.

Abstract:In this paper, a new improved exponential bidirectional associative memory (IeBAM) model is proposed. Its stability in synchronous and asynchronous updating modes of the states is proven by defining an energy function which is bounded and decreases as the states change. On one hand, IeBAM eliminates the unreasonable hypotheses in the stability proofs of both Wang's modified exponential BAM (MeBAM) and Jeng's exponential BAM (eBAM). On the other hand, it relaxes the continuity assumption of the BAM (bidirectional associative memory) and avoids the complement encoding problem. The theoretical analysis and computer simulations indicate that the IeBAM has higher storage capacity and better error-correcting capability than the MeBAM and the eBAM.

Abstract:With the construction and application of lots of large-scale internetworks, it becomes more and more important to manage these internetworks. Since the conventional centralized network management mode becomes less competent, a distributed network management architecture is proposed in this paper. The structure of a Web-based distributed network realtime monitoring system——WebRMonitor is discussed, and its key implementing techniques are given, such as the gathering, decentralized presentation of the realtime data and so on.

Abstract:A time-window based incremental technique for updating association rules is presented in this paper, which can not only re-use the results acquired in the previous discovery process, but also focus the discovery on the recent data set using time window.

Abstract:In the distributed system, all processes that depend on the process, which must be rolled back, have to be rolled back as well in order to keep the global state consistency. The dependency relation defined in the previous literature is too restrict. A new definition of dependency relation is proposed in this paper, and the influence of a process' rolling back can be reduced.

Abstract:In this paper, the search strategies in the acoustic layer of the CSR (continuous speech recognition) and the CDM (Chinese dictation machine) are addressed in two aspects, the acoustic recognition unit and the syntax-constrained word search tree. The SKB-FSS (statistical knowledge based frame synchronous search) algorithm and the syntax-constrained WST (word search tree) structure are proposed, they form the TLSN (two-level search network) in the acoustic layer. The statistical knowledge used by the algorithm includes differential state dwell distribution, the feature difference sum and so on, which result in an improvement of 36.6% in CSR. The principles of a modified back-off estimation algorithm and the search algorithms for the N-gram based language models are also introduced. Finally, by integrating the authors' techniques, a Chinese dictation machine engine (CDME) is implemented. A speaker-independent CDM text editor named ST97 and a voice command system named CMD97 are established for personal computers (PCs) based on the CDME.

Abstract:Introducing the type transformation functions between subtypes and supertypes, the definition of order-sorted algebra is generalized. According to this definition, a type needn't be a subset of its supertype, and a record model may form an order-sorted algebra. The concept of forest-order signature is introduced for describing single inheritance relation between types. A new meaning of equation is given. It is proved that an equational theory has its initial model.