Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.

Partial Maximum Boolean Satisfiability (Partial Max-SAT or PMSAT) is an optimization variant of Boolean satisfiability (SAT) problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many real-life problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis- Putnam-Logemann-Loveland (DPLL) procedure and Branch and Bound (B&B) algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007~2011 Max-SAT evaluations, emphasizing on the most promising research directions.

Boolean satisfiability (SAT) is a well-known problem in computer science, artificial intelligence, and operations research. This paper focuses on the satisfiability problem ofModel RB structure that is similar to graph coloring problems and others. We propose a translation method and three effective complete SAT solving algorithms based on the characterization of Model RB structure. We translate clauses into a graph with exclusive sets and relative sets. In order to reduce search depth, we determine search order using vertex weights and clique in the graph. The results show that our algorithms are much more effective than the best SAT solvers in numerous Model RB benchmarks, especially in those large benchmark instances.

In this paper, we are addressing the exact computation of the Delaunay graph (or quasi-triangulation) and the Voronoi diagram of spheres using Wu's algorithm. Our main contributions are first a methodology for automated derivation of invariants of the Delaunay empty circumsphere predicate for spheres and the Voronoi vertex of four spheres, then the application of this methodology to get all geometrical invariants that intervene in this problem and the exact computation of the Delaunay graph and the Voronoi diagram of spheres. To the best of our knowledge, there does not exist a comprehensive treatment of the exact computation with geometrical invariants of the Delaunay graph and the Voronoi diagram of spheres. Starting from the system of equations defining the zero-dimensional algebraic set of the problem, we are applying Wu's algorithm to transform the initial system into an equivalent Wu characteristic (triangular) set. In the corresponding system of algebraic equations, in each polynomial (except the first one), the variable with higher order from the preceding polynomial has been eliminated (by pseudo-remainder computations) and the last polynomial we obtain is a polynomial of a single variable. By regrouping all the formal coefficients for each monomial in each polynomial, we get polynomials that are invariants for the given problem. We rewrite the original system by replacing the invariant polynomials by new formal coefficients. We repeat the process until all the algebraic relationships (syzygies) between the invariants have been found by applying Wu's algorithm on the invariants. Finally, we present an incremental algorithm for the construction of Voronoi diagrams and Delaunay graphs of spheres in 3D and its application to Geodesy.

We revisit a new type of Voronoi diagram, in which distance is measured from a point to a pair of points. We consider a few more such distance functions, based on geometric primitives, namely, circles and triangles, and analyze the structure and complexity of the nearest- and furthest-neighbor 2-site Voronoi diagrams of a point set in the plane with respect to these distance functions. In addition, we bring to notice that 2-point site Voronoi diagrams can be alternatively interpreted as 1-site Voronoi diagrams of segments, and thus, our results also enhance the knowledge on the latter.

We introduce a new, substantially simplified version of the toggling-branching recurrence operation of computability logic, prove its equivalence to Japaridze's old, "canonical" version, and also prove that both versions preserve the static property of their arguments.

In this paper, we present a general model for Arabic bank check processing indicating the major phases of a check processing system. We then survey the available databases for Arabic bank check processing research. The state of the art in the different phases of Arabic bank check processing is surveyed (i.e., pre-processing, check analysis and segmentation, features extraction, and legal and courtesy amounts recognition). The open issues for future research are stated and areas that need improvements are presented. To the best of our knowledge, it is the first survey of Arabic bank check processing.

Time-series discord is widely used in data mining applications to characterize anomalous subsequences in time series. Compared to some other discord search algorithms, the direct search algorithm based on the recurrence plot shows the advantage of being fast and parameter free. The direct search algorithm, however, relies on quasi-periodicity in input time series, an assumption that limits the algorithm's applicability. In this paper, we eliminate the periodicity assumption from the direct search algorithm by proposing a reference function for subsequences and a new sampling strategy based on the reference function. These measures result in a new algorithm with improved efficiency and robustness, as evidenced by our empirical evaluation.

Generally, abnormal points (noise and outliers) cause cluster analysis to produce low accuracy especially in fuzzy clustering. These data not only stay in clusters but also deviate the centroids from their true positions. Traditional fuzzy clustering like Fuzzy C-Means (FCM) always assigns data to all clusters which is not reasonable in some circumstances. By reformulating objective function in exponential equation, the algorithm aggressively selects data into the clusters. However noisy data and outliers cannot be properly handled by clustering process therefore they are forced to be included in a cluster because of a general probabilistic constraint that the sum of the membership degrees across all clusters is one. In order to improve this weakness, possibilistic approach relaxes this condition to improve membership assignment. Nevertheless, possibilistic clustering algorithms generally suffer from coincident clusters because their membership equations ignore the distance to other clusters. Although there are some possibilistic clustering approaches that do not generate coincident clusters, most of them require the right combination of multiple parameters for the algorithms to work. In this paper, we theoretically study Possibilistic Exponential Fuzzy Clustering (PXFCM) that integrates possibilistic approach with exponential fuzzy clustering. PXFCM has only one parameter and not only partitions the data but also filters noisy data or detects them as outliers. The comprehensive experiments show that PXFCM produces high accuracy in both clustering results and outlier detection without generating coincident problems.

