OpenRaiser/Intern-Atlas huggingface dataset:
A Finite Exact Representation of Register Automata Configurations
Venue: arXiv cs.FL 2014
Year: 2014

A register automaton is a finite automaton with finitely many registers ranging from an infinite alphabet. Since the valuations of registers are infinite, there are infinitely many configurations. We describe a technique to classify infinite register automata configurations into finitely many exact representative configurations. Using the finitary representation, we give an algorithm solving the reachability problem for register automata. We moreover define a computation tree logic for register automata and solve its model checking problem.
Synthesis of Parametric Programs using Genetic Programming and Model Checking
Venue: arXiv cs.SE 2014
Year: 2014

Formal methods apply algorithms based on mathematical principles to enhance the reliability of systems. It would only be natural to try to progress from verification, model checking or testing a system against its formal specification into constructing it automatically. Classical algorithmic synthesis theory provides interesting algorithms but also alarming high complexity and undecidability results. The use of genetic programming, in combination with model checking and testing, provides a powerful heuristic to synthesize programs. The method is not completely automatic, as it is fine tuned by a user that sets up the specification and parameters. It also does not guarantee to always succeed and converge towards a solution that satisfies all the required properties. However, we applied it successfully on quite nontrivial examples and managed to find solutions to hard programming challenges, as well as to improve and to correct code. We describe here several versions of our method for synthesizing sequential and concurrent systems.
An Improved Interactive Streaming Algorithm for the Distinct Elements Problem
Venue: arXiv cs.CC 2014
Year: 2014

The exact computation of the number of distinct elements (frequency moment $F_0$) is a fundamental problem in the study of data streaming algorithms. We denote the length of the stream by $n$ where each symbol is drawn from a universe of size $m$. While it is well known that the moments $F_0,F_1,F_2$ can be approximated by efficient streaming algorithms, it is easy to see that exact computation of $F_0,F_2$ requires space $Ω(m)$. In previous work, Cormode et al. therefore considered a model where the data stream is also processed by a powerful helper, who provides an interactive proof of the result. They gave such protocols with a polylogarithmic number of rounds of communication between helper and verifier for all functions in NC. This number of rounds $\left(O(\log^2 m) \;\text{in the case of} \;F_0 \right)$ can quickly make such protocols impractical. Cormode et al. also gave a protocol with $\log m +1$ rounds for the exact computation of $F_0$ where the space complexity is $O\left(\log m \log n+\log^2 m\right)$ but the total communication $O\left(\sqrt{n}\log m\left(\log n+ \log m \right)\right)$. They managed to give $\log m$ round protocols with $\operatorname{polylog}(m,n)$ complexity for many other interesting problems including $F_2$, Inner product, and Range-sum, but computing $F_0$ exactly with polylogarithmic space and communication and $O(\log m)$ rounds remained open. In this work, we give a streaming interactive protocol with $\log m$ rounds for exact computation of $F_0$ using $O\left(\log m \left(\,\log n + \log m \log\log m\,\right)\right)$ bits of space and the communication is $O\left( \log m \left(\,\log n +\log^3 m (\log\log m)^2 \,\right)\right)$. The update time of the verifier per symbol received is $O(\log^2 m)$.
Outlier Detection using Improved Genetic K-means
Venue: arXiv cs.LG 2014
Year: 2014

The outlier detection problem in some cases is similar to the classification problem. For example, the main concern of clustering-based outlier detection algorithms is to find clusters and outliers, which are often regarded as noise that should be removed in order to make more reliable clustering. In this article, we present an algorithm that provides outlier detection and data clustering simultaneously. The algorithmimprovesthe estimation of centroids of the generative distribution during the process of clustering and outlier discovery. The proposed algorithm consists of two stages. The first stage consists of improved genetic k-means algorithm (IGK) process, while the second stage iteratively removes the vectors which are far from their cluster centroids.
Lower Bounds for Approximate LDC
Venue: arXiv cs.CC 2014
Year: 2014

