OpenRaiser/Intern-Atlas huggingface dataset:
Application of Constacyclic codes to Quantum MDS Codes
Venue: arXiv cs.IT 2014
Year: 2014

Quantum maximal-distance-separable (MDS) codes form an important class of quantum codes. To get $q$-ary quantum MDS codes, it suffices to find linear MDS codes $C$ over $\mathbb{F}_{q^2}$ satisfying $C^{\perp_H}\subseteq C$ by the Hermitian construction and the quantum Singleton bound. If $C^{\perp_{H}}\subseteq C$, we say that $C$ is a dual-containing code. Many new quantum MDS codes with relatively large minimum distance have been produced by constructing dual-containing constacyclic MDS codes (see \cite{Guardia11}, \cite{Kai13}, \cite{Kai14}). These works motivate us to make a careful study on the existence condition for nontrivial dual-containing constacyclic codes. This would help us to avoid unnecessary attempts and provide effective ideas in order to construct dual-containing codes. Several classes of dual-containing MDS constacyclic codes are constructed and their parameters are computed. Consequently, new quantum MDS codes are derived from these parameters. The quantum MDS codes exhibited here have parameters better than the ones available in the literature.
Heuristic-based Optimal Resource Provisioning in Application-centric Cloud
Venue: arXiv cs.DC 2014
Year: 2014

Cloud Service Providers (CSPs) adapt different pricing models for their offered services. Some of the models are suitable for short term requirement while others may be suitable for the Cloud Service User's (CSU) long term requirement. In this paper, we look at the problem of finding the amount of resources to be reserved to satisfy the CSU's long term demands with the aim of minimizing the total cost. Finding the optimal resource requirement to satisfy the the CSU's demand for resources needs sufficient research effort. Various algorithms were discussed in the last couple of years for finding the optimal resource requirement but most of them are based on IPP which is NP in nature. In this paper, we derive some heuristic-based polynomial time algorithms to find some near optimal solution to the problem. We show that the cost for CSU using our approach is comparable to the solution obtained using optimal Integer Programming Problem(IPP).
HoTT formalisation in Coq: Dependency Graphs \& ML4PG
Venue: arXiv cs.LO 2014
Year: 2014

This note is a response to Bas Spitter's email of 28 February 2014 about ML4PG: "We (Jason actually) are adding dependency graphs to our HoTT library: https://github.com/HoTT/HoTT/wiki I seem to recall that finding the dependency graph was a main obstacle preventing machine learning to be used in Coq. However, you seem to have made progress on this. What tool are you using? https://anne.pacalet.fr/dev/dpdgraph/ ? Or another tool? Would it be easy to use your ML4PG on the HoTT library?" This note gives explanation of how ML4PG can be used in the HoTT library and how ML4PG relates to the two kinds of Dependency graphs available in Coq.
An Approach for Discovering Traceability Links between Regulatory Documents and Source Code Through User-Interface Labels
Venue: arXiv cs.SE 2014
Year: 2014

In application domains that are regulated, software vendors must maintain traceability links between the regulatory items and the code base implementing them. In this paper, we present a traceability approach based on the intuition that the regulatory documents and the user-interface of the corresponding software applications are very close. First, they use the same terminology. Second, most important regulatory pieces of information appear in the graphical user-interface because the end-users in those application domains care about the regulation (by construction). We evaluate our approach in the domain of green building. The evaluation involves a domain expert, lead architect of a commercial product within this area. The evaluation shows that the recovered traceability links are accurate.
Flying Insect Classification with Inexpensive Sensors
Venue: arXiv cs.LG 2014
Year: 2014

