OpenRaiser/Intern-Atlas huggingface dataset:
Capturing Hiproofs in HOL Light
Venue: arXiv cs.LO 2013
Year: 2013

Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used to abstract away from details, or to label particular portions to explain their purpose. In this paper we present two complementary methods for capturing hiproofs in HOL Light, along with a tool to produce web-based visualisations. The first method uses tactic recording, by modifying tactics to record their arguments and construct a hierarchical tree; this allows a tactic proof script to be modified. The second method uses proof recording, which extends the HOL Light kernel to record hierachical proof trees alongside theorems. This method is less invasive, but requires care to manage the size of the recorded objects. We have implemented both methods, resulting in two systems: Tactician and HipCam.
Computer Simulation of 3-D Finite-Volume Liquid Transport in Fibrous Materials: a Physical Model for Ink Seepage into Paper
Venue: arXiv cs.CE 2013
Year: 2013

A physical model for the simulation ink/paper interaction at the mesoscopic scale is developed. It is based on the modified Ising model, and is generalized to consider the restriction of the finite-volume of ink and also its dynamic seepage. This allows the model to obtain the ink distribution within the paper volume. At the mesoscopic scale, the paper is modeled using a discretized fiber structure. The ink distribution is obtained by solving its equivalent optimization problem, which is solved using a modified genetic algorithm, along with a new boundary condition and the quasi-linear technique. The model is able to simulate the finite-volume distribution of ink.
Polar Coded Modulation with Optimal Constellation Labeling
Venue: arXiv cs.IT 2013
Year: 2013

A practical $2^m$-ary polar coded modulation (PCM) scheme with optimal constellation labeling is proposed. To efficiently find the optimal labeling rule, the search space is reduced by exploiting the symmetry properties of the channels. Simulation results show that the proposed PCM scheme can outperform the bit-interleaved turbo coded modulation scheme used in the WCDMA (Wideband Code Division Multiple Access) mobile communication systems by up to 1.5dB.
A Constant Factor Approximation Algorithm for Fault-Tolerant k-Median
Venue: arXiv cs.DS 2013
Year: 2013

In this paper, we consider the fault-tolerant $k$-median problem and give the \emph{first} constant factor approximation algorithm for it. In the fault-tolerant generalization of classical $k$-median problem, each client $j$ needs to be assigned to at least $r_j \ge 1$ distinct open facilities. The service cost of $j$ is the sum of its distances to the $r_j$ facilities, and the $k$-median constraint restricts the number of open facilities to at most $k$. Previously, a constant factor was known only for the special case when all $r_j$s are the same, and a logarithmic approximation ratio for the general case. In addition, we present the first polynomial time algorithm for the fault-tolerant $k$-median problem on a path or a HST by showing that the corresponding LP always has an integral optimal solution. We also consider the fault-tolerant facility location problem, where the service cost of $j$ can be a weighted sum of its distance to the $r_j$ facilities. We give a simple constant factor approximation algorithm, generalizing several previous results which only work for nonincreasing weight vectors.
Image Denoising Using Tensor Product Complex Tight Framelets with Increasing Directionality
Venue: arXiv cs.IT 2013
Year: 2013