We study an approximate version of $q$-query LDCs (Locally Decodable Codes) over the real numbers and prove lower bounds on the encoding length of such codes. A $q$-query $(α,δ)$-approximate LDC is a set $V$ of $n$ points in $\mathbb{R}^d$ so that, for each $i \in [d]$ there are $Ω(δn)$ disjoint $q$-tuples $(\vec{u}_1,\ldots,\vec{u}_q) $ in $V$ so that $\text{span}(\vec{u}_1,\ldots,\vec{u}_q)$ contains a unit vector whose $i$'th coordinate is at least $α$. We prove exponential lower bounds of the form $n \geq 2^{Ω(αδ\sqrt{d})}$ for the case $q=2$ and, in some cases, stronger bounds (exponential in $d$).
Rapid AkNN Query Processing for Fast Classification of Multidimensional Data in the Cloud
Venue: arXiv cs.DB 2014
Year: 2014

A $k$-nearest neighbor ($k$NN) query determines the $k$ nearest points, using distance metrics, from a specific location. An all $k$-nearest neighbor (A$k$NN) query constitutes a variation of a $k$NN query and retrieves the $k$ nearest points for each point inside a database. Their main usage resonates in spatial databases and they consist the backbone of many location-based applications and not only (i.e. $k$NN joins in databases, classification in data mining). So, it is very crucial to develop methods that answer them efficiently. In this work, we propose a novel method for classifying multidimensional data using an A$k$NN algorithm in the MapReduce framework. Our approach exploits space decomposition techniques for processing the classification procedure in a parallel and distributed manner. To our knowledge, we are the first to study the classification of multidimensional objects under this perspective. Through an extensive experimental evaluation we prove that our solution is efficient and scalable in processing the given queries. We investigate many different perspectives that can affect the total computational cost, such as different dataset distributions, number of dimensions, growth of $k$ value and granularity of space decomposition and prove that our system is efficient, robust and scalable.
The Wiselib TupleStore: A Modular RDF Database for the Internet of Things
Venue: arXiv cs.DB 2014
Year: 2014

The Internet of Things movement provides self-configuring and universally interoperable devices. While such devices are often built with a specific application in mind, they often turn out to be useful in other contexts as well. We claim that by describing the devices' knowledge in a universal way, IoT devices can become first-class citizens in the Internet. They can then exchange data between heterogeneous hardware, different applications and large data sources on the Web. Our key idea --- in contrast to most existing approaches --- is to not restrict the domain of knowledge that can be expressed on the device in any way and, at the same time, allow this knowledge to be machine-understandable and linkable across different locations. We propose an architecture that allows to connect embedded devices to the Semantic Web by expressing their knowledge in the Resource Description Framework (RDF). We present the Wiselib TupleStore, a modular embedded database tailored specifically for the storage of RDF. The Wiselib TupleStore is portable to many platforms including Contiki and TinyOS and allows a variety of trade-offs, making it able to scale to a large variety of hardware scenarios. We discuss the applicability of RDF to heterogeneous resource-constrained devices and compare our system to the existing embedded tuple stores Antelope and TeenyLIME.
An Information Theoretic Charachterization of Channel Shortening Receivers
Venue: arXiv cs.IT 2014
Year: 2014

Optimal data detection of data transmitted over a linear channel can always be implemented through the Viterbi algorithm (VA). However, in many cases of interest the memory of the channel prohibits application of the VA. A popular and conceptually simple method in this case, studied since the early 70s, is to first filter the received signal in order to shorten the memory of the channel, and then to apply a VA that operates with the shorter memory. We shall refer to this as a channel shortening (CS) receiver. Although studied for almost four decades, an information theoretic understanding of what such a simple receiver solution is actually doing is not available. In this paper we will show that an optimized CS receiver is implementing the chain rule of mutual information, but only up to the shortened memory that the receiver is operating with. Further, we will show that the tools for analyzing the ensuing achievable rates from an optimized CS receiver are precisely the same as those used for analyzing the achievable rates of a minimum mean square error (MMSE) receiver.
A Machine Learning Model for Stock Market Prediction
Venue: arXiv cs.CE 2014
Year: 2014

