A graphical notation for the propositional u-calculus, called modal graphs, is presented. It is shown that both the textual and equational presentations of the u-calculus can be translated into modal graphs. A model checking algorithm based on such graphs is proposed. The algorithm is truly local in the sense that it only generates the parts of the underlying search space which are necessary for the computation of the final result. The correctness of the algorithm is proven and its complexity analysed.

This paper introduces a new family of group key establishment protocols suitable for small or medium-sized groups. Five protocols are presented, using a semi-trusted server, with varying security service. The first one is a non-authenticated key agreement protocol suitable for applications with low security requirements. The second protocol adds an authenticated key agreement to provide collaborative authentication. The third and the fourth protocols provide key establishment with integrity and confirmation services, and the fifth protocol is the member adding protocol. A major advantage of the protocols is that they reduce the numbers of rounds from n to 5.

An epidemic model gives an efficient approach for transaction processing of replication systems in weakly connected environments. The approach has the advantages of high adaptation, support for low-bandwidth network, and committing updates in an entirely decentralized control fashion. But the previous implementing protocols, like ROWA protocol, quorum protocol, and voting protocol, have a common shortcoming that they are pessimistic in conflict reconciliation, therefore bring high transaction abort rate and reduce system performance dramatically when the workload scales up. In this paper, an optimistic voting protocol, which introduces condition vote and order vote in the voting process of transactions, is proposed. The condition vote and order vote postpone the final decision on conflicting transactions and avoid transaction aborts that are incurred by read-write and write-write conflicts. Experimental results indicate that the optimistic voting protocol decreases abort rate and improves average response time of transactions markedly when compared to other protocols.

This paper presents an automatic mesh generation procedure on a 2D domain based on a regular background grid. The idea is to devise a robust mesh generation scheme with equal emphasis on quality and efficiency. Instead of using a traditional regular rectangular grid, a mesh of equilateral triangles is employed to ensure triangular element of the best quality will be preserved in the interior of the domain. As for the boundary, it is to be generated by a node/segment insertion process. Nodes are inserted into the background mesh one by one following the sequence of the domain boundary. The local structure of the mesh is modified based on the Delaunay criterion with the introduction of each node. Those boundary segments, which are not produced in the phase of node insertion, will be recovered through a systematic element swap process. Two theorems will be presented and proved to set up the theoretical basic of the boundary recovery part. Examples will be presented to demonstrate the robustness and the quality of the mesh generated by the proposed technique.

This paper presents Xspace, a programmable coordination paradigm for Internet applications based on mobile agents. The Xspace system fully exploits the advantages of the XML language and Linda-like coordination. It supports XML documents as tuple fields and multiple matching routines implementing different relations among XML documents, including those given by XML query languages. The Xspace uses Java as the implementation language; it is based on object-oriented XMLized tuple spaces to implement a portable and programmable coordination paradigm for mobile agents. The design and implementation procedures of Xspace are described in this paper. Experiment and performance evaluation are also made. Finally, some conclusions and remarks are given.

Web hyperlink structure analysis algorithm plays a significant role in improving the precision of Web information retrieval. Current link algorithms employ iteration function to compute the Web resource weight. The major drawback of this approach is that every Web document has a fixed rank which is independent of the Web queries. This paper proposes an improved algorithm that ranks the quality and the relevance of a page according to the user query dynamically. The experiments show an improvement to the current link analysis algorithm.

The foundation of any network management systems is a database that contains information about the network resources relevant to the management tasks. A network information model is an abstraction of network resources, including both managed resources and managing resources. In the SNMP-based management framework, management information is defined almost exclusively from a "device" viewpoint, namely, managing a network is equivalent to managing a collection of individual nodes. Aiming at making use of recent advances in distributed computing and in object-oriented analysis and design, the Internet management architecture can also be based on the Open Distributed Processing Reference Model (RM-ODP). The purpose of this article is to provide an Internet Network Resource Information Model. First, a layered management information architecture will be discussed. Then the Internet network resource information model is presented. The information model is specified using Object-Z.

The researches on spelling correction aiming at detecting errors in texts tend to focus on context-sensitive spelling error correction, which is more difficult than traditional isolated-word error correction. A novel and efficient algorithm for the system of Chinese spelling error correction, CInsunSpell, is presented. In this system, the work of correction includes two parts: checking phase and correcting phase. At the first phase, a Trigram algorithm within one fixed-size window is designed to locate potential errors in local area. The second phase employs a new method of automatically and dynamically distributing weights among the characters in the confusion set as well as in the Bayesian language model. The tactics used above exhibits good performances.

