OpenRaiser/Intern-Atlas huggingface dataset:
Real-Time Rate-Distortion Optimized Streaming of Wireless Video
Venue: arXiv cs.NI 2014
Year: 2014

Mobile cyberphysical systems have received considerable attention over the last decade, as communication, computing and control come together on a common platform. Understanding the complex interactions that govern the behavior of large complex cyberphysical systems is not an easy task. The goal of this paper is to address this challenge in the particular context of multimedia delivery over an autonomous aerial vehicle (AAV) network. Bandwidth requirements and stringent delay constraints of real-time video streaming, paired with limitations on computational complexity and power consumptions imposed by the underlying implementation platform, make cross-layer and cross-domain co-design approaches a necessity. In this paper, we propose a novel, low-complexity rate-distortion optimized (RDO) algorithms specifically targeted at video streaming over mobile embedded networks. We test the performance of our RDO algorithms using a network of AAVs both in simulation and implementation.
Shape-from-intrinsic operator
Venue: arXiv cs.CV 2014
Year: 2014

Shape-from-X is an important class of problems in the fields of geometry processing, computer graphics, and vision, attempting to recover the structure of a shape from some observations. In this paper, we formulate the problem of shape-from-operator (SfO), recovering an embedding of a mesh from intrinsic differential operators defined on the mesh. Particularly interesting instances of our SfO problem include synthesis of shape analogies, shape-from-Laplacian reconstruction, and shape exaggeration. Numerically, we approach the SfO problem by splitting it into two optimization sub-problems that are applied in an alternating scheme: metric-from-operator (reconstruction of the discrete metric from the intrinsic operator) and embedding-from-metric (finding a shape embedding that would realize a given metric, a setting of the multidimensional scaling problem).
Two-dimensional Sentiment Analysis of text
Venue: arXiv cs.IR 2014
Year: 2014

Sentiment Analysis aims to get the underlying viewpoint of the text, which could be anything that holds a subjective opinion, such as an online review, Movie rating, Comments on Blog posts etc. This paper presents a novel approach that classify text in two-dimensional Emotional space, based on the sentiments of the author. The approach uses existing lexical resources to extract feature set, which is trained using Supervised Learning techniques.
Platform-Centric Android Monitoring---Modular and Efficient
Venue: arXiv cs.SE 2014
Year: 2014

We present an add-on for the Android platform, capable of intercepting nearly all interactions between apps or apps with the platform, including arguments of method invocations in a human-readable format. A preliminary performance evaluation shows that the performance penalty of our solution is roughly comparable with similar tools in that area. The advantage of our solution, however, is that it is truly modular in the sense that we do not actually modify the Android platform itself, and can include it even with an already running system. Possible uses of such an add-on are manifold; we discuss one from the area of runtime verification that aims at improving system security.
Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types
Venue: arXiv cs.LO 2014
Year: 2014

In this paper, we present an Agda formalization of a normalizer for simply-typed lambda terms. The normalizer consists of two coinductively defined functions in the delay monad: One is a standard evaluator of lambda terms to closures, the other a type-directed reifier from values to eta-long beta-normal forms. Their composition, normalization-by-evaluation, is shown to be a total function a posteriori, using a standard logical-relations argument. The successful formalization serves as a proof-of-concept for coinductive programming and reasoning using sized types and copatterns, a new and presently experimental feature of Agda.
ClassSpy: Java Object Pattern Visualization Tool
Venue: arXiv cs.PL 2014
Year: 2014

Modern java programs consist of large number of classes as well as vast amount of objects instantiated during program execution. Software developers are always keen to know the number of objects created for each class. This information is helpful for a developer in understanding the packages/classes of a program and optimizing their code. However, understanding such a vast amount of information is not a trivial task. Visualization helps to depict this information on a single screen and to comprehend it efficiently. This paper presents a visualization approach that depicts information about all the objects instantiated during the program execution. The proposed technique is more space efficient and scalable to handle vast datasets, at the same time helpful to identify the key program components. This easy to use interface provides user an environment to glimpse the entire objects on a single screen. The proposed approach allows sorting objects at class, thread and method levels. Effectiveness and usability of the proposed approach is shown through case studies.
A bio-inspired algorithm for fuzzy user equilibrium problem by aid of Physarum Polycephalum
Venue: arXiv cs.AI 2014
Year: 2014