Stock market prediction is the act of trying to determine the future value of a company stock or other financial instrument traded on a financial exchange.
Link-Reliability Based Two-Hop Routing for Wireless Sensor Networks
Venue: arXiv cs.NI 2014
Year: 2014

Wireless Sensor Networks (WSNs) emerge as underlying infrastructures for new classes of large scale net- worked embedded systems. However, WSNs system designers must fulfill the Quality-of-Service (QoS) requirements imposed by the applications (and users). Very harsh and dynamic physical environments and extremely limited energy/computing/memory/communication node resources are major obstacles for satisfying QoS metrics such as reliability, timeliness and system lifetime. The limited communication range of WSN nodes, link asymmetry and the characteristics of the physical environment lead to a major source of QoS degradation in WSNs. This paper proposes a Link Reliability based Two-Hop Routing protocol for wireless Sensor Networks (WSNs). The protocol achieves to reduce packet deadline miss ratio while consid- ering link reliability, two-hop velocity and power efficiency and utilizes memory and computational effective methods for estimating the link metrics. Numerical results provide insights that the protocol has a lower packet deadline miss ratio and longer sensor network lifetime. The results show that the proposed protocol is a feasible solution to the QoS routing problem in wireless sensor networks that support real-time applications.
Dynamic Decision Process Modeling and Relation-line Handling in Distributed Cooperative Modeling System
Venue: arXiv cs.AI 2014
Year: 2014

The Distributed Cooperative Modeling System (DCMS) solves complex decision problems involving a lot of participants with different viewpoints by network based distributed modeling and multi-template aggregation. This thesis aims at extending the system with support for dynamic decision making process. First, the thesis presents a discussion of characteristics and optimal policy finding Markov Decision Process as well as a brief introduction to dynamic Bayesian decision network, which is inherently equal to MDP. After that, discussion and implementation of prediction in Markov process for both discrete and continuous random variable are given, as well as several different kinds of correlation analysis among multiple indices which could help decision-makers to realize the interaction of indices and design appropriate policy. Appending history data of Macau industry, as the foundation of extending DCMS, is introduced. Additional works include rearrangement of graphical class hierarchy in DCMS, which in turn allows convenient implementation of curve relation-line, which makes template modeling clearer and friendlier.
Semantic Annotation and Search for Educational Resources Supporting Distance Learning
Venue: arXiv cs.IR 2014
Year: 2014

Multimedia educational resources play an important role in education, particularly for distance learning environments. With the rapid growth of the multimedia web, large numbers of education articles video resources are increasingly being created by several different organizations. It is crucial to explore, share, reuse, and link these educational resources for better e-learning experiences. Most of the video resources are currently annotated in an isolated way, which means that they lack semantic connections. Thus, providing the facilities for annotating these video resources is highly demanded. These facilities create the semantic connections among video resources and allow their metadata to be understood globally. Adopting Linked Data technology, this paper introduces a video annotation and browser platform with two online tools: Notitia and Sansu-Wolke. Notitia enables users to semantically annotate video resources using vocabularies defined in the Linked Data cloud. Sansu-Wolke allows users to browse semantically linked educational video resources with enhanced web information from different online resources. In the prototype development, the platform uses existing video resources for education articles. The result of the initial development demonstrates the benefits of applying Linked Data technology in the aspects of reusability, scalability, and extensibility
Robust Nonlinear L2 Filtering of Uncertain Lipschitz Systems via Pareto Optimization
Venue: arXiv cs.SY 2014
Year: 2014

