Abstract:This paper optimizes the encoding of verifying G(p) and G(p→F(q)) which are two important and frequently used modal operators in optimization of encoding for bounded model checking (BMC). Through analysis of the properties of finite state machine (FSM) and LTL (linear-time temporal logic) when verifying these modal operators, it presents a concise recursive formula, which can efficiently translate BMC instances into SAT (satisfiability) instances. The logical properties of these recursion formulas are verified. The experimental comparison between the optimization of BMC and the other two important methods AA_BMC and Timo_BMC for solving these modal operators in BMC shows that the former is superior to the latter in both the scale of instances and the difficulty to solve the problem. Research of this paper is also beneficial to encoding optimization of verifying other modal operators in BMC.

Abstract:To make symbolic model checking approach applicable to all ω-regular properties, this paper studies symbolic model checking for ETL (extended temporal logic). First, the Tableau approach for LTL (linear temporal logic) is extended to that of ETL, and then the BDD (binary decision diagram)-based encodings of this technique is given. Moreover, the model checking tool ENuSMV is implemented based on NuSMV, which allows users to customize temporal connectives, and hence all ω-regular properties can be verified. Experimental results show that ETL can also be efficiently verified by the symbolic approach.

Abstract:This paper discusses the use of intuitionistic linear-time μ-calculus (IμTL) whose underlying model is based on Heyting algebra of prefixed closed sets as the basis for the specification of assumption and guarantee paradigm, and then propose an assumption-guarantee rule in IμTL. The rule formulated is more general then previously proposed rules that used linear-time temporal logic (LTL) in the specification of assumption and guarantee paradigm and extends the discussion for safety properties of the form “always φ”, and therefore represents more uniform reasoning of assumption and guarantee specifications for also supporting circular compositional reasoning.

Abstract:This paper presents a technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic. The technique realized as a tool called APL is implemented. The APL theoremprover is fully automated with which proofs can be recorded and checked efficiently. The tool is tested on pointerprograms mainly about singly-linked lists, doubly-linked lists and binary trees.

Abstract:This paper introduces the verification theory of separation logic, characteristics of separation logic, and some successful applications of separation logic. Researches on separation logic to support program verification are analyzed, including the properties of separation logic, its relation to other logics, its support to programming languages and design patterns, and the theorem provers’ support to separation logic. The problems encountered when separation logic is applied more widely are pointed out, and the future research directions are discussed.

Abstract:Consumers need to make prediction on the quality of unused Web services before selecting. Usually, this prediction is made based on other consumers’ experiences. Being aware of different QoS (quality of service) experiences of consumers, this paper proposes a QoS prediction approach. This approach makes similarity mining among consumers and QoS data, and then predicts the QoS of the unused Web services from other consumers’ experiences. Experimental results show that with this approach the preciseness of QoS prediction for Web services can be improved significantly.

Abstract:Two kinds of program transformations widely-used in optimizing compilation, statement exchange and variable substitution, are investigated and their soundness conditions are formally defined with CTL-FV, an extension of the temporal logic CTL (computation tree logic). Sound statement exchange T_exch and sound variable substitution T_sub are defined with conditioned rewriting rules and their soundness is proved under an inductive proof frame. In addition, based on T_exch, the soundess of another transformation, dependence-preserving statement reordering inside basic blocks of programs, is also proved with a constructive method.

Abstract:This paper proposes a graph transformation based description language of model refactoring (GraTDeLMoR) to formalize model refactorings. It designs basic elements of the language according to the features of model refactorings, and proposes approaches to describe model refactorings with these basic elements. It also proposes steps of the application of refactorings formalized with the proposed language, and provides corresponding CASE support. The paper discusses the descriptive ability of the description language with some typical examples, and results suggest that the proposed language is expressive in formalizing model refactorings.

Abstract:As the Web Service composition becomes complex, testing to ensure their quality and reliability become crucial. This paper extends traditional data flow analysis to Web Service composition testing. A test method for BPEL-based Web Service composition based on data flow analysis is presented. The test method is based on a test model called WSCTM that captures data flow test artifacts of Web Service composition. With the considerations of the intra-activity, intra-service, and inter-service, testing for Web Service composition based on data flow analysis can be accomplished in three levels, and various flow graphs are used to describe the interaction within and between services in structure model. The def-use chains of the Web Service composition can be obtained based on above analysis method. As a result, test paths can be selected to satisfy given criteria in order to achieve a desired Web Service composition test coverage.

