Abstract:A partition based Boolean satisfiability solving method is proposed. By partitioning a CNF(conjunctive normal form) formula into several clause groups, Boolean satisfiability problem can be divided into small sub-problems, hence reducing the complexity of the original problem. Meanwhile, the satisfiability of different clause group can be solved in parallel, thus further speeding up the decision procedure. For the formula that clause group partition cannot be generated directly, a clustering algorithm is given to cluster clauses into clusters so that clause group partition can be generated by eliminating common variables among clusters.

Abstract:Developed in recent years, artificial bee colony (ABC) algorithm is a relatively new global optimization algorithm that has been successfully used to solve various real-world optimization problems. However, in the algorithm, including its improved versions, the scout bee usually employs the random initialization method to generate a new food source. Although this method is relatively straightforward, it tends to result in the loss of the scout bee's search experience. Based on the intrinsic mechanism of ABC's search process, this paper proposes a new scheme that employs the orthogonal experimental design (OED) to generate a new food source for the scout bee so that the scout bee can preserve useful information of the abandoned food source and the global optimal solution in different dimensions simultaneously, and therefore enhancing the search efficiency of ABC. A series of experiments on the 16 well-known benchmark functions has been conducted with the experimental results showing the following advantages of the presented approach: 1) it can significantly improve the solution accuracy and convergence speed of ABC almost without increasing the running time; 2) it has better performance than other three typical mutation methods; and 3) it can be used as a general framework to enhance the performance of other improved ABCs with good applicability.

Abstract:The emergence of open mobile platform accelerates the development of service composition in mobile application. However, most current mobile applications fulfill service through static and clustering-based composition. It is prone to "software function overloading" and overlong service accessing path, hindering the efficient use for the users. In this paper, an exploratory service composition method for mobile application. With this method, candidate composable services are provided to the user when the context changes and the selected service(s) is(are) composed into the application just in time. To acquire the candidate services, association rules between the contexts and services are mined based on the history of service selection by different users in different contexts, and used as the matching basis. Further, the traditional FP-tree algorithm is extended to enable the mining of two-dimensional items in mobile application. Experiments show that the extended algorithm has higher precision and recall rate than the traditional method in matching for candidate services.

Abstract:In this paper, an approach is proposed to model and verify a class of interrupt-driven systems. An interrupt-driven system usually consists of interrupt handlers and system-scheduling tasks. When an interrupt occurs, the corresponding interrupt-handler executes in response. The operating system schedules a set of tasks to deal with routine events and certain post-processing of some interrupts. In the real-time control system, it is important that interrupts are handled within their specific deadlines, otherwise, it may cause catastrophic system failures. In order to improve the reliability of interrupt-driven systems, model checking technique is introduced to the design and development process. Through analyzing numerous systems, the major system elements (including system scheduling tasks, interrupts and their handlers) and their parameters relevant to time-related failures are identified. When these parameters are specified by system designer in the design process, formal models can be constructed by the modeling method in this paper: The interrupt source is modeled as timed automata. The execution processes of interrupt handlers are modeled by the interrupt vector and the CPU process stack. A model-checking algorithm is provided to check the above formal model whether interrupt handlers can be executed within their response deadlines. Moreover, a variation of this algorithm is developed to check properties of the integrity of shared resources and the atomicity of subprograms.

Abstract:In this paper, an inherent relationship between MUPS and MIPS is obtained by defining covering relations of unsatisfiable concepts and developing the definition of R-MUPS of unsatisfiable concept. Then a proof is given that there exists at least one unsatisfiable concept whose R-MUPS is also a MIPS for every MIPS. Based on this conclusion, an R-MUPS algorithm based on the ordered label calculus is proposed. It applies depth-first traversal in merging branches to calculate R-MUPS, and also caches the concepts of covered at the same time to speed up the solving of MIPS to achieve ontology debugging. Through revealing the equivalence between concept expansion tree and R-MUPS algorithm, the correctness of R-MUPS algorithm is proved, and its complexity is further analyzed. Finally, a comprehensive test is performed using automatically generated ontology test sets, realistic ontology and its expansion ontology. The experimental results show that the solving of MIPS based on R-MUPS algorithm can efficiently and accurately complete the ontology debugging tasks.

Abstract:The extension rule based theorem proving methods are inverse methods to resolution in a sense that they check the satisfiability by determining whether all the maximum terms of the clause set can be deduced. IER (improved extension rule) algorithm is incomplete as it cannot determine the satisfiability of the clause set when the subspace of the clause set is unsatisfiable. In this condition, calling ER (extension rule) algorithms is still needed. After a thorough investigation on the maximum terms space of the clause set, this paper develops a decomposition method for decomposing the maximum terms space of the clause set. The study on extension rule also results in the PSER (partial semi-extension rule) algorithm for determining the satisfiability of a partial space of the maximum terms. When the IER determines the subspace is unsatisfiable, PSER can be used to determine the satisfiability of the complementary space, thereby, the satisfiability of the clause set can be obtained. Based on the above progress, this paper further introduces DPSER (degree partial semi-extension rule) theorem proving method. Results show that the proposed DPSER and IPSER outperform both the directional resolution algorithm DR and the extension rule based algorithms IER and NER.