A new approach for robust Hinfty filtering for a class of Lipschitz nonlinear systems with time-varying uncertainties both in the linear and nonlinear parts of the system is proposed in an LMI framework. The admissible Lipschitz constant of the system and the disturbance attenuation level are maximized simultaneously through convex multiobjective optimization. The resulting Hinfty filter guarantees asymptotic stability of the estimation error dynamics with exponential convergence and is robust against nonlinear additive uncertainty and time-varying parametric uncertainties. Explicit bounds on the nonlinear uncertainty are derived based on norm-wise and element-wise robustness analysis.
A Novel Approach for Computing Dynamic Slices of Aspect-Oriented Programs
Venue: arXiv cs.SE 2014
Year: 2014

We propose a dynamic slicing algorithm to compute the slices of aspect-oriented programs. We use a dependence based intermediate program representation called Aspect System Dependence Graph (AOSG) to represent aspect-oriented programs. Then, we propose the dynamic slicing algorithm for AOPs, which is an extended version of EMDS algorithm for object-oriented programs. Our algorithm is based on marking and unmarking of the edges of AOSG appropriately during runtime.
Size Adaptive Region Based Huffman Compression Technique
Venue: arXiv cs.IT 2014
Year: 2014

A loss-less compression technique is proposed which uses a variable length Region formation technique to divide the input file into a number of variable length regions. Huffman codes are obtained for entire file after formation of regions. Symbols of each region are compressed one by one. Comparisons are made among proposed technique, Region Based Huffman compression technique and classical Huffman technique. The proposed technique offers better compression ratio for some files than other two.
Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction
Venue: arXiv cs.LO 2014
Year: 2014

We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.
Decentralized Hybrid Formation Control of Unmanned Aerial Vehicles
Venue: arXiv cs.SY 2014
Year: 2014

This paper presents a decentralized hybrid supervisory control approach for a team of unmanned helicopters that are involved in a leader-follower formation mission. Using a polar partitioning technique, the motion dynamics of the follower helicopters are abstracted to finite state machines. Then, a discrete supervisor is designed in a modular way for different components of the formation mission including reaching the formation, keeping the formation, and collision avoidance. Furthermore, a formal technique is developed to design the local supervisors decentralizedly, so that the team of helicopters as whole, can cooperatively accomplish a collision-free formation task.
Design and Performance Evaluation of an Optimized Disk Scheduling Algorithm (ODSA)
Venue: arXiv cs.OS 2014
Year: 2014

Management of disk scheduling is a very important aspect of operating system. Performance of the disk scheduling completely depends on how efficient is the scheduling algorithm to allocate services to the request in a better manner. Many algorithms (FIFO, SSTF, SCAN, C-SCAN, LOOK, etc.) are developed in the recent years in order to optimize the system disk I/O performance. By reducing the average seek time and transfer time, we can improve the performance of disk I/O operation. In our proposed algorithm, Optimize Disk Scheduling Algorithm (ODSA) is taking less average seek time and transfer time as compare to other disk scheduling algorithms (FIFO, SSTF, SCAN, C-SCAN, LOOK, etc.), which enhances the efficiency of the disk performance in a better manner.
Hybrid evolving clique-networks and their communicability
Venue: arXiv cs.SI 2014
Year: 2014

Aiming to understand real-world hierarchical networks whose degree distributions are neither power law nor exponential, we construct a hybrid clique network that includes both homogeneous and inhomogeneous parts, and introduce an inhomogeneity parameter to tune the ratio between the homogeneous part and the inhomogeneous one. We perform Monte-Carlo simulations to study various properties of such a network, including the degree distribution, the average shortest-path-length, the clustering coefficient, the clustering spectrum, and the communicability.
Efficient Representation for Online Suffix Tree Construction
Venue: arXiv cs.DS 2014
Year: 2014

Suffix tree construction algorithms based on suffix links are popular because they are simple to implement, can operate online in linear time, and because the suffix links are often convenient for pattern matching. We present an approach using edge-oriented suffix links, which reduces the number of branch lookup operations (known to be a bottleneck in construction time) with some additional techniques to reduce construction cost. We discuss various effects of our approach and compare it to previous techniques. An experimental evaluation shows that we are able to reduce construction time to around half that of the original algorithm, and about two thirds that of previously known branch-reduced construction.
Face Recognition Methods & Applications
Venue: arXiv cs.CV 2014
Year: 2014