Abstract:In this paper, the typed category theory is extended and combined with process algebra to provide a unified description framework for the formal semantics of architecture-centric model transformations. The structural semantics of architecture models are described within typed category diagrams, and the behavioral semantics are represented by process traces affiliated to the categorical framework, and the mapping relations between component models are formally described by morphisms and functors of category theory. The framework can be used for the description, analysis and judgment of property preservation of model transformations, and thus make an effective support for model-driven software development.

Abstract:This paper surveys the state-of-the-art research on paraphrasing in natural language processing, including the applications, the acquisition of resources, the generation, and the evaluation of paraphrases, as well as some closely related topics. This paper aims to make a summary, comparison and analysis of the mainstream methods and the latest progress in the field, expecting to be helpful to the future research.

Abstract:The goal of this paper is to give a brief summary of the current unsupervised word sense disambiguation techniques in order to facilitate future research. First of all, the significance of unsupervised word sense disambiguation study is introduced. Then, key techniques of various unsupervised word sense disambiguation studies at home and abroad are reviewed, including data sources, disambiguation methods, evaluation system and the achieved performance. Finally, 14 novel unsupervised word sense disambiguation methods are summarized, and the existing research and possible direction for the development of unsupervised word sense disambiguation study are pointed out.

Abstract:A covariance-free method of computing kernel principal components is proposed. First, a matrix, called Gram-power matrix, is constructed with the original Gram matrix. It is proven by the theorem of linear algebra that the eigenvectors of newly constructed matrix are the same as those of the Gram matrix. Therefore, each column of the Gram matrix can be treated as the input sample for the iterative algorithm. Thus, the kernel principle components can be iteratively computed without the eigen-decomposition. The space complexity of the proposed method is only O(m), and the time complexity is reduced to O(pkm). The effectiveness of the proposed method is validated by experimental results. More importantly, it still can be used even if traditional eigen-decomposition technique cannot be applied when faced with the extremely large-scale data set.

Abstract:The proposed model labels the negotiation history data automatically by making full use of the implicit information in negotiation history. Then, the labeled data become the training samples of least-squares support vector machine that outputs the estimation of opponent’s utility function. After that, the self’s utility function and the estimation of opponent’s utility function constitute a constraint optimization problem that will be further figured out by genetic algorithm. The optimal solution is the counter-offer of oneself. Experimental results show that the proposed model is effective and efficient in environments where information is private and the prior knowledge is not available.

Abstract:This paper proposes a possibility walking state analysis model for legged robots based on the feedback of acceleration sensor processed by discrete Fourier transform the dynamic analysis of the walking of legged robot. According to Mahalanobis distance, this model can express the legged robot walking status quantitatively. Using quadrupled robots as an example for evaluation, the experimental results show that this model is able to describe the walking of legged robots and express the walking status in real time, and it can help legged robots adjust their locomotion with the change of environment to ensure their walking stability.

Abstract:This paper proposes a model of argumentation, in which the internal structures of arguments are expressed with the simplified Toulmin model, and the relations between arguments are defined with the method of Dung’s abstract argumentation framework. It also gives the algorithms of the defensibility of an argument and the acceptability of a statement. This model is used to reconstruct the examples in the published literature, and results show that this model can accurately calculate the acceptability of statements and draw a conclusion from argumentation. This research is to construct models for real-world practices of argumentation, but the conclusion will contribute to the modeling of formal nonclassical logics systems.

Abstract:A strategy is proposed for facial expression recognition under the graph embedding (GE) framework. The neighborhood weighted graph based on the expression similarity is constructed to learn the sub-space. In the sub-space, the data distribute on the manifold based on expression semantic. The proposed sub-space method can overcome the difficulties for facial expression recognition caused by the differences in individuals, lightings, poses. The expressions of the facial images in the data set are exploited in a semi-supervised way. Expression similarity between two facial images is measured by the dot product of the expression fuzzy membership function vectors. Experimental results on Cohn-Kanade and the data set of this paper demonstrate the effectiveness of the approach.

Abstract:This paper analyzes the previous study of applying P2P technology in mobile Internet. It first introduces the P2P technology and the conception of mobile Internet, and presents the challenges and service pattern of P2P technology in mobile Internet. Second, the architectures of P2P technology in mobile Internet are described in terms of centralized architecture, super node architecture and ad hoc architecture, respectively. Further more, the resource location algorisms and cross-layer optimizations are introduced based on two different terminal access patterns. Detailed analyses of different key technologies are presented and the disadvantages are pointed out. At last, this paper outlines future research directions.