Tensor product real-valued wavelets have been employed in many applications such as image processing with impressive performance. Though edge singularities are ubiquitous and play a fundamental role in two-dimensional problems, tensor product real-valued wavelets are known to be only sub-optimal since they can only capture edges well along the coordinate axis directions. The dual tree complex wavelet transform (DTCWT), proposed by Kingsbury [16] and further developed by Selesnick et al. [24], is one of the most popular and successful enhancements of the classical tensor product real-valued wavelets. The two-dimensional DTCWT is obtained via tensor product and offers improved directionality with 6 directions. In this paper we shall further enhance the performance of DTCWT for the problem of image denoising. Using framelet-based approach and the notion of discrete affine systems, we shall propose a family of tensor product complex tight framelets TPCTF_n for all integers n>2 with increasing directionality, where n refers to the number of filters in the underlying one-dimensional complex tight framelet filter bank. For dimension two, such tensor product complex tight framelet TPCTF_n offers (n-1)(n-3)/2+4 directions when n is odd, and (n-4)(n+2)/2+6 directions when n is even. In particular, TPCTF_4, which is different to DTCWT in both nature and design, provides an alternative to DTCWT. Indeed, TPCTF_4 behaves quite similar to DTCWT by offering 6 directions in dimension two, employing the tensor product structure, and enjoying slightly less redundancy than DTCWT. When TPCTF_4 is applied to image denoising, its performance is comparable to DTCWT. Moreover, better results on image denoising can be obtained by using TPCTF_6. Moreover, TPCTF_n allows us to further improve DTCWT by using TPCTF_n as the first stage filter bank in DTCWT.
Framework for Ubiquitous Social Networks
Venue: arXiv cs.CY 2013
Year: 2013

This paper presents a novel framework for ubiquitous social networks (USNs). Instead of making virtual connections, on the basis of human social networks, an effort has been made to facilitate interactions among human social networks with the help of virtual social networks. The imperative domains that support ubiquitous social networks are highlighted and different scenarios are provided to project real world applications of proposed framework. Our proposed framework can provide preliminary foundations for creating ubiquitous social networks in true essence.
Soft Computing Framework for Routing in Wireless Mesh Networks: An Integrated Cost Function Approach
Venue: arXiv cs.NI 2013
Year: 2013

Dynamic behaviour of a WMN imposes stringent constraints on the routing policy of the network. In the shortest path based routing the shortest paths needs to be evaluated within a given time frame allowed by the WMN dynamics. The exact reasoning based shortest path evaluation methods usually fail to meet this rigid requirement. Thus, requiring some soft computing based approaches which can replace "best for sure" solutions with "good enough" solutions. This paper proposes a framework for optimal routing in the WMNs; where we investigate the suitability of Big Bang-Big Crunch (BB-BC), a soft computing based approach to evaluate shortest/near-shortest path. In order to make routing optimal we first propose to replace distance between the adjacent nodes with an integrated cost measure that takes into account throughput, delay, jitter and residual energy of a node. A fuzzy logic based inference mechanism evaluates this cost measure at each node. Using this distance measure we apply BB-BC optimization algorithm to evaluate shortest/near shortest path to update the routing tables periodically as dictated by network requirements. A large number of simulations were conducted and it has been observed that BB-BC algorithm appears to be a high potential candidate suitable for routing in WMNs.
QuickXsort: Efficient Sorting with n log n - 1.399n +o(n) Comparisons on Average
Venue: arXiv cs.DS 2013
Year: 2013

In this paper we generalize the idea of QuickHeapsort leading to the notion of QuickXsort. Given some external sorting algorithm X, QuickXsort yields an internal sorting algorithm if X satisfies certain natural conditions. With QuickWeakHeapsort and QuickMergesort we present two examples for the QuickXsort-construction. Both are efficient algorithms that incur approximately n log n - 1.26n +o(n) comparisons on the average. A worst case of n log n + O(n) comparisons can be achieved without significantly affecting the average case. Furthermore, we describe an implementation of MergeInsertion for small n. Taking MergeInsertion as a base case for QuickMergesort, we establish a worst-case efficient sorting algorithm calling for n log n - 1.3999n + o(n) comparisons on average. QuickMergesort with constant size base cases shows the best performance on practical inputs: when sorting integers it is slower by only 15% to STL-Introsort.
The technology of using a data warehouse to support decision-making in health care
Venue: arXiv cs.DB 2013
Year: 2013