Semi-input-memory finite automata, a kind of finite automata introduced by the author of this paper for studying error propagation, are a generalization of input-memory finite automata by appending an autonomous finite automaton component. This paper gives a characterization on the structure of weakly invertible semi-input-memory finite automata with delay 2 in which input alphabets and output alphabets have two elements and autonomous finite automata are cyclic. For the structure of feedforward inverse finite automata with delay 2, Zhu first gave a characterization; from a result on mutual invertibility of finite automata, the result mentioned above also leads to a different characterization on the structure of feedforward inverse finite automata with delay 2.

Grammar-based parsing is a prevalent method for natural language understanding (NLU) and has been introduced into dialogue systems for spoken language processing (SLP). A robust parsing scheme is proposed in this paper to overcome the notorious phenomena, such as garbage, ellipsis, word disordering, fragment, and ill-form, which frequently occur in spoken utterances. Keyword categories are used as terminal symbols, and the definition of grammar is extended by introducing three new rule types, by-passing, up-messing and over-crossing, in addition to the general rules called up-tying in this paper, and the use of semantic items simplifies the semantics extraction. The corresponding parser marionette, which is essentially a partial chart parser, is enhanced to parse the semantic grammar. The robust parsing scheme integrating the above methods has been adopted in an air traveling information service system called EasyFlight, and has achieved a high performance when used for parsing spontaneous speeches.

This paper introduces a kind of semantic computation and presents how to combine it into our Chinese Question-Answering (QA) system. Based on two kinds of language resources, Hownet and Cilin, we present an approach to computing the similarity and relevancy between words. Using these results, we can calculate the relevancy between two sentences and then get the optimal answer for the query in the system. The calculation adopts quantitative methods and can be incorporated into QA systems easily, avoiding some difficulties in conventional NLP (Natural Language Processing) problems. The experiments show that the results are satisfactory.

In this paper, the problem of checking a timed automaton for a Duration Calculus formula of the form Temporal Duration Property is addressed. It is shown that Temporal Duration Properties are in the class of discretisable real-time properties of Timed Automata, and an algorithm is given to solve the problem based on linear programming techniques and the depth-first search method in the integral region graph of the automaton. The complexity of the algorithm is in the same class as that of the solution of the reachability problem of timed automata.

A non-slicing approach, Corner Block List (CBL), has been presented recently. Since CBL only can represent floorplans without empty rooms, the algorithm based on CBL cannot get the optimum placement. In this paper, an extended corner block list, ECBLla, is proposed. It can represent non-slicing floorplan including empty rooms. Based on the optimum solution theorem of BSG (bounded-sliceline grid), it is proved that the solution space of ECBLn, where n is the number of blocks, contains the optimum block placement with the minimum area. A placement algorithm based on ECBLla, whose solution space can be controlled by setting la, the extending ratio, is completed. When la is set as n, the algorithm based on ECBLn is the optimum placement search algorithm. Experiments show that la has a reasonable constant range for building block layout problem, so the algorithm can translate an ECBLla representation to its corresponding placement in O(n) time. Experimental results on MCNC benchmarks show promising performance with 7% improvement in wire length and 2% decrease in dead space over algorithms based on CBL. Meanwhile, compared with other algorithms, the proposed algorithm can get better results with less runtime.

Interprocedural analysis and optimization are very important for compilers to exploit parallelism of modern high-performance computer systems. But it is very complicated, easy to make mistakes and difficult to maintain and port. To solve the problem, we construct an automatic generator of interprocedural analyzers and optimizers --- IGEN. In IGEN, first a new model to describe the interprocedural data-flow problem is designed. It is fit for all traditional data-flow problems and can be used in context-sensitive algorithms. Then, the structure and the working environment of IGEN are described in detail. Finally, the implementation of IGEN and our experimental result are given.

In this paper a new image representation for compressed domain image retrieval and an image retrieval system are presented. To represent images compactly and hierarchically, multiple features such as color and texture features directly extracted from DCT coefficients are structurally organized using vector quantization. To train the codebook, a new Minimum Description Length vector quantization algorithm is used and it automatically decides the number of code words. To compare two images using the proposed representation, a new efficient similarity measure is designed. The new method is applied to an image database with 1,005 pictures. The results demonstrate that the method is better than two typical histogram methods and two DCT-based image retrieval methods.

This paper presents a novel methodology for modelling and analyzing of behavior relations of concurrent systems. The set of all firing sequences of a Petri net is an important tool for describing the dynamic behavior of concurrent systems. In this paper, the behavior relativity of two concurrent subsystems in their synchronous composition is presented. Such behavior relativities, including Controlled Relativity, United Relativity, Interactive Relativity and Exclusive Relativity, are defined respectively. The properties of the relativities are discussed in detail. The analysis method for these properties is based on minimum T-invariants, when two subsystems are live bounded Petri nets. A well-known example has also been analyaed using the new methodology to demonstrate the advantages of the proposed methodology.

