Abstract:This paper investigates reasoning support for the semantic Web based on the first-order logic. The key reasoning tasks of the semantic Web can be reduced to deciding the satisfiability of formulas. The first-order logic theorem prover is efficient and complete for unsatisfiability, while finite model searcher finds models for satisfiable formula. This paper proposes to use a theorem prover and a finite model searcher concurrently in the semantic Web reasoning. The experiments show that the method can make up the deficiencies of the description logic reasoner and complement the theorem prover for satisfiable formulas.

Abstract:Based on the vision of the Semantic Web, DLclog, a new hybrid formalism combining description logics (DL) and logic programming (LP), is described, which extends DL+log from syntax and semantics. In DLclog, negative dl-atoms can occur in the bodies of the rules, and are interpreted non-classically by McCarthy’s parallel circumscription, i.e., the extents of these DL predicates are minimized with the extents of all other DL predicates varying. In this way, the Nonmonotonic Semantics (NM-Semantics) of DL+log is extended to the Nonmonotonic Circumscriptive Semantics (NMC-Semantics), and therefore, DLclog becomes the hybrid system with the stronger expressiveness and reasoning abilities. A decision procedure is given when DL ontology is written in ALCIO or ALCQO and roles are not allowed to occur in negative dl-atoms, and the complexity is analyzed.

Abstract:A restricted constraint system called hybrid zone is formalized for the representation and manipulation of rectangular automata state-spaces. Hybrid zones are proved to be closed over reachability operations of rectangular hybrid systems. In addition, rectangular hybrid systems are used to simulate nonlinear hybrid systems, which enables us to use hybrid zones for reachability analysis of nonlinear hybrid systems. After the hybrid zone has been converted to the canonical form, reachability operations for hybrid systems can be implemented straightforwardly. Hence, the main computation is the operation for obtaining the canonical form of hybrid zones. Finding the canonical form can be automated by an algorithm for linear programming.

Abstract:Linear time mu-calculus (μTL) is an extension of linear-time temporal logic (LTL) by fixed points, which is a convenient way to specify and reasoning about reactive systems. As μTL being more expressible than LTL, the properties specified by LTL could be determined by μTL. Similar to the intuitionistic linear-time temporal logic (ILTL), we propose an intuitionistic variant of μTL as intuitionistic linear time mu-calculus (IμTL). We have established a correspondence between ImTL and ILTL, and compared their expressive power. Using IμTL to specify safety and liveness properties, and assumption-guarantee specifications are also discussed.

Abstract:Combining the classification and matching of fingerprints together, a neighborhood structure is proposed in this paper, which includes the orientation field and minutia around the reference singular point. This structure has the advantage that the identification information is centralized around the singular point, and can dramatically decrease the calculation of matching. It can also be directly used as pattern in both the continuous classification and the fast matching of fingerprints, and carry out the fast identification of the large scale database. Experimental results on NIST and FVC2004 databases show that this algorithm can highly speed up the matching of large scale fingerprint database with a preferable performance, and it can be used in one-to-many matching of on-line fingerprint identification system.

Abstract:Within the internal organization of the data, the data points respectively play three different structural roles: the hub, centroid and outlier. The neighborhood-based density factor (NDF) used in the neighborhood based clustering (NBC) algorithm has the ability of identifying which points act as hubs, centriods or outliers in separated-well data set. However, NDF often works poorly in the circumstances of noise and overlapping. This paper introduces a polynomial kernel based neighborhood density factor (PKNDF) to address this issue. Relying on the PKNDF, a structural data clustering algorithm is further presented which can find all salient clusters with arbitrary shapes and unbalanced sizes in a noisy or overlapping data set. It builds clusters into the framework of directed trees in graph theory and thereby each point is scanned only once in the process of clustering. Hence, its computational complexity is nearly linear in the size of the input data. Experimental results on both synthetic and real-world datasets have demonstrated its effectiveness and efficiency.

Abstract:The distance preserving level set method proposed by Li et al. has many advantages over the traditional variational level set methods. However, it has the disadvantage of requiring the initial curve to surround (let in or keep out) the objects to be detected. In this paper, an adaptive distance preserving level set method is proposed, in which the initial curve is no longer required to surround (let in or keep out) the objects to be detected, i.e., the initial curve can be anywhere in the image. The proposed method can detect certain object boundaries, for which the original method is not applicable. E.g. it can automatically detect interior and exterior contours of an object and edges of multi-objects, starting with only one initial curve whose position is anywhere in the image. Moreover, active contours can move into boundary concavities and perform better in the presence of weak boundaries. The proposed method has been applied to synthetic and real images of different object boundaries with promising results.