The ability to use inexpensive, noninvasive sensors to accurately classify flying insects would have significant implications for entomological research, and allow for the development of many useful applications in vector control for both medical and agricultural entomology. Given this, the last sixty years have seen many research efforts on this task. To date, however, none of this research has had a lasting impact. In this work, we explain this lack of progress. We attribute the stagnation on this problem to several factors, including the use of acoustic sensing devices, the over-reliance on the single feature of wingbeat frequency, and the attempts to learn complex models with relatively little data. In contrast, we show that pseudo-acoustic optical sensors can produce vastly superior data, that we can exploit additional features, both intrinsic and extrinsic to the insect's flight behavior, and that a Bayesian classification approach allows us to efficiently learn classification models that are very robust to over-fitting. We demonstrate our findings with large scale experiments that dwarf all previous works combined, as measured by the number of insects and the number of species considered.
Transformation von Scade-Modellen zur SMT-basierten Verifikation
Venue: arXiv cs.LO 2014
Year: 2014

In this work we develop a fully automatic verification procedure of safety properties of Scade programs. We transform each such program into an SMT instance (Satisfiability Modulo Theories) and feed this to a solver. The goal is to have a publicly accessible experimentation platform for the verification of Scade programs. The choice of SMT is determined by the fact that it offers more expressive logics than propositional logic, yet their solvers have been shown to perform very well. The expressiveness of SMT logics allows us to implement symbolic model checking thus avoiding the expansion of the complete state space of the models during the verification. In order to reduce the complexity we transform the Scade programs into SMT instances in two steps. First they are reduced to programs of a synchronous data flow language Lama. This language has simpler semantics than Scade while still preserving some of the programmer's abstractions. Next we interpret such a Lama program as a system of quantifier free first-order formulas. The remaining abstractions in Lama can be used to simplify these systems. This in turn could lead to speeding up the verification process and allowing more properties to be verifiable. We implemented these transformations successfully in a software using Haskell. This work is concluded by a comparison of this software to the existing verification software "Scade Design Verifier" which comes with the Scade Suite.
Zig-zag Sort: A Simple Deterministic Data-Oblivious Sorting Algorithm Running in O(n log n) Time
Venue: arXiv cs.DS 2014
Year: 2014

We describe and analyze Zig-zag Sort--a deterministic data-oblivious sorting algorithm running in O(n log n) time that is arguably simpler than previously known algorithms with similar properties, which are based on the AKS sorting network. Because it is data-oblivious and deterministic, Zig-zag Sort can be implemented as a simple O(n log n)-size sorting network, thereby providing a solution to an open problem posed by Incerpi and Sedgewick in 1985. In addition, Zig-zag Sort is a variant of Shellsort, and is, in fact, the first deterministic Shellsort variant running in O(n log n) time. The existence of such an algorithm was posed as an open problem by Plaxton et al. in 1992 and also by Sedgewick in 1996. More relevant for today, however, is the fact that the existence of a simple data-oblivious deterministic sorting algorithm running in O(n log n) time simplifies the inner-loop computation in several proposed oblivious-RAM simulation methods (which utilize AKS sorting networks), and this, in turn, implies simplified mechanisms for privacy-preserving data outsourcing in several cloud computing applications. We provide both constructive and non-constructive implementations of Zig-zag Sort, based on the existence of a circuit known as an epsilon-halver, such that the constant factors in our constructive implementations are orders of magnitude smaller than those for constructive variants of the AKS sorting network, which are also based on the use of epsilon-halvers.
Delineation of Techniques to implement on the enhanced proposed model using data mining for protein sequence classification
Venue: arXiv cs.DB 2014
Year: 2014