For most scheduling problems the set of machines is fixed initially and remains unchanged for the duration of the problem. Recently Imreh and Nogaproposed to add the concept of machine cost to scheduling problems and considered the so-called List Model problem. An online algorithm with a competitive ratio 1.618 was given while the lower bound is 4/3. In this paper, two different semi-online versions of this problem are studied. In the first case, it is assumed that the processing time of the largest job is known a priori. A semi-online algorithm is presented with the competitive ratio at most 1.5309 while the lower bound is 4/3. In the second case, it is assumed that the total processing time of all jobs is known in advance. A semi-online algorithm is presented with the competitive ratio at most 1.414 while the lower bound is 1.161. It is shown that the additional partial available information about the jobs leads to the possibility of constructing a schedule with a smaller competitive ratio than that of online algorithms.

In this paper we propose a novel scheme for scheduling divisible task on parallel processors connected by system interconnection network with arbitrary topology. The divisible task is a computation that can be divided into arbitrary independent subtasks solved in parallel. Our model takes into consideration communication initial time and communication delays between processors. Moreover, by constructing the corresponding Network Spanning Tree (NST) for a network, our scheme can be applied to all kinds of network topologies. We present the concept of Balanced Task Distribution Tree and use it to design the Equation Set Creation Algorithm in which the set of linear equations is created by traversing the NST in post-order. After solving the created equations, we get the optimal task assignment scheme. Experiments confirm the applicability of our scheme in real-life situations.

Retiming is a technique for optimizing sequential circuits. In this paper, we discuss this problem and propose an improved retiming algorithm based on variables bounding. Through the computation of the lower and upper bounds on variables, the algorithm can significantly reduce the number of constraints and speed up the execution of retiming. Furthermore, the elements of matrixes D and W are computed in a demand-driven way, which can reduce the capacity of memory. It is shown through the experimental results on ISCAS89 benchmarks that our algorithm is very effective for large-scale sequential circuits.

XML (eXtensible Markup Language) is a standard which is widely applied in data representation and data exchange. However, as an important concept of XML, DTD (Document Type Definition) is not taken full advantage in current applications. In this paper, a new method for clustering DTDs is presented, and it can be used in XML document clustering. The two-level method clusters the elements in DTDs and clusters DTDs separately. Element clustering forms the first level and provides element clusters, which are the generalization of relevant elements. DTD clustering utilizes the generalized information and forms the second level in the whole clustering process. The two-level method has the following advantages: 1) It takes into consideration both the content and the structure within DTDs; 2) The generalized information about elements is more useful than the separated words in the vector model; 3) The two-level method facilitates the searching of outliers. The experiments show that this method is able to categorize the relevant DTDs effectively.

In secure multicast communication, packet source authentication is a bottleneck problem due to the dynamic property of the multicast group, unreliability of data transmission and the large number of data packets. This paper proposes a novel authentication scheme called B-MSAS (Balance Multicast Source Authentication Scheme) that can be used to solve this problem, in which a new message authentication technique is introduced. This scheme dramatically reduces the signature size overhead and raises the signature rate. It provides the non-repudiation service, high loss resistance, and can easily be scaled up to potentially millions of receivers, and hence has a sweeping applicability. It should have applications to many practical problems.

In order to decrease crimes such as money laundering, blackmailing etc. in electronic cash systems, fair electronic cash has been a major focus of academic research in electronic commence. When a bank finds some dubious cash or owner, the trusted entity or trustee can help him to revoke the anonymity of the cash. In the previous protocols, the trustee knows all the information of the cash whether he is trusted or not, that is, he can trace the user or cash unconditionally. Furthermore, the dishonest trustee may deceive a user, which means that he may withdraw cash while tracing other users. Such cases are unfair to the honest users.

In the implementation of hyperelliptic curve cryptosystems, a siginificant step is the selection of secure hyperelliptic curves on which the Jacobian is constructed. In this paper, we discuss the hyperelliptic curves of g=2 such as v^2+uv=f and v^2+v=f(u) defined on GF(2^r). The curves defined on GF(4) and GF(8) are expanded to the curves defined on GF(4)^k and GF(8)^t respectively, where 38 Related Articles | Metrics

The concept of aqueous computing is presented here, first in full generality, and afterward, using an implementation in a specific enzymatic technology. Aqueous computing arose in the context of biomolecular (DNA) computing, but the concept is independent of the specifics of its biochemical origin. Alternate technologies for realizing aqueous computing are being considered for future implementation. A solution of an instance of the Boolean satisfiability problem, (SAT), is reported here that provides a new example of an aqueous computation that has been carried out successfully. This small instance of the SAT problem is sufficiently complex to allow our current enzymatic technology to be illustrated in detail. The reader is invited to participate in the rich interdisciplinary activity required by wet lab computing. A project is suggested to the reader for determining the three-colorings of a graph. The basic operations required for this project are exhibited in the solution of the SAT example reported here.

