Abstract:Synthesis process is an important bottom-up approach on modeling Petri net systems, and the preservation of certain good properties such as liveness, deadlock-freeness, reversibility and so forth is also a significant problem in the study of synthesis processes. In this paper, the preservation of liveness and deadlock-freeness is discussed for a synchronous synthesis process. The difference from other work is that the presented approaches are based on the concurrent composition of paths using a concurrent language. The concurrent language relation formula is presented and proved in the synchronous synthesis of Petri net systems, and it can be applied to judge the liveness and deadlock-freeness of a synthesized system. Meanwhile, criteria which are necessary and sufficient for the liveness and deadlock-freeness of the resultant system are developed. Finally, conditions under which the preservation of liveness and deadlock-freeness holds for the synchronous synthesis of Petri net systems are proposed.

Abstract:The main focus in Monad-oriented programming is on a set of Monad definitions and a Monad can be defined in an MAP style or a BIND style. Given a Monad library, it can be used directly if it meets the style of the users?need, otherwise, a new style of Monad should be reconstructed, which is a fussy job and even more the new one may not always satisfy the axioms of a Monad definition. However if an automatic Monad generator is added to the library, users can use a Monad freely without asking whether a new style of Monad is needed or how to construct a Monad in order to satisfy the several axioms of the Monad definition, which not only benefits users but also extends the original Monad library. In this paper an automatic Monad generator from other style of Monad is designed and implemented in Haskell. The generating arithmetic is based on the identity relationship between two Monad definitions.

Abstract:Binarization is the most popular discretization method in decision tree generation, while for the domain with many continuous attributes, it always gets a big incomprehensible tree which can't be described as knowledge. In order to get a more intelligible decision tree, this paper presents a new discretization algorithm, RCAT, for continuous attributes in the generation of binary classification tree. It uses simple binarization to solve the multisplitting problem through mapping a continuous attribute into another probability attribute based on statistic information. Two pruning methods are introduced to simplify the constructed tree. Empirical results of several domains show that, for the two-class problem with a preponderance of continuous attributes, RCAT algorithm can generate a much smaller decision tree efficiently with higher intelligibility than binarization while retaining predictive accuracy.

Abstract:Support vector machine (SVM) is a learning technique based on the structural risk minimization principle, and it is also a class of regression method with a good generalization ability. This paper presents an improved SMO (sequential minimal optimization) algorithm to train the regression SVM, which gives an the analytical solution to the QP problem of size two. A new working set selection method and a stopping condition are developed. The simulation results show that the improved SMO algorithm is significantly faster and more precise than the original SMO one.

Abstract:In this paper, a speech recognition and verification method is presented based on the integration of likelihood and likelihood ratio. Speech recognition and verification is unified in one-phase framework. In the process of decoding, likelihood ratio is combined with likelihood to get the combination score for searching the final results. Experimental results show that the false-alarm rate is significantly reduced, with only a slight loss in the accuracy rate.

Abstract:In 1996, Mambo et al. introduced the concept of proxy signature. However, a proxy signature only provides the delegated authenticity and doesn't provide the confidentiality. Chan and Wei proposed a threshold proxy signcryption scheme (denoted as Chan-Wei scheme), which extended the concept of proxy signature. In this paper, the authors demonstrate Chan-Wei scheme does not satisfy strong unforgeablity, strong nonrepudiation and strong identifiability. Based on Chan-Wei scheme, a nonrepudiable threshold proxy signcryption scheme with known proxy agents is proposed. The proposed scheme overcomes the weaknesses of Chan-Wei scheme. Completeness proof and security analysis of the proposed scheme are presented. In addition, compared with Chan-Wei scheme, the proposed scheme exactly finds out which proxy agents present bogus secret shadow or tamper secret shadow.

Abstract:Strand space model and CSP method are two popular approaches to formal analysis for authentication protocols. In this paper, the different characteristics of the above approaches are outlined through a concrete authentication protocol.

Abstract:NAT-PT(network address translation + protocol translation) would allow IPv4 nodes to communicate with IPv6 nodes transparently by translating the IPv6 address into a registered V4 address. However, NAT-PT would fall flat when the pool of V4 addresses is exhausted. NAPT-PT multiplexes the registered address' ports and will allow for a maximum of 63K outbound TCP and 63K UDP sessions per IPv4 address, but it is unidirectional. In this paper, a novel solution ENAT-PT (enhanced NAT-PT) is presented which allows for a great number of inbound sessions by using a single V4 address. The main idea of ENAT-PT is the use of session parameters instead of source address for session identification. By using ENAT-PT, it is easy to visit V6 networks from a V4 network with a small address pool.

Abstract:Mobility management is an important aspect in LEO (low earth orbit) systems. In terrestrial wireless networks, the movement of the user triggers location updating and determines the paging scheme, while in LEO satellite systems, the location updating and paging is mainly based on the movement of satellite. Terrestrial location management techniques must be altered to fit the LEO systems. This paper introduces a modified movement-based location updating and paging scheme in LEO networks. In this scheme the meta-cell concept is proposed which includes two spot-beams of one satellite. First the location management scheme based on the architecture with meta-cell location area is presented. Then an analytical model is applied to formulate the cost of location updating and paging for the movement meta-cell based dynamic location updating scheme. The comparison of performance between the meta-cell architecture method and the conventional signal-spot-cell architecture method is provided to demonstrate the cost-effectiveness and robustness of the proposed scheme under various parameters. To reduce the impact of meta-cell architecture on the location paging cost, a forced location updating strategy is presented which is used in the cases that the meta-cell includes the two spot-beams from different satellites.

