Abstract:To solve the satisfiability (SAT) problem in propositional logic, many algorithms have been proposed in recent years. However, practical problems are often more naturally described as satisfying a set of first-order formulas. When the domain of interpretation is finite and its size is a fixed positive integer, the satisfiability problem in the first-order logic can be reduced to SAT. To facilitate the use of SAT solvers, this paper presents an algorithm for generating SAT instances from first-order clauses, and describes an automatic tool performing the transformation, together with some experimental results. Several different ways of adding formulas are also discussed to eliminate symmetries, which will reduce the search space. Experiments show that the algorithm is effective and can be used to solve many problems in mathematics and real-world applications.

Abstract:A homomorphism φ of CNF formulas from H to F is a function mapping the set of literals in H to the set of literals in F and it preserves complements and clauses. If the formula H is homomorphic to the formula F, then the unsatisfiability of H implies the unsatisfiability of F. A CNF formula F is minimally unsatisfiable if F is unsatisfiable and the resulting formula deleting any one clause from F is satisfiable. MU(1) is a class of minimally unsatisfiable formulas with the deficiency of the number of clauses and variables to be one. A triple (H,φ,F) is called a homomorphism proof from H of F if φ is a homomorphism from H to F. In this paper, a method from the basic matrix of MU(1) formula is used to prove that a tree resolution proof for an unsatisfiable formula F can be transformed into a homomorphism proof from a MU(1) formula for F. Whence, the homomorphism proof system from formulas in MU(1) is complete, and this proof system and the tree resolution proof system can be transformed mutually in polynomial time on the size of proof.

Abstract:In the area of language -based security, programs written in typed high-level languages need to be translated into those written in typed low-level languages. This work is not trivial when type dispatch constructs are involved and implemented with tag mechanism. This paper proposes a new type that can deal with a special type dispatch construct occurring in the interface invokation of Java. A low-level language with this type is able to efficiently implement the interface invokation. This implementation approach is adopted in a Just-In-Time compiler with a typed low-level language as a certifying language.

Abstract:A reactive system does not terminate and its behaviors are typically defined as a set of infinite sequences of states. In formal verification, a requirement is usually expressed in a logic, and when the models of the logic are also defined as infinite sequences, such as the case for LTL (linear temporal logic), the satisfaction relation is simply defined by the set containment. However, this satisfaction relation does not work for interval temporal logics, where the models are finite sequences. In fact, for different interval based properties, different satisfaction relations are sensible. Two classes of finitary properties are identified, and then two satisfaction relations are defined for them, which are unified by a general relation. A model checking algorithm is proposed and implemented in a verification tool for QRDC (quantified RDC (restricted duration calculus)), which is an interval temporal logic. The tool QRDChecker can check the validity of QRDC formulae under both continuous and discrete interpretations. Moreover, for discrete QRDC, it can also translate the formulae into an automaton in the form accepted by the Spin model checking system, which can be subsequently used to verify a reactive system against properties expressed in the logic.

Abstract:Mean shift is an effective iterative algorithm widely used in clustering, tracking, segmentation, discontinuity preserving smoothing, filtering, edge detection, and information fusion etc. However, its convergence, a key property of any iterative method, has not been rigorously proved till now. In this paper, the traditional mean shift algorithm is first extended to account for both the local property at different sampling points and the anisotropic property at different directions, then a rigorous convergence proof is provided under these extended conditions. Finally, some approaches to adaptively selecting the algorithm’s parameters are outlined. The results in this paper contribute substantially to the establishment of a sound theoretical foundation for the mean shift algorithm.

Abstract:Input-Queueing is becoming increasingly used for high-bandwidth switches and routers for its scalability, but it needs an elaborate scheduling algorithm to achieve good performance. Round-Robin algorithms have been extensively investigated due to its simplicity and parallelism. However, the present Round-Robin algorithms suffer from poor performance under nonuniform and burst traffic. This paper proposes a Round-Robin algorithm named iSLOT, which can approximate the maximum matching algorithms by iterating the scheduling decision between slots and using the randomness of the queue length. Simulation results show that iSLOT not only is stable under uniform i.i.d traffics, but also outperforms the existing round-robin algorithms under burst and nonuniform traffics in throughput and delay performance.

Abstract:As Wu’s method, based on symbolic computation, has found applications in more and more fields, it is challenged by more and more complicated calculation problems. The soul of the method, dividing and ruling problem, is very suitable for distributed computation. In this paper, a high performance computing technique is introduced into the symbolic computation and a distributed computing model (DCM) for Wu’s method over Internet is put forward. First, the feasibility and requirement for distributed computation of Wu’s method is analyzed. Then the data communications for big integers and polynomials are put forward in detail, and finally the design and implementation for DCM based on ELIMINO and Globus Toolkits 3 are presented.

Abstract:Research on the approximated algorithms for k-Median problem has been a focus of computer scientists, and most of the existing results are based on the Euclidean and Metric k-Median problem. However, results for general distance space k-Median has not been found for many years. In general distance space, let dmax/dmin denote the maximum value of the length of the longest edge divided by the length of the shortest edge for one client point. In this paper, it is first proved that there are no polynomial algorithms of approximation ratio 1+ω-1/e for k-Median with the condition d_max/d_min≤ω+ε, unless NP=DTIME(n^{O (loglog n)}) . This result implies there are no polynomial algorithms of approximation ratio 1+2/e for Metric k-Median unless NP=DTIME(n^O(loglogn)). Then a local search algorithm for k-Median is presented. New analysis shows that the local search can achieve a ratio of 1+ω-1/2. This result can also be extended to the Metric k-Median, and if ω≤5, the local search algorithm can achieve a ratio less than 3 for the Metric k-Median, which is better than the existing best ratio 3+2/p. Finally, p computer verification is used to study the real computational effect and the improved method of the local search algorithm.