An innovative and uniform framework based on a combination of Gabor wavelets with principal component analysis (PCA) and multiple discriminant analysis (MDA) is presented in this paper. In this framework, features are extracted from the optimal random image components using greedy approach. These feature vectors are then projected to subspaces for dimensionality reduction which is used for solving linear problems. The design of Gabor filters, PCA and MDA are crucial processes used for facial feature extraction. The FERET, ORL and YALE face databases are used to generate the results. Experiments show that optimal random image component selection (ORICS) plus MDA outperforms ORICS and subspace projection approach such as ORICS plus PCA. Our method achieves 96.25%, 99.44% and 100% recognition accuracy on the FERET, ORL and YALE databases for 30% training respectively. This is a considerably improved performance compared with other standard methodologies described in the literature.

Event detection is one of the major applications of wireless sensor networks (WSNs). Most of existing medium access control (MAC) protocols are mainly optimized for the situation under which an event only generates one packet on a single sensor node. When an event generates multiple packets on a single node, the performance of these MAC protocols degrades rapidly. In this paper, we present a new synchronous duty-cycle MAC protocol called SR-MAC for the event detection applications in which multiple packets are generated on a single node. SR-MAC introduces a new scheduling mechanism that reserves few time slots during the SLEEP period for the nodes to transmit multiple packets. By this approach, SR-MAC can schedule multiple packets generated by an event on a single node to be forwarded over multiple hops in one operational cycle without collision. We use event delivery latency (EDL) and event delivery ratio (EDR) to measure the event detection capability of the SR-MAC protocol. Through detailed ns-2 simulation, the results show that SR-MAC can achieve lower EDL, higher EDR and higher network throughput with guaranteed energy efficiency compared with R-MAC, DW-MAC and PR-MAC.

Cooperative communication for wireless networks has gained a lot of recent interest due to its ability to mitigate fading with exploration of spatial diversity. In this paper, we study a joint optimization problem of jointly considering transmission mode selection, relay assignment and power allocation to maximize the capacity of the network through cooperative wireless communications. This problem is much more challenging than relay assignment considered in literature work which simply targets to maximize the transmission capacity for a single transmission pair. We formulate the problem as a variation of the maximum weight matching problem where the weight is a function over power values which must meet power constraints (VMWMC). Although VMWMC is a non-convex problem whose complexity increases exponentially with the number of relay nodes, we show that the duality gap of VMWMC is virtual zero. Based on this result, we propose a solution using Lagrange dual decomposition to reduce the computation complexity. We do simulations to evaluate the performance of the proposed solution. The results show that our solution can achieve maximum network capacity with much less computation time compared with exhaustive search, and our solution outperforms existing sub-optimal solutions that can only achieve much lower network capacity.

Addressing the problem of queue scheduling for the packet-switched system is a vital aspect of congestion control. In this paper, the fuzzy logic based decision method is adopted for queue scheduling in order to enforce some level of control for traffic of different quality of service requirements using predetermined values. The fuzzy scheduler proposed in this paper takes into account the dynamic nature of the Internet traffic with respect to its time-varying packet arrival process that affects the network states and performance. Three queues are defined, viz low, medium and high priority queues. The choice of prioritizing packets in皍ences how queues are served. The fuzzy scheduler not only utilizes queue priority in the queue scheduling scheme, but also considers packet drop susceptibility and queue limit. Through simulation it is shown that the fuzzy scheduler is more appropriate for the dynamic nature of Internet traffic in a packet-switched system as compared with some existing queue scheduling methods. Results show that the scheduling strategy of the proposed fuzzy scheduler reduces packet drop, provides good link utilization and minimizes queue delay as compared with the priority queuing (PQ), first-in-first-out (FIFO), and weighted fair queuing (WFQ).

In this paper, we focus on efficient processing of XML keyword queries based on smallest lowest common ancestor (SLCA) semantics. For a given query Q with m keywords, we propose to use stable matches as the basis for SLCA computation, where each stable match M consists of m nodes that belong to the m distinct keyword inverted lists of Q. M satisfies that no other lowest common ancestor (LCA) node of Q can be found to be located after the first node of M and be a descendant of the LCA of M, based on which the operation of locating a stable match can skip more useless nodes. We propose two stable match based algorithms for SLCA computation, i.e., BSLCA and HSLCA. BSLCA processes two keyword inverted lists each time from the shortest to the longest, while HSLCA processes all keyword inverted lists in a holistic way to avoid the problem of redundant computation invoked by BSLCA. Our extensive experimental results verify the performance advantages of our methods according to various evaluation metrics.

Keyword query has attracted much research attention due to its simplicity and wide applications. The inherent ambiguity of keyword query is prone to unsatisfied query results. Moreover some existing techniques on Web query, keyword query in relational databases and XML databases cannot be completely applied to keyword query in dataspaces. So we propose KeymanticES, a novel keyword-based semantic entity search mechanism in dataspaces which combines both keyword query and semantic query features. And we focus on query intent disambiguation problem and propose a novel three-step approach to resolve it. Extensive experimental results show the effectiveness and correctness of our proposed approach.

Electronic communication service providers are obliged to retain communication data for a certain amount of time by their local laws. The retained communication data or the communication logs are used in various applications such as crime detection, viral marketing, analytical study, and so on. Many of these applications rely on effective techniques for analyzing communication logs. In this paper, we focus on measuring the proximity between two communication entities, which is a fundamental and important step toward further analysis of communication logs, and propose a new proximity measure called ESP (Efficient and Spam-Robust Proximity measure). Our proposed measure considers only the (graph- theoretically) shortest paths between two entities and gives small values to those between spam-like entities and others. Thus, it is not only computationally efficient but also spam-robust. By conducting several experiments on real and synthetic datasets, we show that our proposed proximity measure is more accurate, computationally efficient and spam-robust than the existing measures in most cases.