Abstract:A memory efficient regular expression compression algorithm is devised for deep packet inspection. First, a parameter DR (distending rate) is defined to quantify the explosive quality of regular expressions. Then based on DR, a regular expression cutting algorithm is proposed to downsize the storage needs of individual regular expression, by detecting and confining the parts which cause DFA (deterministic finite automaton) states’ exponential growth. Then according to the relation of different regular expressions, a selective grouping algorithm is introduced for regular expression sets, which could cut down the number of finite automata, and reduce the runtime memory consumption.

Abstract:This paper proposes a data gathering method-SRAD (selective replication-based adaptive data delivery scheme). The main idea of SRAD is to replicate messages selectively to nodes that have higher probability to meet the sink. SRAD consists of two key components: data transmission and queue management. The former makes decisions on when and where to transmit data messages according to the node delivery probability in random waypoint mobility model. The latter based on the message survival time to decide message’s transmission and dropping to minimize the transmission overhead. Simulation results show that the proposed SRAD data delivery scheme cannot only have a relatively longer network lifetime but also a higher message delivery ratio with the lower transmission overhead and less data delivery delay than other DTMSN (delay tolerant mobile sensor networks) data delivering approaches.

Abstract:Inspired from the idea of data fields, a community discovery algorithm based on topological potential is proposed. The basic idea is that a topological potential function is introduced to analytically model the virtual interaction among all nodes in a network and, by regarding each community as a local high potential area, the community structure in the network can be uncovered by detecting all local high potential areas margined by low potential nodes. The experiments on some real-world networks show that the algorithm requires no input parameters and can discover the intrinsic or even overlapping community structure in networks. The time complexity of the algorithm is O(m+n^3/γ)～O(n²), where n is the number of nodes to be explored, m is the number of edges, and 2<γ<3 is a constant.

Abstract:Parallel downloading is modeled. And based on the model, the optimal mechanism is analyzed and proposed in terms of the performance of downloading nodes. The optimal mechanism includes the optimal source nodes set selected and file blocking scheme. Theoretical analysis proves that this mechanism can minimize the cost function of downloading nodes. Simulation results justify the validity of this mechanism.

Abstract:After the best optimizing approach of network coding is being studied, some methods are proposed based on the characteristics of the network coding overhead optimization problem. First, two modifications are added to the preprocessing phase: 1) How to generate a fitness value to a network coding scheme under a certain network coding optimization request is presented. This makes different network coding optimization problems be solved with the same genetic algorithm. 2) An additional exam processing of the multi-in outgoing links is imported to reduce the solution space. Second, experimental results show that the random generated solution of network coding optimization problem can hardly achieve the multicast rate, three new steps are suggested be taken with the common genetic algorithm: 1) use more delicate member generating function to generate initial members; 2) add new members at the beginning of each round of the genetic algorithm to avoid localized optimization; 3) assign a fitness value based on each receiver’s data rate rather than ?1 to those network coding solutions which cannot achieve the max multicast rate. Experimental results show dramatic improvements in terms of both efficiency and result.

Abstract:To improve the efficiency of alias resolution in large scale network, a concept of alias filtering is proposed based on IP level topology measured by traceroute. The characteristics of alias relationship are explored theoretically, and three attributes are proposed to deal with traceroute data based on the characteristics. Then, an alias filtering algorithm called AF and a verification of alias filtering algorithm called VAR are put forward. Finally, both the algorithms are verified via the traceroute data from Internet covering China, Japan, and Korea, which are measured by Skitter of CAIDA (Cooperative Association for Internet Data Analysis). The results prove that the concept of alias filtering is very important and the algorithms proposed in this paper are valid and efficient.

Abstract:An interleaving coded multi-threshold scheduling (ICMTS) algorithm is proposed in this paper. Since the ICMTS algorithm uses the interleaving coded thresholds of two stage queues as the scheduling weights, it can systematically evaluate the scheduling demands of both the input queues and the crosspoint queues. By segmenting the queue length as multiple thresholds, the hardware resource of this algorithm can be largely decreased. It is proved that a CICQ (combined input-crosspoint-queued) switch operating with the ICMTS algorithm can achieve 100% throughput with a speedup of two. To facilitate hardware implementation, a simplified maximal ICMTS scheme is also presented with a time complexity of O(logN). Simulation results show that even the simplified ICMTS scheme can obtain better performance than the existing algorithms.

Abstract:RT_B, the language describing behavior-driven trust management, is given. Variables are introduced into roles to maintain the cumulate behavior status of the users. Behavior-Driven credentials modify users’ assigned local roles in a trust domain according to the behaviors enforced by the users. Combined credentials improve the efficiency of trust determination. Trust policy update credentials allow trust domains to update trust policies automatically when the system statuses are changed. Implementation framework of behavior-driven trust management is described. Several optimization mechanisms of realization are discussed.