Abstract:Supporting multiple instances of one activity can enable workflow management system to be flexible on handling workflow process. When handling multiple instances the main problem is the schedule of instances. After analyzing the assignment and the join of multiple instances, this paper proposes the context of workflow activities and then formally describes the semantic of a multi-instance activity. Base on the formal presentation, the concept of Shell is proposed to control the assignment and submission of the multiple instances. The Shell can control the multiple instances to run synchronically and control the progress of workflow process according to the semantics of activities. The Shell gives a solution to schedule and control of activity multi-instances in workflow process.

Abstract:This paper presents an active measurement model (AMM) for software process control and improvement, and the related measurement method. AMM formally describes the goal, feature, and indicator of software process, and their relationship. AMM also provides some principles, methods, and techniques to determine the measurement of software process. Based on AMM, on one hand, software organizations can deduce the appropriate measurement process according to the goals of the processes they focus; on the other hand, they can also identify the opportunity and roadmap of improvement according to the result of measurement. It will provide an effective support for software organization to make an accurate decision and achieve a successful result.

Abstract:The problem of constructing a Petri net feedback controller, which enforces linear inequality constraints involving the marking vector and the Parikh vector on a discrete event system (DES) modeled by Petri nets (PN), is discussed in this paper. A novel method for design of controller enforcing the constraints is presented. First the constraints involving the marking and Parikh vectors are transformed into the constraints involving Parikh vector only using Petri net state equality, and then the controller is constructed based on the viewpoint that a place can be seen as a linear inequality constraint on the Parikh vector. The method is proved to be simpler and more efficient than that presented by Iordache and Moody through an applied instance that was also used by Moody et al., and holds remarkable advantage especially for large systems.

Abstract:In this paper, software requirements are analyzed by using quantification theory of type 3 (QT3). On the basis of this quantitative analysis, by utilizing the house of quality (HOQ) matrix of quality function deployment (QFD), and based on the fuzzy analytic hierarchy process (FAHP) improved by fuzzy technique, a method of mapping software requirements going through the process of software design is proposed. Its effectiveness is presented by applying this method to the development process of the CD-R/RW recording device software.

Abstract:As originally designed for wired networks, TCP (transmission control protocol) congestion control mechanism is triggered into action when packet loss is detected. This implicit assumption for packet loss mostly due to network congestion does not work well in Mobile Ad Hoc Network, where there is a comparatively high likelihood of packet loss due to high bit error rate (BER) and node roaming. Such non-congestion packet loss, when dealt with by congestion control mechanism, causes poor TCP performance in MANET. All improvement mechanisms have two distinct phases: problem detection and problem solving. This paper attempts to address this problem by first summarizing over several major reasons for such mis-behavior, an in-depth analysis and the detailed comparison between different solutions are proposed to improve at each of the two phases. Finally, some new research directions for optimizing TCP performance in MANET (mobile ad hoc network) are suggested.

Abstract:On the basis of analyzing the problem of unicasting QoS routing in Ad Hoc networks, a new distributed QoS routing algorithm in the Ad Hoc network—EBLLD (entropy-based long-life distributed QoS routing) algorithm, is proposed. The key idea of EBLLD algorithm is to construct the new metric-entropy and select the long-life path with the help of entropy metric to reduce the number of route reconstruction so as to provide QoS guarantee in the Ad Hoc network whose topology changes continuously. The EBLLD algorithm uses the local multicast mechanism, orders and sorts the outgoing link with the heuristic function and entropy metric to reduce the message overhead. The simulation shows that the EBLLD algorithm can acquire a higher routing success ratio with the low message overhead. In addition, the EBLLD algorithm is scalable and applicable to large-scale Ad Hoc network.

Abstract:Transformation of the widely used Pedersen's Verifiable Secret Sharing (Pedersen-VSS) to Pedersen-VSS-General secure against general adversary is first presented. Then a misunderstanding about the use of zero-knowledge (ZK) proof in the DL-Key-Gen scheme proposed by R. Canetti etc. is pointed out, and an improvement to it is made. An adaptively secure distributed key generation scheme against general adversary without the assumption of erasure is developed. A detailed black-box simulator for the security proof of the proposed scheme is also given.

Abstract:Linux is widely adopted in routers nowadays, and traffic control is one of the most important functions for this kind of network-oriented operating systems. This paper studies the traffic control mechanism of Linux system and shows that the packet scheduling based traffic control mechanism adopted by current Linux kernel lacks a global view of system bandwidth, and is also short of efficient ingress scheduling. This can result in unnecessary CPU time wasting. To address this problem, a novel traffic control scheme is proposed, which is based on the CPU scheduling of the network protocol processing. By transplanting packet scheduling from the egress point of network interfaces to the soft interrupt handler that processes incoming packets, the new method can eliminate disadvantages of the old traffic control scheme without introducing any additional demerits. An implementation of the new traffic control scheme is given, and comparative experimental results show that the new mechanism has fewer overload than the old traffic control scheme in Linux, and can maintain the efficiency of traffic isolation and traffic policing while avoiding the CPU time wasting.

Abstract:This paper analyses Wang et al.’s member deletion scheme of group signature and shows that in their scheme, after the group manager changes the group’s key, the excluded group members can still modify their secret property key, prove their membership and issue valid signatures. So this scheme cannot delete any group member and is insecure.

Abstract:Focusing on the particular security problem of mobile Agent data protection, the IKCE (interrelated keys chains encryption) method is proposed. Security analysis and performance analysis for the IKCE method are surveyed. The key idea of the IKCE method is to establish an interrelated relationship among encryption keys used in encrypting Agent data in order to protect the Agent data. The research states that the IKCE method is available for protecting the Agent data.