Abstract:The paper studies a matrix factorization problem for time series data, where the target matrix R consists of the equal length time series data generated by a set of objects. The goal is to find two low rank matrices U and V, such that R≈U^T×V. Many time series analysis problems, such as finance data analysis and missing traffic data imputation, can be reduced to the proposed model. A probabilistic graphical representation for the problem is proposed, and a constrained optimization model from the graphical representation is derived. The solution algorithms for the proposed model is also presented. Empirical studies show that the proposed model is superior to the baselines.

Abstract:Extended independence-friendly (IF) logic is an extension of classical first-order logic. The main characteristic of IF logic is to allowing one to express independence relations between quantifiers. However, its propositional level has never been successfully axiomatized. Based on Cirquent calculus, this paper axiomatically constructs a formal system, which is sound and complete w.r.t. the propositional fragment of Cirquent-based semantics, for propositional extended IF logic. Such a system can account for independence relations between propositional connectives, and can thus be considered an axiomatization of purely propositional extended IF logic in its full generality.

Abstract:This paper proposes a propositional modal logic with a modality □φ=□₁V□₂φ, and specifies the language, the syntax and the semantics for the logic. The axiomatic system for □ is sound and complete, where □₁ and □₂ are given in this paper. The axiomatic system for the logic has the similar language, but has the different syntax and semantics. For any formula φ, □φ=□₁V□₂φ; the frame for the axiomatic system is defined as an tripleW,R₁,R₂, and the model is defined as quadruple W,R₁,R₂,I. When the completeness theorem is proved, two equivalence relations are constructed on the set that is made up of all the maximal consistent sets. The construction method of a canonical model for the axiomatic system is different from the classical canonical model. If the accessibility relation R₁ for □₁ is the accessibility relation R₂ for □₂, then the axiomatic system for □ changes into S5.

Abstract:This paper proposes a novel Skyline query: mutual k-Skyband (MkSB) query. Unlike the traditional k-skyband query methods, MkSB executes the Skyline query from a symmetric perspective, and retrieves all the objects which are among both the dynamic k-Skyband (DkSB) of a specified query object q and the reverse k-Skyband (RkSB) of q. Furthermore, the ranking operation is introduced into MkSB due to its importance in data analysis and decision support. Since MkSB needs to perform DkSB and RkSB of q, it traverses the index multiple times, incurring much redundant I/O overhead. The proposed algorithms reduce multiple traversals to a single one, using the information reuse technology and several effective pruning heuristics that significantly cut down I/O accesses. Meanwhile, it is proved that MkSB based on window query (WMkSB) has the lowest I/O cost. Extensive experiments are conducted on both real and synthetic datasets, and the experimental results show that the proposed algorithms are efficient and outperform their competitors, i.e. the basic algorithm based on BBS (branch and bound Skyline). Especially, WMkSB has the least I/O cost and often reduces more than 95% redundant I/O accesses.

Abstract:Time series shapelets are subsequences of time series that can maximally represent a class. One of the most promising approaches to solve the problem of time series classification is to separate the process of finding shapelets from classification algorithm by adopting a shapelet transformation. The main advantages of that technique are that it optimizes the process of shapelets selection and different classification strategies could be applied. Important limitations also exist in that method. First, although the number of shapelets selected for the transformation directly affects the classification result, the quantity of shapelets which yields the best data for classification is hard to be decided. Second, previous algorithms often inevitably result in similar shapelets among the selected shapelets. This work addresses the latter problem by introducing an efficient and effective shapelet pruning technique to filter similar shapelets and decrease the number of candidate shapelets at the same time. On this basis, a shapelet coverage method is proposed for selecting the number of shapelets for a given dataset. Experiments using the classic benchmark datasets for time series classification demonstrate that the proposed transformation can improve classification accuracy.

Abstract:Tag cloud has been a popular facility used by social networks for online resource summarization and navigation. Tag selection, which aims to select a limited number of representative tags from a large set of tags, is the core task for creating tag clouds. Diversity of tag selection result is an important factor that affects user satisfaction. Information coverage and tag dissimilarity are two major perspectives for introducing diversity in tag selection. To improve information coverage and tag dissimilarity of tag selection result, this paper proposes three new tag selection approaches. In each approach, an objective function is defined to quantify both information coverage and tag dissimilarity of tags, and an approximate algorithm is designed to solve the corresponding maximization problem. Further the approximate ratio for each approximate algorithm is analyzed. The proposed and existing approaches are compared using tagging datasets extracted from the websites of CiteULike and Last.fm. The experimental results show that the new approaches perform better in terms of both information coverage and tag dissimilarity.