This paper describes the technology of data warehouse in healthcare decision-making and tools for support of these technologies, which is used to cancer diseases. The healthcare executive managers and doctors needs information about and insight into the existing health data, so as to make decision more efficiently without interrupting the daily work of an On-Line Transaction Processing (OLTP) system. This is a complex problem during the healthcare decision-making process. To solve this problem, the building a healthcare data warehouse seems to be efficient. First in this paper we explain the concepts of the data warehouse, On-Line Analysis Processing (OLAP). Changing the data in the data warehouse into a multidimensional data cube is then shown. Finally, an application example is given to illustrate the use of the healthcare data warehouse specific to cancer diseases developed in this study. The executive managers and doctors can view data from more than one perspective with reduced query time, thus making decisions faster and more comprehensive.
Linking Correlated Network Flows through Packet Timing: a Game-Theoretic Approach
Venue: arXiv cs.CR 2013
Year: 2013

Deciding that two network flows are essentially the same is an important problem in intrusion detection or in tracing anonymous connections. A stepping stone or an anonymity network may try to prevent flow correlation by delaying the packets, introducing chaff traffic, or even splitting the flow in several subflows. We introduce a game-theoretic framework for this problem. The framework is used to derive the Nash equilibrium under two different adversary models: the first one, when the adversary is limited to delaying packets, and the second, when the adversary also adds dummy packets and removes packets from the flow. As the optimal decoder is not computationally feasible, we restrict the possible decoder to one that estimates and compensates the attack. Our analysis can be used for understanding the limits of flow correlation based on packet timings under an active attacker.
Performance Comparison of Packet Scheduling Algorithms for Video Traffic in LTE Cellular Network
Venue: arXiv cs.NI 2013
Year: 2013

In this paper we have studied downlink packet scheduling algorithms proposed for LTE cellular networks. The study emphasize on three most promising scheduling algorithms such as: FLS, EXP rule and LOG rule. The performance of these three algorithms is conducted over video traffic in a vehicular environment using LTE-Sim simulator. The simulation was setup with varying number of users from 10 - 60 in fixed bounded regions of 1 km radius. The main goal this study is to provide results that will help in the design process of packet scheduler for LTE cellular networks, aiming to get better overall performance users. Simulation results show that, the FLS scheme outperforms in terms of average system throughput, average packet delay, PLR; and with a satisfactory level of fairness index.
Engaging with mental health: a global challenge
Venue: arXiv cs.HC 2013
Year: 2013

Using the metrics of the World Health Organisation, the Global Burden of Disease Study has found that mental health difficulties are currently the leading cause of disability in developed countries [1]. Projections also indicate that the global burden of mental health difficulties will continue to rise in the coming decades. The human and economic costs of this trend will be substantial. In this paper we discuss how effectively designed interactive systems, developed through collaborative, interdisciplinary efforts, can play a significant role in helping to address this challenge. Our discussion is grounded in a description of four exploratory systems, each of which has undergone initial clinical evaluations. Directions for future research on mental health technologies are also identified.
Alias and Change Calculi, Applied to Frame Inference
Venue: arXiv cs.PL 2013
Year: 2013

Alias analysis, which determines whether two expressions in a program may reference to the same object, has many potential applications in program construction and verification. We have developed a theory for alias analysis, the "alias calculus", implemented its application to an object-oriented language, and integrated the result into a modern IDE. The calculus has a higher level of precision than many existing alias analysis techniques. One of the principal applications is to allow automatic change analysis, which leads to inferring "modifies clauses", providing a significant advance towards addressing the Frame Problem. Experiments were able to infer the "modifies" clauses of an existing formally specified library. Other applications, in particular to concurrent programming, also appear possible. The article presents the calculus, the application to frame analysis including ex-perimental results, and other projected applications. The ongoing work includes building more efficient model capturing aliasing properties and soundness proof for its essential elements.
Certification of Bounds of Non-linear Functions: the Templates Method
Venue: arXiv cs.SC 2013
Year: 2013