The user equilibrium in traffic assignment problem is based on the fact that travelers choose the minimum-cost path between every origin-destination pair and on the assumption that such a behavior will lead to an equilibrium of the traffic network. In this paper, we consider this problem when the traffic network links are fuzzy cost. Therefore, a Physarum-type algorithm is developed to unify the Physarum network and the traffic network for taking full of advantage of Physarum Polycephalum's adaptivity in network design to solve the user equilibrium problem. Eventually, some experiments are used to test the performance of this method. The results demonstrate that our approach is competitive when compared with other existing algorithms.
Rescue Robotics in Bore well Environment
Venue: arXiv cs.RO 2014
Year: 2014

A technique for rescue task in bore well environment has been proposed. India is facing a distressed cruel situation where in the previous years a number of child deaths have been reported falling in the bore well. As the diameter of the bore well is quiet narrow for any adult person and the lights goes dark inside it, the rescue task in those situations is a challenging task. Here we are proposing a robotic system which will attach a harness to the child using pneumatic arms for picking up. A teleconferencing system will also be attached to the robot for communicating with the child.
Euclidean TSP with few inner points in linear space
Venue: arXiv cs.DS 2014
Year: 2014

Given a set of $n$ points in the Euclidean plane, such that just $k$ points are strictly inside the convex hull of the whole set, we want to find the shortest tour visiting every point. The fastest known algorithm for the version when $k$ is significantly smaller than $n$, i.e., when there are just few inner points, works in $O(k^{11\sqrt{k}} k^{1.5} n^{3})$ time [Knauer and Spillner, WG 2006], but also requires space of order $k^{c\sqrt{k}}n^{2}$. The best linear space algorithm takes $O(k! k n)$ time [Deineko, Hoffmann, Okamoto, Woeginer, Oper. Res. Lett. 34(1), 106-110]. We construct a linear space $O(nk^2+k^{O(\sqrt{k})})$ time algorithm. The new insight is extending the known divide-and-conquer method based on planar separators with a matching-based argument to shrink the instance in every recursive call. This argument also shows that the problem admits a quadratic bikernel.
Tableaux for Dynamic Logic of Propositional Assignments
Venue: arXiv cs.LO 2014
Year: 2014

The Dynamic Logic for Propositional Assignments (DL-PA) has recently been studied as an alternative to Propositional Dynamic Logic (PDL). In DL-PA, the abstract atomic programs of PDL are replaced by assignments of propositional variables to truth values. This makes DL-PA enjoy some interesting meta-logical properties that PDL does not, such as eliminability of the Kleene star, compactness and interpolation. We define and analytic tableaux calculus for DL-PA and show that it matches the known complexity results.
Memristor models for machine learning
Venue: arXiv cs.LG 2014
Year: 2014

In the quest for alternatives to traditional CMOS, it is being suggested that digital computing efficiency and power can be improved by matching the precision to the application. Many applications do not need the high precision that is being used today. In particular, large gains in area- and power efficiency could be achieved by dedicated analog realizations of approximate computing engines. In this work, we explore the use of memristor networks for analog approximate computation, based on a machine learning framework called reservoir computing. Most experimental investigations on the dynamics of memristors focus on their nonvolatile behavior. Hence, the volatility that is present in the developed technologies is usually unwanted and it is not included in simulation models. In contrast, in reservoir computing, volatility is not only desirable but necessary. Therefore, in this work, we propose two different ways to incorporate it into memristor simulation models. The first is an extension of Strukov's model and the second is an equivalent Wiener model approximation. We analyze and compare the dynamical properties of these models and discuss their implications for the memory and the nonlinear processing capacity of memristor networks. Our results indicate that device variability, increasingly causing problems in traditional computer design, is an asset in the context of reservoir computing. We conclude that, although both models could lead to useful memristor based reservoir computing systems, their computational performance will differ. Therefore, experimental modeling research is required for the development of accurate volatile memristor models.
Industrial-Strength Documentation for ACL2
Venue: arXiv cs.SE 2014
Year: 2014

The ACL2 theorem prover is a complex system. Its libraries are vast. Industrial verification efforts may extend this base with hundreds of thousands of lines of additional modeling tools, specifications, and proof scripts. High quality documentation is vital for teams that are working together on projects of this scale. We have developed XDOC, a flexible, scalable documentation tool for ACL2 that can incorporate the documentation for ACL2 itself, the Community Books, and an organization's internal formal verification projects, and which has many features that help to keep the resulting manuals up to date. Using this tool, we have produced a comprehensive, publicly available ACL2+Books Manual that brings better documentation to all ACL2 users. We have also developed an extended manual for use within Centaur Technology that extends the public manual to cover Centaur's internal books. We expect that other organizations using ACL2 will wish to develop similarly extended manuals.
Distilling Abstract Machines (Long Version)
Venue: arXiv cs.PL 2014
Year: 2014