Face recognition presents a challenging problem in the field of image analysis and computer vision. The security of information is becoming very significant and difficult. Security cameras are presently common in airports, Offices, University, ATM, Bank and in any locations with a security system. Face recognition is a biometric system used to identify or verify a person from a digital image. Face Recognition system is used in security. Face recognition system should be able to automatically detect a face in an image. This involves extracts its features and then recognize it, regardless of lighting, expression, illumination, ageing, transformations (translate, rotate and scale image) and pose, which is a difficult task. This paper contains three sections. The first section describes the common methods like holistic matching method, feature extraction method and hybrid methods. The second section describes applications with examples and finally third section describes the future research directions of face recognition.
Distributed Cooperative Localization in Wireless Sensor Networks without NLOS Identification
Venue: arXiv cs.NI 2014
Year: 2014

In this paper, a 2-stage robust distributed algorithm is proposed for cooperative sensor network localization using time of arrival (TOA) data without identification of non-line of sight (NLOS) links. In the first stage, to overcome the effect of outliers, a convex relaxation of the Huber loss function is applied so that by using iterative optimization techniques, good estimates of the true sensor locations can be obtained. In the second stage, the original (non-relaxed) Huber cost function is further optimized to obtain refined location estimates based on those obtained in the first stage. In both stages, a simple gradient descent technique is used to carry out the optimization. Through simulations and real data analysis, it is shown that the proposed convex relaxation generally achieves a lower root mean squared error (RMSE) compared to other convex relaxation techniques in the literature. Also by doing the second stage, the position estimates are improved and we can achieve an RMSE close to that of the other distributed algorithms which know \textit{a priori} which links are in NLOS.
Limits to the scope of applicability of extended formulations for LP models of combinatorial optimization problems: A summary
Venue: arXiv cs.CC 2014
Year: 2014

We show that new definitions of the notion of "projection" on which some of the recent "extended formulations" works (such as Kaibel (2011); Fiorini et al. (2011; 2012); Kaibel and Walter (2013); Kaibel and Weltge (2013) for example) have been based can cause those works to over-reach in their conclusions in relating polytopes to one another when the sets of the descriptive variables for those polytopes are disjoint.
Unconstrained Online Linear Learning in Hilbert Spaces: Minimax Algorithms and Normal Approximations
Venue: arXiv cs.LG 2014
Year: 2014

We study algorithms for online linear optimization in Hilbert spaces, focusing on the case where the player is unconstrained. We develop a novel characterization of a large class of minimax algorithms, recovering, and even improving, several previous results as immediate corollaries. Moreover, using our tools, we develop an algorithm that provides a regret bound of $\mathcal{O}\Big(U \sqrt{T \log(U \sqrt{T} \log^2 T +1)}\Big)$, where $U$ is the $L_2$ norm of an arbitrary comparator and both $T$ and $U$ are unknown to the player. This bound is optimal up to $\sqrt{\log \log T}$ terms. When $T$ is known, we derive an algorithm with an optimal regret bound (up to constant factors). For both the known and unknown $T$ case, a Normal approximation to the conditional value of the game proves to be the key analysis tool.
Free Applicative Functors
Venue: arXiv cs.PL 2014
Year: 2014

Applicative functors are a generalisation of monads. Both allow the expression of effectful computations into an otherwise pure language, like Haskell. Applicative functors are to be preferred to monads when the structure of a computation is fixed a priori. That makes it possible to perform certain kinds of static analysis on applicative values. We define a notion of free applicative functor, prove that it satisfies the appropriate laws, and that the construction is left adjoint to a suitable forgetful functor. We show how free applicative functors can be used to implement embedded DSLs which can be statically analysed.