In post genomic era with the advent of new technologies a huge amount of complex molecular data are generated with high throughput. The management of this biological data is definitely a challenging task due to complexity and heterogeneity of data for discovering new knowledge. Issues like managing noisy and incomplete data are needed to be dealt with. Use of data mining in biological domain has made its inventory success. Discovering new knowledge from the biological data is a major challenge in data mining technique. The novelty of the proposed model is its combined use of intelligent techniques to classify the protein sequence faster and efficiently. Use of FFT, fuzzy classifier, String weighted algorithm, gram encoding method, neural network model and rough set classifier in a single model and in an appropriate place can enhance the quality of the classification system.Thus the primary challenge is to identify and classify the large protein sequences in a very fast and easy but intellectual way to decrease the time complexity and space complexity.
Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs
Venue: arXiv cs.FL 2014
Year: 2014

Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from state space explosion. In this paper, we address probabilistic bisimulation to reduce the size of such an MDPs while preserving PCTL properties it satisfies. We discuss different interpretations of uncertainty in the models which are studied in the literature and that result in two different definitions of bisimulations. We give algorithms to compute the quotients of these bisimulations in time polynomial in the size of the model and exponential in the uncertain branching. Finally, we show by a case study that large models in practice can have small branching and that a substantial state space reduction can be achieved by our approach.
Nonuniform Fuchsian codes for noisy channels
Venue: arXiv cs.IT 2014
Year: 2014

We develop a new transmission scheme for additive white Gaussian noisy (AWGN) channels based on Fuchsian groups from rational quaternion algebras. The structure of the proposed Fuchsian codes is nonlinear and nonuniform, hence conventional decoding methods based on linearity and symmetry do not apply. Previously, only brute force decoding methods with complexity that is linear in the code size exist for general nonuniform codes. However, the properly discontinuous character of the action of the Fuchsian groups on the complex upper half-plane translates into decoding complexity that is logarithmic in the code size via a recently introduced point reduction algorithm.
Efficiently inferring community structure in bipartite networks
Venue: arXiv cs.SI 2014
Year: 2014

Bipartite networks are a common type of network data in which there are two types of vertices, and only vertices of different types can be connected. While bipartite networks exhibit community structure like their unipartite counterparts, existing approaches to bipartite community detection have drawbacks, including implicit parameter choices, loss of information through one-mode projections, and lack of interpretability. Here we solve the community detection problem for bipartite networks by formulating a bipartite stochastic block model, which explicitly includes vertex type information and may be trivially extended to $k$-partite networks. This bipartite stochastic block model yields a projection-free and statistically principled method for community detection that makes clear assumptions and parameter choices and yields interpretable results. We demonstrate this model's ability to efficiently and accurately find community structure in synthetic bipartite networks with known structure and in real-world bipartite networks with unknown structure, and we characterize its performance in practical contexts.
Searching in Unstructured Overlays Using Local Knowledge and Gossip
Venue: arXiv cs.DC 2014
Year: 2014

This paper analyzes a class of dissemination algorithms for the discovery of distributed contents in Peer-to-Peer unstructured overlay networks. The algorithms are a mix of protocols employing local knowledge of peers' neighborhood and gossip. By tuning the gossip probability and the depth k of the k-neighborhood of which nodes have information, we obtain different dissemination protocols employed in literature over unstructured P2P overlays. The provided analysis and simulation results confirm that, when properly configured, these schemes represent a viable approach to build effective P2P resource discovery in large-scale, dynamic distributed systems.
Image reconstruction from limited range projections using orthogonal moments
Venue: arXiv cs.CV 2014
Year: 2014

A set of orthonormal polynomials is proposed for image reconstruction from projection data. The relationship between the projection moments and image moments is discussed in detail, and some interesting properties are demonstrated. Simulation results are provided to validate the method and to compare its performance with previous works.
Encapsulating Formal Methods within Domain Specific Languages: A Solution for Verifying Railway Scheme Plans
Venue: arXiv cs.SE 2014
Year: 2014

The development and application of formal methods is a long standing research topic within the field of computer science. One particular challenge that remains is the uptake of formal methods into industrial practices. This paper introduces a methodology for developing domain specific languages for modelling and verification to aid in the uptake of formal methods within industry. It illustrates the successful application of this methodology within the railway domain. The presented methodology addresses issues surrounding faithful modelling, scalability of verification and accessibility to modelling and verification processes for practitioners within the domain.
Formal Analysis of Optical Systems
Venue: arXiv cs.LO 2014
Year: 2014