It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between big-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in call-by-name, call-by-value, and call-by-need, catching many machines in the literature. We start by distilling the KAM, the CEK, and the ZINC, and then provide simplified versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we also introduce some new machines with global environments. Moreover, we show that distillation preserves the time complexity of the executions, i.e. the LSC is a complexity-preserving abstraction of abstract machines.
Controller selection in a Wireless Mesh SDN under network partitioning and merging scenarios
Venue: arXiv cs.NI 2014
Year: 2014

In this paper we consider a Wireless Mesh Network (WMN) integrating SDN principles. The Wireless Mesh Routers (WMR) are OpenFlow capable switches that can be controlled by SDN controllers, according to the wmSDN (wireless mesh SDN) architecture that we have introduced in a previous work. We consider the issue of controller selection in a scenario with intermittent connectivity. We assume that over time a single WMN can become split in two or more partitions and that separate partitions can merge into a larger one. We assume that a set of SDN controllers can potentially take control of the WMRs. At a given time only one controller should be the master of a WMR and it should be the most appropriate one according to some metric. We argue that the state of the art solutions for "master election" among distributed controllers are not suitable in a mesh networking environment, as they could easily be affected by inconsistencies. We envisage a "master selection" approach which is under the control of each WMR, and guarantees that at a given time only one controller will be master of a WMR. We designed a specific master selection procedure which is very simple in terms of the control logic to be executed in the WMR. We have implemented the proposed solution and deployed it over a network emulator (CORE) and over the combination of two physical wireless testbeds (NITOS and wiLab.t).
On Importance of Steganographic Cost For Network Steganography
Venue: arXiv cs.MM 2014
Year: 2014

Network steganography encompasses the information hiding techniques that can be applied in communication network environments and that utilize hidden data carriers for this purpose. In this paper we introduce a characteristic called steganographic cost which is an indicator for the degradation or distortion of the carrier caused by the application of the steganographic method. Based on exemplary cases for single- and multi-method steganographic cost analyses we observe that it can be an important characteristic that allows to express hidden data carrier degradation - similarly as MSE (Mean-Square Error) or PSNR (Peak Signal-to-Noise Ratio) are utilized for digital media steganography. Steganographic cost can moreover be helpful to analyse the relationships between two or more steganographic methods applied to the same hidden data carrier.
Faithful Glitch Propagation in Binary Circuit Models
Venue: arXiv cs.OH 2014
Year: 2014