Abstract:Tracking the evolution and detecting events are popular and difficult problems in the field of social network analysis. Most of the research focuses on proposing different models to fit different network characteristics. This type of approach usually has three problems: (1) Each model is designed for one particular network and cannot well fit other networks; (2) There are many network statistics, so the evaluation of these network models lacks of unified platforms; (3) Without taking temporal information into account, these network models can hardly track the evolution and detect events. To solve these problems, this paper presents a method for event detection in social networks based on link prediction, which can evaluate the fluctuation of the networks and detect the events in social networks. The main work is as follow: (1) Demonstrates the method "modelling and evaluating" is in accord with link prediction on revealing the network evolution mechanism; (2) Proposes an algorithm similarity computing (SimC) to compute the similarity of networks and further improves this algorithm by taking micro factors into account; (3) Evaluates the fluctuation of the network evolution and proposes an event detecting (EventD) algorithm to detect the events. The results of the experiment show that the presented method can effectively solve the problem of tracking the evolution and detecting events.

Abstract:Network tomography provides the ability to employ the end-to-end measurements to infer the network-internal link performance parameters indirectly without requiring cooperation from the intermediate elements of the network. As a significant alternative to network measurements to be able to guide the network management as well as the network optimization, network tomography receives a plenty of attention both in academia and industry. This survey is based on an extensive collection and reference of research works at home and abroad. First, the measurement schemes exploited by the network tomography are summarized. Next, the corresponding tomographic approaches are divided into two classes regarding at what granularity they describe the link's performance: the quantitative parameter estimation and the qualitative parameter estimation. Then according to inference problems of the different parameters, a general analysis of the existing algorithms is conducted. Lastly, future research areas and potential applications are suggested.

Abstract:Location-based service (LBS) has recently become popular in almost all social and business fields due to the boom of location-aware mobile electronic devices. LBS, albeit providing enormous benefits to individuals and society, poses a serious threat to users' privacy as they are enticed to disclose their locations and query attributes to untrusted LBS providers via their LBS queries. Moreover, the contextual information attached to these locations and service attributes can reveal users' personal interests, life styles, health conditions, etc. How to preserve users' privacy against potentially malicious LBS providers is of vital importance to the well-being of LBS ecosystem, and as such, it attracts great attentions from many researchers. This paper provides a review of the state-of-the-art of privacy preserving for LBS. First, the concept and threat model of LBS privacy are presented. Then, the existing schemes for preserving users' LBS privacy are described in detail from the aspects of architecture, metric and technology. Next, a pointed discussion is placed on the latest mainstream technology, with emphasis on the distortion-based technology. Further, following a comprehensive comparison and analysis of the performance and defects of various technologies, the problems and possible solutions for LBS privacy preserving are pointed out. Finally, some future research directions are provided.

Abstract:TCM provides key migration interfaces to enhance interoperability between different TCM chips, allowing users to share keys between TCMs by key migration protocols. This study finds that the conventional TCM key migration protocol, which uses the new parent key of the migrated key on the destination TCM as the migration protection key, has two weaknesses. First, keys cannot be migrated to symmetric keys, which violates the design principles of TCM. Second, the absence of authentication between the originating TCM and destination TCM allows attacker to recover the migrated key of the originating TCM and to import his key into the destination TCM. To solve these issues, the paper proposes two new TCM key migration protocols. The first protocol, compliant with the TCM specification, allows keys to be migrated to symmetric keys and provides authentication of the destination TCM. The second protocol, which requires a slight modification to TCM key migration interfaces, not only solves all the two weaknesses, but also provides prefect forward security. Finally, the study formally analyzes the two protocols and demonstrates that the proposed protocols satisfy the correctness and desired security properties.

Abstract:In unstructured P2P networks, the existing search protocols are effective for popular resources, but searching for scarce resources is inefficient. Improving copy rates of scarce resources is the main method to solve the search inefficiency. The query hit rates on scarce resources are lower as copies of scarce resources are small. So the existing passive copy replication strategies based on the success queries are not suitable for the improvement of rare resources popularity. To solve this problem, we propose an active replication and search strategy of scarce resources. In the search process, peers with scarce resources actively initiate the search for scarce resources. And local demand information is effectively obtained in the process of search, and then scarce resources are copied to the peers that have demands for the scarce resources. The method implements the on-demand replication of scarce resources to improve popularity and query hit rates of scarce resources. Based on local requirement information, we provide three different kinds of on-demand replication strategies and a rare resource search algorithm. Experimental results show that the active replication and search strategy of scarce resources can effectively increase copy rates of scarce resources with lower replication consumption and network overhead, and then improve the query hit rates of scarce resources.

Abstract:In the traditional anonymous roaming mechanism of wireless network, remote network authentication server (RS) can not directly authenticate the identity legitimacy of roaming mobile nodes. Thus, only with the aid of home domain authentication server (HS) can RS fulfill the authentication, which results in longer time delay in roaming communication and failure to meet the fast roaming needs of sensor subnets. To address the defects mentioned above, this paper proposes a direct anonymous authentication protocol with provable secure mobile nodes in Internet of things, enabling the mobile nodes to fulfill the legitimacy authentication of their identity through one round of message exchange with RS. The protocol proposed in this paper not only achieves the legitimacy authentication of anonymous identity, but also has shorter time delay and higher operating efficiency and good anti-attack capability. Fast roaming also makes it more suitable for the environment of Internet of things in comparison with the traditional anonymous roaming protocol. The security proof shows that the new protocol is provably secure in the CK security model.