Optical systems are becoming increasingly important by resolving many bottlenecks in today's communication, electronics, and biomedical systems. However, given the continuous nature of optics, the inability to efficiently analyze optical system models using traditional paper-and-pencil and computer simulation approaches sets limits especially in safety-critical applications. In order to overcome these limitations, we propose to employ higher-order-logic theorem proving as a complement to computational and numerical approaches to improve optical model analysis in a comprehensive framework. The proposed framework allows formal analysis of optical systems at four abstraction levels, i.e., ray, wave, electromagnetic, and quantum.
Improvement of the monotonicity properties of the difference schemes by building in them of the monotonizing operators
Venue: arXiv cs.NA 2014
Year: 2014

The method of monotonization of difference schemes is being considered in the paper. The method was earlier proposed by the author for stationary problems. It is investigated in the paper more profoundly. The idea of the method is to build the monotonizing operators into the schemes so that the balance relations from point to point are not violated. Different monotonizing operators can be used to be installed in the schemes. Propositions concerning approximation and stability of the monotonized schemes are formulated and proved. Also a proposition significant for practical use of the schemes is formulated and proved. The idea is to use the monotonized schemes in the cases when the proposition conditions are fulfilled. The proposition is based on closeness of solutions of the initial and auxiliary schemes. Constructions for solving of time dependent problems are also written in the paper. One dimensional example and three-dimensional hydrodynamic example are considered. The method allows to considerably decrease value of calculations in many cases.
Fulfillment Request Management (The approach)
Venue: arXiv cs.SE 2014
Year: 2014

In this paper we introduce the term FRM (Fulfillment Request Management). According to the FRM in a BSS / OSS environment we can use a unified approach to implement a SOA in order to integrate BSS with OSS and handle 1. Orders 2. Events 3. Processes. So in a way that systems like ESB, Order Management, and Business Process Management can be implemented under a unified architecture and a unified implementation. We assume that all the above mentioned are 'requests' and according to the system we want to implement, the request can be an event, an order, a process etc. So instead of having N systems we have 1 system that covers all the above (ESB, Order Management, BPM etc) With the FRM we can have certain advantages such as: 1. adaptation 2. Interoperability. 3. Re-usability 4. Fast implementation 5. Easy reporting. In this paper we present a set of the main principles in order to build an FRM System.
Non linear Prediction of Antitubercular Activity Of Oxazolines and Oxazoles derivatives Making Use of Compact TS-Fuzzy models Through Clustering with orthogonal least sqaure technique and Fuzzy identification system
Venue: arXiv cs.CE 2014
Year: 2014

The prediction of uncertain and predictive nonlinear systems is an important and challenging problem. Fuzzy logic models are often a good choice to describe such systems however in many cases these become complex soon. commonlly, too less effort is put into descriptor selection and in the creation of suitable local rules. Moreover, in common no model reduction is applied, while this may analyze the model by removing redundant data. This paper suggests a combined method that deal with these issues in order to create compact Takagi Sugeno (TS) models that can be effectively used to represent complex predictive systems. A new fuzzy clustering method is come up with for the identification of compact TS-fuzzy models. The best relevant consequent variables of the TS model are choosen by an orthogonal least squares technique based on the obtained clusters.For the selection of the relevant antecedent (scheduling) variables a new method has been developed based on Fisher's interclass separability basis. This complete approach is demonstrated by means of the Oxazolines and Oxazoles derivatives as antituberculosis agent for nonlinear regression benchmark. The results are compared with results obtained by neuro-fuzzy i.e. ANFIS algorithm and advanced fuzzyy clustering techniques i.e FMID toolbox .
Statistical Decision Making for Optimal Budget Allocation in Crowd Labeling
Venue: arXiv cs.LG 2014
Year: 2014