Modern digital circuit design relies on fast digital timing simulation tools and, hence, on accurate binary-valued circuit models that faithfully model signal propagation, even throughout a complex design. Unfortunately, it was recently proved [Függer et al., ASYNC'13] that no existing binary-valued circuit model proposed so far, including the two most commonly used pure and inertial delay channels, faithfully captures glitch propagation: For the simple Short-Pulse Filtration (SPF) problem, which is related to a circuit's ability to suppress a single glitch, we showed that the quite broad class of bounded single-history channels either contradict the unsolvability of SPF in bounded time or the solvability of SPF in unbounded time in physical circuits. In this paper, we propose a class of binary circuit models that do not suffer from this deficiency: Like bounded single-history channels, our involution channels involve delays that may depend on the time of the previous output transition. Their characteristic property are delay functions which are based on involutions, i.e., functions that form their own inverse. A concrete example of such a delay function, which is derived from a generalized first-order analog circuit model, reveals that this is not an unrealistic assumption. We prove that, in sharp contrast to what is possible with bounded single-history channels, SPF cannot be solved in bounded time due to the nonexistence of a lower bound on the delay of involution channels, whereas it is easy to provide an unbounded SPF implementation. It hence follows that binary-valued circuit models based on involution channels allow to solve SPF precisely when this is possible in physical circuits. To the best of our knowledge, our model is hence the very first candidate for a model that indeed guarantees faithful glitch propagation.
A Flexible Fitness Function for Community Detection in Complex Networks
Venue: arXiv cs.NE 2014
Year: 2014

Most community detection algorithms from the literature work as optimization tools that minimize a given \textit{fitness function}, while assuming that each node belongs to a single community. Since there is no hard concept of what a community is, most proposed fitness functions focus on a particular definition. As such, these functions do not always lead to partitions that correspond to those observed in practice. This paper proposes a new flexible fitness function that allows the identification of communities with distinct characteristics. Such flexibility was evaluated through the adoption of an immune-inspired optimization algorithm, named cob-aiNet[C], to identify both disjoint and overlapping communities in a set of benchmark networks. The results have shown that the obtained partitions are much closer to the ground-truth than those obtained by the optimization of the modularity function.
Identification of Orchid Species Using Content-Based Flower Image Retrieval
Venue: arXiv cs.CV 2014
Year: 2014

In this paper, we developed the system for recognizing the orchid species by using the images of flower. We used MSRM (Maximal Similarity based on Region Merging) method for segmenting the flower object from the background and extracting the shape feature such as the distance from the edge to the centroid point of the flower, aspect ratio, roundness, moment invariant, fractal dimension and also extract color feature. We used HSV color feature with ignoring the V value. To retrieve the image, we used Support Vector Machine (SVM) method. Orchid is a unique flower. It has a part of flower called lip (labellum) that distinguishes it from other flowers even from other types of orchids. Thus, in this paper, we proposed to do feature extraction not only on flower region but also on lip (labellum) region. The result shows that our proposed method can increase the accuracy value of content based flower image retrieval for orchid species up to $\pm$ 14%. The most dominant feature is Centroid Contour Distance, Moment Invariant and HSV Color. The system accuracy is 85,33% in validation phase and 79,33% in testing phase.
Integer Vector Addition Systems with States
Venue: arXiv cs.FL 2014
Year: 2014

This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Although it is folklore that reachability in ZVASS is NP-complete, it turns out that despite their naturalness, from a complexity point of view this class has received little attention in the literature. We fill this gap by providing an in-depth analysis of the computational complexity of the aforementioned decision problems. Most interestingly, it turns out that while the addition of reset operations to ordinary VASS leads to undecidability and Ackermann-hardness of reachability and coverability, respectively, they can be added to ZVASS while retaining NP-completness of both coverability and reachability.
Simulation based Hardness Evaluation of a Multi-Objective Genetic Algorithm
Venue: arXiv cs.NE 2014
Year: 2014

Studies have shown that multi-objective optimization problems are hard problems. Such problems either require longer time to converge to an optimum solution, or may not converge at all. Recently some researchers have claimed that real culprit for increasing the hardness of multi-objective problems are not the number of objectives themselves rather it is the increased size of solution set, incompatibility of solutions, and high probability of finding suboptimal solution due to increased number of local maxima. In this work, we have setup a simple framework for the evaluation of hardness of multi-objective genetic algorithms (MOGA). The algorithm is designed for a pray-predator game where a player is to improve its lifespan, challenging level and usability of the game arena through number of generations. A rigorous set of experiments are performed for quantifying the hardness in terms of evolution for increasing number of objective functions. In genetic algorithm, crossover and mutation with equal probability are applied to create offspring in each generation. First, each objective function is maximized individually by ranking the competing players on the basis of the fitness (cost) function, and then a multi-objective cost function (sum of individual cost functions) is maximized with ranking, and also without ranking where dominated solutions are also allowed to evolve.
Merge Path - A Visually Intuitive Approach to Parallel Merging
Venue: arXiv cs.DC 2014
Year: 2014

Merging two sorted arrays is a prominent building block for sorting and other functions. Its efficient parallelization requires balancing the load among compute cores, minimizing the extra work brought about by parallelization, and minimizing inter-thread synchronization requirements. Efficient use of memory is also important. We present a novel, visually intuitive approach to partitioning two input sorted arrays into pairs of contiguous sequences of elements, one from each array, such that 1) each pair comprises any desired total number of elements, and 2) the elements of each pair form a contiguous sequence in the output merged sorted array. While the resulting partition and the computational complexity are similar to those of certain previous algorithms, our approach is different, extremely intuitive, and offers interesting insights. Based on this, we present a synchronization-free, cache-efficient merging (and sorting) algorithm. While we use a shared memory architecture as the basis, our algorithm is easily adaptable to additional architectures. In fact, our approach is even relevant to cache-efficient sequential sorting. The algorithms are presented, along with important cache-related insights.
Linear Non-Transitive Temporal Logic, Knowledge Operations, Algorithms for Admissibility
Venue: arXiv cs.LO 2014
Year: 2014

The paper studies problems of satisfiability, decidability and admissibility of inference rules, conceptions of knowledge and agent's knowledge in non-transitive temporal linear logic LTL(Past,m). We find algorithms solving mentioned problems, justify our approach to consider linear non-transitive time with several examples. Main, most complicated, technical new result is decidability of LTL(Past,m) w.r.t. admissible rules. We discuss several ways to formalize conceptions of knowledge and agent's knowledge within given approach in non-transitive linear logic with models directed to past.