In this paper we present an algorithm with a new trace-terminating condition for tracing along surface-surface intersection curves on surface boundaries, while several tracing methods and embedding methods that include tracing scheme may cause false termination with a traditional trace-terminating condition: tracing stops when the surface-domain's boundary is reached. And we also suggest another iterative method to calculate intersection points on surface boundaries with parallel surface normal. Some numerical examples with these two ideas and comparisons to `DESIGNBASE', `ACIS', and `Parasolid' are included to demonstrate the effectiveness of our algorithm.

Strongly inspired by the research on physics-based dynamic models for surfaces, we propose a new method for precisely evaluating the dynamic parameters (mass, damping and stiffness matrices, and dynamic forces) for Loop surfaces without recursive subdivision regardless of regular or irregular faces. It is shown that the thin-plate-energy of Loop surfaces can be evaluated precisely and efficiently, even though there are extraordinary points in the initial meshes, unlike the previous dynamic Loop surface scheme. Hence, the new method presented for Loop surfaces is much more efficient than the previous schemes.

A new method is presented for tracking a person's head in real-time. The head is shaped as an ellipse, and the adaptively modified RGB color histogram is used to represent the tracked object (head). The method is composed of two parts. First, a robust nonparametric technique, called mean shift algorithm, is adopted for histogram matching to estimate the head's location in the current frame. Second, a local search is performed after histogram matching to maximize the normalized gradient magnitude around the boundary of the elliptical head, so that a more accurate location and the best scale size of the head can be obtained. The method is demonstrated to be a real-time tracker and robust to clutter, scale variation, occlusion, rotation and camera motion, for several test sequences.

This paper presents a built-in self-test (BIST) scheme for detecting all robustly testable multiple stuck-open faults confined to any single complex cell of a CMOS circuit. The test pattern generator (TPG) generates all n.2^n single-input-change (SIC) ordered test pairs for an n-input circuit-under-test (CUT) contained in a sequence of length 2n\.2^n. The proposed design is universal, i.e., independent of the structure and functionality of the CUT. A counter that counts the number of alternate transitions at the output of the CUT, is used as a signature analyzer (SA). The design of TPG and SA is simple and no special design- or synthesis-for-testability techniques and/or additional control lines are needed.

In this paper, a solution to the Problem of Malicious Hosts, named SPMH, is suggested. At first, Mobile Agent Blackbox Construction Method based on Loureiro's Protocol (MABCM-LP) is suggested to convert a mobile agent into a Mobile Agent Blackbox (MAB) which makes the mobile agent difficult to be understood and tampered by malicious hosts. At the same time, a Protocol Tracing the Inputs/outputs and Results (PTIR) is developed to trace the mobile agent running at a host, which can be used to detect and prove the attacks by malicious hosts. It is proved that this solution is secure, correct, and robust. It is found firstly that the detection method and the prevention method are complementary to each other, and this is the first solution that integrated both of these two methods too.

The need to improve software productivity and software quality has put forward the research on software metrics technology and the development of software metrics tool to support related activities. To support object-oriented software metrics practice effectively, a model-based approach to object-oriented software metrics is proposed in this paper. This approach guides the metrics users to adopt the quality metrics model to measure the object-oriented software products. The development of the model can be achieved by using a top-down approach. This approach explicitly proposes the conception of absolute normalization computation and relative normalization computation for a metrics model. Moreover, a generic software metrics tool --- Jade Bird Object-Oriented Metrics Tool (JBOOMT) is designed to implement this approach. The parser-based approach adopted by the tool makes the information of the source program accurate and complete for measurement. It supports various customizable hierarchical metrics models and provides a flexible user interface for users to manipulate the models. It also supports absolute and relative normalization mechanisms in different situations.

In high-level synthesis of VLSI circuits, good lower bound prediction can efficiently narrow down the large space of possible designs. Previous approaches predict the lower bound by relaxing or even ignoring the precedence constraints of the data flow graph (DFG), and result in inaccuracy of the lower bound. The loop folding and conditional branch were also not considered. In this paper, a new stepwise refinement algorithm is proposed, which takes consideration of precedence constraints of the DFG to estimate the lower bound of hardware resources under time constraints. Processing techniques to handle multi-cycle, chaining, pipelining, as well as loop folding and mutual exclusion among conditional branches are also incorporated in the algorithm. Experimental results show that the algorithm can produce a very tight and close to optimal lower bound in reasonable computation time.