The aim of this work is to certify lower bounds for real-valued multivariate functions, defined by semialgebraic or transcendental expressions. The certificate must be, eventually, formally provable in a proof system such as Coq. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of inequalities. We introduce an approximation algorithm, which combines ideas of the max-plus basis method (in optimal control) and of the linear templates method developed by Manna et al. (in static analysis). This algorithm consists in bounding some of the constituents of the function by suprema of quadratic forms with a well chosen curvature. This leads to semialgebraic optimization problems, solved by sum-of-squares relaxations. Templates limit the blow up of these relaxations at the price of coarsening the approximation. We illustrate the efficiency of our framework with various examples from the literature and discuss the interfacing with Coq.
Fuzzy Fibers: Uncertainty in dMRI Tractography
Venue: arXiv cs.CV 2013
Year: 2013

Fiber tracking based on diffusion weighted Magnetic Resonance Imaging (dMRI) allows for noninvasive reconstruction of fiber bundles in the human brain. In this chapter, we discuss sources of error and uncertainty in this technique, and review strategies that afford a more reliable interpretation of the results. This includes methods for computing and rendering probabilistic tractograms, which estimate precision in the face of measurement noise and artifacts. However, we also address aspects that have received less attention so far, such as model selection, partial voluming, and the impact of parameters, both in preprocessing and in fiber tracking itself. We conclude by giving impulses for future research.
Unsupervised Gene Expression Data using Enhanced Clustering Method
Venue: arXiv cs.CE 2013
Year: 2013

Microarrays are made it possible to simultaneously monitor the expression profiles of thousands of genes under various experimental conditions. Identification of co-expressed genes and coherent patterns is the central goal in microarray or gene expression data analysis and is an important task in bioinformatics research. Feature selection is a process to select features which are more informative. It is one of the important steps in knowledge discovery. The problem is that not all features are important. Some of the features may be redundant, and others may be irrelevant and noisy. In this work the unsupervised Gene selection method and Enhanced Center Initialization Algorithm (ECIA) with K-Means algorithms have been applied for clustering of Gene Expression Data. This proposed clustering algorithm overcomes the drawbacks in terms of specifying the optimal number of clusters and initialization of good cluster centroids. Gene Expression Data show that could identify compact clusters with performs well in terms of the Silhouette Coefficients cluster measure.
Evaluating a healthcare data warehouse for cancer diseases
Venue: arXiv cs.DB 2013
Year: 2013

This paper presents the evaluation of the architecture of healthcare data warehouse specific to cancer diseases. This data warehouse containing relevant cancer medical information and patient data. The data warehouse provides the source for all current and historical health data to help executive manager and doctors to improve the decision making process for cancer patients. The evaluation model based on Bill Inmon's definition of data warehouse is proposed to evaluate the Cancer data warehouse.
Refining Data Security in Infrastructure Networks Support of Multipath Routing
Venue: arXiv cs.DC 2013
Year: 2013

An infrastructure network is a self-organizing network with help of Access Point (AP) of wireless links connecting nodes to another. The nodes can communicate without an ad hoc. They form an uninformed topology (BSS/ESS), where the nodes play the role of routers and are free to move randomly. Infrastructure networks proved their efficiency being used in different fields but they are highly vulnerable to security attacks and dealing with this is one of the main challenges of these networks at present. In recent times some clarification are proposed to provide authentication, confidentiality, availability, secure routing and intrusion avoidance in infrastructure networks. Implementing security in such dynamically changing networks is a hard task. Infrastructure network characteristics should be taken into consideration to be clever to design efficient solutions. Here we spotlight on civilizing the flow transmission privacy in infrastructure networks based on multipath routing. Certainly, we take benefit of the being of multiple paths between nodes in an infrastructure network to increase the confidentiality robustness of transmitted data with the help of Access Point. In our approach the original message to secure is split into shares through access point that are encrypted and combined then transmitted along different disjointed existing paths between sender and receiver. Even if an intruder achieve something to get one or more transmitted distribute the likelihood that the unique message will be reconstituted is very squat.
Learning an Integrated Distance Metric for Comparing Structure of Complex Networks
Venue: arXiv cs.SI 2013
Year: 2013