In crowd labeling, a large amount of unlabeled data instances are outsourced to a crowd of workers. Workers will be paid for each label they provide, but the labeling requester usually has only a limited amount of the budget. Since data instances have different levels of labeling difficulty and workers have different reliability, it is desirable to have an optimal policy to allocate the budget among all instance-worker pairs such that the overall labeling accuracy is maximized. We consider categorical labeling tasks and formulate the budget allocation problem as a Bayesian Markov decision process (MDP), which simultaneously conducts learning and decision making. Using the dynamic programming (DP) recurrence, one can obtain the optimal allocation policy. However, DP quickly becomes computationally intractable when the size of the problem increases. To solve this challenge, we propose a computationally efficient approximate policy, called optimistic knowledge gradient policy. Our MDP is a quite general framework, which applies to both pull crowdsourcing marketplaces with homogeneous workers and push marketplaces with heterogeneous workers. It can also incorporate the contextual information of instances when they are available. The experiments on both simulated and real data show that the proposed policy achieves a higher labeling accuracy than other existing policies at the same budget level.
ARM 7 Based Controller Area Network for Accident Avoidance in Automobiles
Venue: arXiv cs.OH 2014
Year: 2014

Based on requirements of modern vehicle, in- vehicle Controller Area Network (CAN) architecture has been implemented. In order to reduce point to point wiring harness in vehicle automation, CAN is suggested as a means for data communication within the vehicle environment. The benefits of CAN bus based network over traditional point to point schemes will offer increased flexibility and expandability for future technology insertions. This paper describes system which uses sensors to measure various parameters of the car like speed, distance from the other car, presence of alcohol in car and accidental change of lane and sends a warning signal to the driver if any of the parameter goes out of range to avoid accidents . In addition to this if accident occurs in any remote area then using bump sensor accident is detected and SMS is send immediately using GSM. A situation that provides a good example of how the system works is when a driver is about to change lanes, and there is a car in his blind spot. The sensors will detect that car and inform the driver before he starts turning, preventing him from potentially getting into a serious accident.
The Computational Compexity of Decision Problem in Additive Extensions of Nonassociative Lambek Calculus
Venue: arXiv cs.LO 2014
Year: 2014

We analyze the complexity of decision problems for Boolean Nonassociative Lambek Calculus admitting empty antecedent of sequents ($\mathsf{BFNL^*}$), and the consequence relation of Distributive Full Nonassociative Lambek Calculus ($\mathsf{DFNL}$). We construct a polynomial reduction from modal logic $\mathsf{K}$ into $\mathsf{BFNL^*}$. As a consequence, we prove that the decision problem for $\mathsf{BFNL^*}$ is PSPACE-hard. We also prove that the same result holds for the consequence relation of DFNL, by reducing $\mathsf{BFNL^*}$ in polynomial time to DFNL enriched with finite set of assumptions. Finally, we prove analogous results for variants of $\mathsf{BFNL^*}$, including $\mathsf{BFNL^*e}$ ($\mathsf{BFNL^*}$ with exchange), modal extensions of $\mathsf{BFNL^*_i}$ and $\mathsf{BFNL^*_{ei}}$ for $i \in \{\mathsf{K}, \mathsf{T}, \mathsf{K4}, \mathsf{S4}, \mathsf{S5}\}$.
Sentiment Analysis by Using Fuzzy Logic
Venue: arXiv cs.IR 2014
Year: 2014

How could a product or service is reasonably evaluated by anyone in the shortest time? A million dollar question but it is having a simple answer: Sentiment analysis. Sentiment analysis is consumers review on products and services which helps both the producers and consumers (stakeholders) to take effective and efficient decision within a shortest period of time. Producers can have better knowledge of their products and services through the sentiment analysis (ex. positive and negative comments or consumers likes and dislikes) which will help them to know their products status (ex. product limitations or market status). Consumers can have better knowledge of their interested products and services through the sentiment analysis (ex. positive and negative comments or consumers likes and dislikes) which will help them to know their deserving products status (ex. product limitations or market status). For more specification of the sentiment values, fuzzy logic could be introduced. Therefore, sentiment analysis with the help of fuzzy logic (deals with reasoning and gives closer views to the exact sentiment values) will help the producers or consumers or any interested person for taking the effective decision according to their product or service interest.