Abstract:Multicast is a preferred network communication technique in the case of multiple recipients, whose importance has been increasingly highlighted with the development of the Internet. IGMP, the multicastmanagement protocol, does not provide access control of the users. In order to protect communicationconfidentiality, traffic in secure multicast is encrypted with a Session Encryption Key (SEK) which is known only to the certificated group members. Whenever there is a change in the group membership, the SEK has to bedynamically updated, thus the key distribution becomes a key problem in the research of secure multicast. In designing key distribution algorithms, communication costs, key storage, protection against attacks and computation complexity are considered as the four important factors. A group key distribution scheme utilizing a polynomial expansion is proposed, which features in no traditional encryption and decryption. Analyses show that it performs well in small scale multicast. This polynomial expansion based algorithm is then integrated with the Logical Key Hierarchy; while preserving the logarithmic communication cost with the group size, the presented PE-LKH scheme lowers the computation complexity observably, thus is scalable to large dynamic groups.

Abstract:Nowadays, Internet is facing two challenges simultaneously: the need of a higher switching speed and the provision of a QoS guarantee. The former requires that memories in switches/routers should work at a line rate, and the latter requires that switches should mimic OQ (output queuing) switches. The present CIOQ (combined input-output queuing) scheme for switches needs a speedup of 2. In this paper, a novel design scheme based on parallel technique is proposed, which is called DPS (duplicated ports switch). DPS enables the internal fabric of switches to work at the line rate. A theoretical proof shows that each port with a duplicated number of 2 is sufficient to mimic the OQ switches and is necessary in practice.

Abstract:While content-aware distribution policies are getting more popular in cluster-based web systems, they make the dispatching node a bottleneck. To address the scalability and fault-tolerance problem, issues about designing distributed dispatching policies are discussed. For the policies aiming at improving the cache hit rate, a distributed dispatching policy named DWARD (distributed workload-aware request distribution) that takes into account both the load balance and the locality enhancement is presented. Finally, a testbed is implemented on the basis of a Linux kernel to benchmark various dispatching algorithms. The performance results show that DWARD can achieve a favorable throughput compared with the state-of-the-art dispatching policies.

Abstract:Virtual endoscopy, which is a noninvasive procedure for detecting anomalies inside human organs, is meaningful for medical diagnosis and surgery. In order to perform an accurate navigation, the centerline of the model must be extracted. In this paper, a new centerline extraction algorithm based on Hessian Matrix is proposed. First, the distance transformation is performed. Then the initial path is obtained by computing the eigenvalues and eigenvectors of the Hessian matrix. After that, the visibility test with an adaptive visibility sphere radius, which is determined by the eigenvalues of the Hessian matrix, is carried out to remove the useless voxels in the centerline. Finally, the path with all the points staying away from the surface is generated by Dijkstra抯 shortest path algorithm. The experimental results illustrate the efficiency of the proposed algorithm.

Abstract:Generating subdivision surfaces with complicated curve interpolation constrains is a concerned topic for computer graphics and geometric modeling. In this paper an efficient method that can interpolate cubic NURBS curves is proposed for generating the subdivision surfaces. A 憇ymmetric zonal mesh?is constructed by designing symmetric quadrilaterals for both sides of the control polygon of the interpolated curve. Applying the non-uniform Catmull-Clark subdivision scheme proposed by Sederberg et al. to the symmetric zonal mesh, it is proved that the mesh can converge to the interpolated curve. As a result, the limit surface of the polygonal mesh containing the symmetric zonal meshes is the subdivision surface satisfying the curve interpolation constrains. This algorithm can interpolate both the single NURBS curve and the curve mesh consisting of several NURBS curves. Therefore it can be widely used for product shape design and graphic software development.

Abstract:In parametric CAD design, the designers often encounter the question of judging whether a parametric model is under-, over- or well-constrained. In this paper, a graph-based algorithm for the question is proposed. This algorithm gives not only the decision of under-, over- or well-constrainess of a parametric model, but also the exact location where under-, over- or well-constraint occurs in the parametric model. This feature provides a more convenient way to the designers in the process of designing.

Abstract:Analysis and recognition of the facial expressions play an important role in both the social society and the affective computing in the field of the computer science. There are three primary methods for the analysis of expression motive features: methods based on the facial geometrical structure features, on the definition of the expression space based on the eigen-face, and on the motion pattern matching. This paper extracts the feature regions of the expressions based on the facial physics-muscle model and evaluats the optical flow of the expression image sequences. The eigen-flow vectors can be calculated to constitute the eigen-sequences, and therefore, the expressions can be analyzed. The recognition system is implemented as an agent in the multi-perception machine and it is used as part of the video input for understanding the human body languages.

Abstract:Some new formulae for the derivative bounds of parametric curves, such as the general polynomial curves and rational polynomial curves in CAGD, are presented. Based on these new formulae, the point-by-point algorithm for rasterizing parametric curves is developed in this paper. To solve the problem of repetition and discontinuity arising from the previous algorithms, a new rule of interpolation is given. Without doubt, these results will remarkably improve the efficiency of modeling, intersection, approximation, rendering and rasterizing of curves.