Abstract:As an extension of traditional modal logics, this paper proposes a fuzzy first-order modal logic based on beilievable degree, and gives out a description of the fuzzy first-order modal logic based on constant domain semantics. In order to make the reasoning procedure between the fuzzy assertions efficiently, the notion of the fuzzy constraint is considered. A fuzzy constraint is an expression in which both syntax ingredient and semantics information are contained. By using the notion of the constraint, the reasoning procedure between the fuzzy assertions can be directly considered in the semantics environment, thus a fuzzy reasoning formal system which contains fuzzy constraint as its basic element is developed. As a main work of the paper, the relationship between the validity of the new assertion and the satisfiability of the fuzzy constraints is analyzed, and reasoning rules of the fuzzy reasoning formal system based on first order modal logic are given out. Further work could be done by considering the soundness and completeness of the formal system, and by building an efficient mechanism of reasoning procedure. The results have potential application in the areas of artificial intelligence and computer science.

Abstract:The state of the art of network architecture is presented. Based on a micro-communication element structure (MCES), a service-based network architecture prototype is implemented, in which service units are scheduled and assembled logically. While supporting QoS and ensuring network security more effectively, the prototype can be compatible with all existing TCP/IP applications by an improved socket design. The experimental results show that the prototype of service-based network architecture is feasible, and possesses good transmission efficiently and scalability.

Abstract:A new problem is addressed, which is how to improve energy efficiency for both unicast and multicast services without violating QoS requirements of mobile stations in 802.16e wireless networks. To solve this problem, a scheduling set based integrated scheduling (SSBIS) algorithm is proposed. SSBIS partitions all the mobile stations into multicast scheduling sets and a unicast scheduling set. All the unicast data of the mobile stations in the multicast scheduling sets are transmitted in the adjacent intervals of their multicast data transmission periods, and for the mobile stations in the unicast scheduling set, longest sleep duration based (LSDB) scheduling scheme is obtained using convex optimization to improve energy efficiency of the whole system. Numerical results show that SSBIS can save overall energy significantly and guarantee the minimum data rates of mobile stations at the same time.

Abstract:An in-order queuing (IOQ) PPS architecture proposed in this paper uses a small fixed-size buffer in the demultiplexor to distribute traffic equally among switch planes, with central combined input-and-output queuing (CIOQ) switch planes under the control of a single scheduler that applies the same matching at each of the parallel switch planes during each cell slot. This operation is called synchronous scheduling. It is proved that the round robin demultiplexing algorithm along with synchronous scheduling guarantees cells of a flow can be read in order from the output queues of the switch planes. Furthermore, by using a synchronous scheduling called strict longest queue first (SLQF) algorithm this scheme reduces considerably not only the amount of state information required by the scheduler, but the communication overhead required to achieve cell reordering. Compared with existing PPS designs, IOQ PPS (in-order queuing parallel packet switch) is more practical to implement in hardware because of its simple implementation mechanisms, as the experimental results demonstrate, and it offers the best delay performance.

Abstract:A TBPR (time-based broadcasting for power-aware routing) protocol is proposed. Since more hops can save more energy in wireless transmission, the TBPR protocol selects more energy efficient routes by comparing accumulated power consumption based on the mechanism of delaying rebroadcast route request packets. This method can reduce energy consumption and prolong the lifetime of network. Simulation results indicate that the TBPR protocol can conserve more energy and reduce energy consumption in wireless Ad hoc networks.

Abstract:According to the given keyframes and associated timing, how to simulate the human motion that conforms to Newton’s law by optimization is an important problem. The convergence property of current optimization models where the constraint of Newton’s law is regarded as the direct constraint condition is not satisfactory in practice. There are 2 reasons for that. The first is that the nonlinearity of Newton’s law is strong. The second is that the current optimization methods can only find local minimizers. By converting the constraint of Newton’s law into the objective function and adding the optimization of given timing, the convergence property of which is better than that of the current optimization models and is independent of the type of simulated motion, the error of mass parameters of human body and the error of the given timing. The simulated human motion can conform to Newton’s law as much as possible. The efficacy of the new model is validated by simulating seven types of somersaults on the trampoline. Furthermore, this model has been applied to the analysis of forces acting on human body and the design of new motions in sports.

Abstract:This paper designs and implements an algorithm framework for the out-of-core medical data processing and analyzing and integrates it into MITK (medical imaging toolkit), an algorithm toolkit for medical image processing and analyzing accomplished by the group. With the help of this, a processing platform for the out-of-core medical data is set up and fast out-of-core volume rendering algorithms based on volume ray casting and 3D texture are studied in this paper. A semi-adaptive partitioning method is proposed to divide original data sets into sub-blocks and get a better partitioning result without influencing the partitioning speed. Furthermore, the graphics hardware is also used to accelerate the rendering process. The experimental results indicate that the new framework and algorithms are effective and efficient for the processing and visualization of the out-of-core medical data sets.