Graph comparison plays a major role in many network applications. We often need a similarity metric for comparing networks according to their structural properties. Various network features - such as degree distribution and clustering coefficient - provide measurements for comparing networks from different points of view, but a global and integrated distance metric is still missing. In this paper, we employ distance metric learning algorithms in order to construct an integrated distance metric for comparing structural properties of complex networks. According to natural witnesses of network similarities (such as network categories) the distance metric is learned by the means of a dataset of some labeled real networks. For evaluating our proposed method which is called NetDistance, we applied it as the distance metric in K-nearest-neighbors classification. Empirical results show that NetDistance outperforms previous methods, at least 20 percent, with respect to precision.
A Nobel Defence Scheme Against Selfish Node Attack in MANET
Venue: arXiv cs.NI 2013
Year: 2013

Security is one of the major issue in wired and wireless network but due to the presence of centralized administration not difficult to find out misbehavior in network other than in Mobile Ad hoc Network due to the absence of centralized management and frequently changes in topology security is one of a major issue in MANET. Only prevention methods for attack are not enough. In this paper a new Intrusion Detection System (IDS) algorithm has proposed against selfish node attack to secure MANET. Here the behavior of selfish node is unnecessary flooding the information in network and block all types of packets transferring between the reliable nodes. Proposed IDS Algorithm identifies the behavior of selfish node and also blocked their misbehavior activities. In case of selfish node attack network performance is almost negligible but after applying IDS on attack network performance is enhanced up to 92% and provides 0% Infection rate from attack.
Partition Function of the Ising Model via Factor Graph Duality
Venue: arXiv cs.IT 2013
Year: 2013

The partition function of a factor graph and the partition function of the dual factor graph are related to each other by the normal factor graph duality theorem. We apply this result to the classical problem of computing the partition function of the Ising model. In the one-dimensional case, we thus obtain an alternative derivation of the (well-known) analytical solution. In the two-dimensional case, we find that Monte Carlo methods are much more efficient on the dual graph than on the original graph, especially at low temperature.
Where in the Internet is congestion?
Venue: arXiv cs.NI 2013
Year: 2013

Understanding the distribution of congestion in the Internet is a long-standing problem. Using data from the SamKnows US broadband access network measurement study, commissioned by the FCC, we explore patterns of congestion distribution in DSL and cable Internet service provider (ISP) networks. Using correlation-based analysis we estimate prevalence of congestion in the periphery versus the core of ISP networks. We show that there are significant differences in congestion levels and its distribution between DSL and cable ISP networks and identify bottleneck sections in each type of network.
Numerical LTL Synthesis for Cyber-Physical Systems
Venue: arXiv cs.SE 2013
Year: 2013

Cyber-physical systems (CPS) are systems that interact with the physical world via sensors and actuators. In such a system, the reading of a sensor represents measures of a physical quantity, and sensor values are often reals ranged over bounded intervals. The implementation of control laws is based on nonlinear numerical computations over the received sensor values. Synthesizing controllers fulfilling features within CPS brings a huge challenge to the research community in formal methods, as most of the works in automatic controller synthesis (LTL synthesis) are restricted to specifications having a few discrete inputs within the Boolean domain. In this report, we present a novel approach that addresses the above challenge to synthesize controllers for CPS. Our core methodology, called numerical LTL synthesis, extends LTL synthesis by using inputs or outputs in real numbers and by allowing predicates of polynomial constraints to be defined within an LTL formula as specification. The synthesis algorithm is based on an interplay between an LTL synthesis engine which handles the pseudo-Boolean structure, together with a nonlinear constraint validity checker which tests the (in)feasibility of a (counter-)strategy. The methodology is integrated within the CPS research framework Ptolemy II via the development of an LTL synthesis module G4LTL and a validity checker JBernstein. Although we only target the theory of nonlinear real arithmetic, the use of pseudo-Boolean synthesis framework also allows an easy extension to embed a richer set of theories, making the technique applicable to a much broader audience.