OpenRaiser/Intern-Atlas huggingface dataset:
Algorithmic Analysis of Edge Ranking and Profiling for MTF Determination of an Imaging System
Venue: arXiv cs.CV 2015
Year: 2015

Edge detection is one of the most principal techniques for detecting discontinuities in the gray levels of image pixels. The Modulation Transfer Function (MTF) is one of the main criteria for assessing imaging quality and is a parameter frequently used for measuring the sharpness of an imaging system. In order to determine the MTF, it is essential to determine the best edge from the target image so that an edge profile can be developed and then the line spread function and hence the MTF, can be computed accordingly. For regular image sizes, the human visual system is adept enough to identify suitable edges from the image. But considering huge image datasets, such as those obtained from satellites, the image size may range in few gigabytes and in such a case, manual inspection of images for determination of the best suitable edge is not plausible and hence, edge profiling tasks have to be automated. This paper presents a novel, yet simple, algorithm for edge ranking and detection from image data-sets for MTF computation, which is ideal for automation on vectorised graphical processing units.
Workspace and Singularity analysis of a Delta like family robot
Venue: arXiv cs.RO 2015
Year: 2015

Workspace and joint space analysis are essential steps in describing the task and designing the control loop of the robot, respectively. This paper presents the descriptive analysis of a family of delta-like parallel robots by using algebraic tools to induce an estimation about the complexity in representing the singularities in the workspace and the joint space. A Gr{ö}bner based elimination is used to compute the singularities of the manipulator and a Cylindrical Algebraic Decomposition algorithm is used to study the workspace and the joint space. From these algebraic objects, we propose some certified three dimensional plotting describing the the shape of workspace and of the joint space which will help the engineers or researchers to decide the most suited configuration of the manipulator they should use for a given task. Also, the different parameters associated with the complexity of the serial and parallel singularities are tabulated, which further enhance the selection of the different configuration of the manipulator by comparing the complexity of the singularity equations.
Noisy Network Coding with Partial DF
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we propose a noisy network coding integrated with partial decode-and-forward relaying for single-source multicast discrete memoryless networks (DMN's). Our coding scheme generalizes the partial-decode-compress-and-forward scheme (Theorem 7) by Cover and El Gamal. This is the first time the theorem is generalized for DMN's such that each relay performs both partial decode-and-forward and compress-and-forward simultaneously. Our coding scheme simultaneously generalizes both noisy network coding by Lim, Kim, El Gamal, and Chung and distributed decode-and-forward by Lim, Kim, and Kim. It is not trivial to combine the two schemes because of inherent incompatibility in their encoding and decoding strategies. We solve this problem by sending the same long message over multiple blocks at the source and at the same time by letting the source find the auxiliary covering indices that carry information about the message simultaneously over all blocks.
Expansion Coding for Channel and Source Coding
Venue: arXiv cs.IT 2015
Year: 2015

A general method of coding over expansion is proposed,which allows one to reduce the highly non-trivial problems of coding over analog channels and compressing analog sources to a set of much simpler subproblems, coding over discrete channels and compressing discrete sources. More specifically, the focus of this paper is on the additive exponential noise (AEN) channel, and lossy compression of exponential sources. Taking advantage of the essential decomposable property of these channels (sources), the proposed expansion method allows for mapping of these problems to coding over parallel channels (respectively, sources), where each level is modeled as an independent coding problem over discrete alphabets. Any feasible solution to the resulting optimization problem after expansion corresponds to an achievable scheme of the original problem. Utilizing this mapping, even for the cases where the optimal solutions are difficult to characterize, it is shown that the expansion coding scheme still performs well with appropriate choices of parameters. More specifically, theoretical analysis and numerical results reveal that expansion coding achieves the capacity of AEN channel in the high SNR regime. It is also shown that for lossy compression, the achievable rate distortion pair by expansion coding approaches to the Shannon limit in the low distortion region. Remarkably, by using capacity-achieving codes with low encoding and decoding complexity that are originally designed for discrete alphabets, for instance polar codes, the proposed expansion coding scheme allows for designing low-complexity analog channel and source codes.
Semantic Degrees for Industrie 4.0
Venue: arXiv cs.SE 2015
Year: 2015

Under the context of Industrie 4.0 (I4.0), future production systems provide balanced operations between manufacturing flexibility and efficiency, realized in an autonomous, horizontal, and decentralized item-level production control framework. Structured interoperability via precise formulations on an appropriate degree is crucial to achieve engineering efficiency in the system life cycle. However, selecting the degree of formalization can be challenging, as it crucially depends on the desired common understanding (semantic degree) between multiple parties. In this paper, we categorize different semantic degrees and map a set of technologies in industrial automation to their associated degrees. Furthermore, we created guidelines to assist engineers selecting appropriate semantic degrees in their design. We applied these guidelines on publically available scenarios to examine the validity of the approach, and identified semantic elements over internally developed use cases targeting semantically-enabled plug-and-produce.
Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms
Venue: arXiv cs.RO 2015
Year: 2015

The emergent global behaviours of robotic swarms are important to achieve their navigation task goals. These emergent behaviours can be verified to assess their correctness, through techniques like model checking. Model checking exhaustively explores all possible behaviours, based on a discrete model of the system, such as a swarm in a grid. A common problem in model checking is the state-space explosion that arises when the states of the model are numerous. We propose a novel implementation of symmetry reduction, in the form of encoding navigation algorithms relatively with respect to a reference, based on the symmetrical properties of swarms in grids. We applied the relative encoding to a swarm navigation algorithm, Alpha, modelled for the NuSMV model checker. A comparison of the state-space and verification results with an absolute (or global) and a relative encoding of the Alpha algorithm highlights the advantages of our approach, allowing model checking larger grid sizes and number of robots, and consequently, verifying more complex emergent behaviours. For example, a property was verified for a grid with 3 robots and a maximum allowed size of 8x8 cells in a global encoding, whereas this size was increased to 16x16 using a relative encoding. Also, the time to verify a property for a swarm of 3 robots in a 6x6 grid was reduced from almost 10 hours to only 7 minutes. Our approach is transferable to other swarm navigation algorithms.
Verification of Control Systems Implemented in Simulink with Assertion Checks and Theorem Proving: A Case Study
Venue: arXiv cs.SY 2015
Year: 2015

This paper presents the verification of control systems implemented in Simulink. The goal is to ensure that high-level requirements on control performance, like stability, are satisfied by the Simulink diagram. A two stage process is proposed. First, the high-level requirements are decomposed into specific parametrized sub-requirements and implemented as assertions in Simulink. Second, the verification takes place. On one hand, the sub-requirements are verified through assertion checks in simulation. On the other hand, according to their scope, some of the sub-requirements are verified through assertion checks in simulation, and others via automatic theorem proving over an ideal mathematical model of the diagram. We compare performing only assertion checks against the use of theorem proving, to highlight the advantages of the latter. Theorem proving performs verification by computing a mathematical proof symbolically, covering the entire state space of the variables. An automatic translation tool from Simulink to the language of the theorem proving tool Why3 is also presented. The paper demonstrates our approach by verifying the stability of a simple discrete linear system.
On the Evaluation of GMSK Scheme with ECC Techniques in Wireless Sensor Network
Venue: arXiv cs.NI 2015
Year: 2015

Wireless sensor nodes are powered by batteries, for which replacement is very difficult. That is why, optimization of energy consumption is a major objective in the area of wireless sensor networks (WSNs).On the other hand, noisy channel has a prominent influence on the reliability of data transmission. Therefore, an energy efficient transmission strategy should be considered on the communication process of wireless nodes in order to obtain optimal energy network consumption. Indeed, the choice of suitable modulation format with the proper Error Correcting code (ECC) played a great responsibility to obtain better energy conservation.In this work, we aim to evaluate the performance analysis of Gaussian Minimum Shift Keying (GMSK) modulation with several combinations of coding strategies using various analysis metrics such as Bit Error Rate (BER), energy consumption.Through extensive simulation, we disclose that he gain achieved through GMSK modulation with suitable channel coding mechanism is promising to obtain reliable communication and energy conservation in WSN.
Watch and Learn: Semi-Supervised Learning of Object Detectors from Videos
Venue: arXiv cs.CV 2015
Year: 2015

We present a semi-supervised approach that localizes multiple unknown object instances in long videos. We start with a handful of labeled boxes and iteratively learn and label hundreds of thousands of object instances. We propose criteria for reliable object detection and tracking for constraining the semi-supervised learning process and minimizing semantic drift. Our approach does not assume exhaustive labeling of each object instance in any single frame, or any explicit annotation of negative data. Working in such a generic setting allow us to tackle multiple object instances in video, many of which are static. In contrast, existing approaches either do not consider multiple object instances per video, or rely heavily on the motion of the objects present. The experiments demonstrate the effectiveness of our approach by evaluating the automatically labeled data on a variety of metrics like quality, coverage (recall), diversity, and relevance to training an object detector.
Graph colouring algorithms
Venue: arXiv cs.DS 2015
Year: 2015

This chapter presents an introduction to graph colouring algorithms. The focus is on vertex-colouring algorithms that work for general classes of graphs with worst-case performance guarantees in a sequential model of computation. The presentation aims to demonstrate the breadth of available techniques and is organized by algorithmic paradigm.
Quantifying Conformance using the Skorokhod Metric (full version)
Venue: arXiv cs.SY 2015
Year: 2015

The conformance testing problem for dynamical systems asks, given two dynamical models (e.g., as Simulink diagrams), whether their behaviors are "close" to each other. In the semi-formal approach to conformance testing, the two systems are simulated on a large set of tests, and a metric, defined on pairs of real-valued, real-timed trajectories, is used to determine a lower bound on the distance. We show how the Skorkhod metric on continuous dynamical systems can be used as the foundation for conformance testing of complex dynamical models. The Skorokhod metric allows for both state value mismatches and timing distortions, and is thus well suited for checking conformance between idealized models of dynamical systems and their implementations. We demonstrate the robustness of the system conformance quantification by proving a \emph{transference theorem}: trajectories close under the Skorokhod metric satisfy "close" logical properties. Specifically, we show the result for the timed linear time logic \TLTL augmented with a rich class of temporal and spatial constraint predicates. We provide a window-based streaming algorithm to compute the Skorokhod metric, and use it as a basis for a conformance testing tool for Simulink. We experimentally demonstrate the effectiveness of our tool in finding discrepant behaviors on a set of control system benchmarks, including an industrial challenge problem.
Synthesis through Unification
Venue: arXiv cs.PL 2015
Year: 2015

Given a specification and a set of candidate programs (program space), the program synthesis problem is to find a candidate program that satisfies the specification. We present the synthesis through unification (STUN) approach, which is an extension of the counter-example guided inductive synthesis (CEGIS) approach. In CEGIS, the synthesizer maintains a subset S of inputs and a candidate program Prog that is correct for S. The synthesizer repeatedly checks if there exists a counter-example input c such that the execution of Prog is incorrect on c. If so, the synthesizer enlarges S to include c, and picks a program from the program space that is correct for the new set S. The STUN approach extends CEGIS with the idea that given a program Prog that is correct for a subset of inputs, the synthesizer can try to find a program Prog' that is correct for the rest of the inputs. If Prog and Prog' can be unified into a program in the program space, then a solution has been found. We present a generic synthesis procedure based on the STUN approach and specialize it for three different domains by providing the appropriate unification operators. We implemented these specializations in prototype tools, and we show that our tools often per- forms significantly better on standard benchmarks than a tool based on a pure CEGIS approach.
Identifying Modes of Intent from Driver Behaviors in Dynamic Environments
Venue: arXiv cs.SY 2015
Year: 2015

In light of growing attention of intelligent vehicle systems, we propose developing a driver model that uses a hybrid system formulation to capture the intent of the driver. This model hopes to capture human driving behavior in a way that can be utilized by semi- and fully autonomous systems in heterogeneous environments. We consider a discrete set of high level goals or intent modes, that is designed to encompass the decision making process of the human. A driver model is derived using a dataset of lane changes collected in a realistic driving simulator, in which the driver actively labels data to give us insight into her intent. By building the labeled dataset, we are able to utilize classification tools to build the driver model using features of based on her perception of the environment, and achieve high accuracy in identifying driver intent. Multiple algorithms are presented and compared on the dataset, and a comparison of the varying behaviors between drivers is drawn. Using this modeling methodology, we present a model that can be used to assess driver behaviors and to develop human-inspired safety metrics that can be utilized in intelligent vehicular systems.
Privacy-preserving Cross-domain Routing Optimization -- A Cryptographic Approach
Venue: arXiv cs.CR 2015
Year: 2015

Today's large-scale enterprise networks, data center networks, and wide area networks can be decomposed into multiple administrative or geographical domains. Domains may be owned by different administrative units or organizations. Hence protecting domain information is an important concern. Existing general-purpose Secure Multi-Party Computation (SMPC) methods that preserves privacy for domains are extremely slow for cross-domain routing problems. In this paper we present PYCRO, a cryptographic protocol specifically designed for privacy-preserving cross-domain routing optimization in Software Defined Networking (SDN) environments. PYCRO provides two fundamental routing functions, policy-compliant shortest path computing and bandwidth allocation, while ensuring strong protection for the private information of domains. We rigorously prove the privacy guarantee of our protocol. We have implemented a prototype system that runs PYCRO on servers in a campus network. Experimental results using real ISP network topologies show that PYCRO is very efficient in computation and communication costs.
Scientometrics and Science Studies: From Words and Co-Words to Information and Probabilistic Entropy
Venue: arXiv cs.DL 2015
Year: 2015

The tension between qualitative theorizing and quantitative methods is pervasive in the social sciences, and poses a constant challenge to empirical research. But in science studies as an interdisciplinary specialty, there are additional reasons why a more reflexive consciousness of the differences among the relevant disciplines is necessary. How can qualitative insights from the history of ideas and the sociology of science be combined with the quantitative perspective? By using the example of the lexical and semantic value of word occurrences, the issue of qualitatively different meanings of the same phenomena is discussed as a methodological problem. Nine criteria for methods which are needed for the development of science studies as an integrated enterprise can then be specified. Information calculus is suggested as a method which can comply with these criteria.
PIR with Low Storage Overhead: Coding instead of Replication
Venue: arXiv cs.IT 2015
Year: 2015

Private information retrieval (PIR) protocols allow a user to retrieve a data item from a database without revealing any information about the identity of the item being retrieved. Specifically, in information-theoretic $k$-server PIR, the database is replicated among $k$ non-communicating servers, and each server learns nothing about the item retrieved by the user. The cost of PIR protocols is usually measured in terms of their communication complexity, which is the total number of bits exchanged between the user and the servers, and storage overhead, which is the ratio between the total number of bits stored on all the servers and the number of bits in the database. Since single-server information-theoretic PIR is impossible, the storage overhead of all existing PIR protocols is at least $2$. In this work, we show that information-theoretic PIR can be achieved with storage overhead arbitrarily close to the optimal value of $1$, without sacrificing the communication complexity. Specifically, we prove that all known $k$-server PIR protocols can be efficiently emulated, while preserving both privacy and communication complexity but significantly reducing the storage overhead. To this end, we distribute the $n$ bits of the database among $s+r$ servers, each storing $n/s$ coded bits (rather than replicas). For every fixed $k$, the resulting storage overhead $(s+r)/s$ approaches $1$ as $s$ grows; explicitly we have $r\le k\sqrt{s}(1+o(1))$. Moreover, in the special case $k = 2$, the storage overhead is only $1 + \frac{1}{s}$. In order to achieve these results, we introduce and study a new kind of binary linear codes, called here $k$-server PIR codes. We then show how such codes can be constructed, and we establish several bounds on the parameters of $k$-server PIR codes. Finally, we briefly discuss extensions of our results to nonbinary alphabets, to robust PIR, and to $t$-private PIR.
Efficient Large Scale Video Classification
Venue: arXiv cs.CV 2015
Year: 2015

Video classification has advanced tremendously over the recent years. A large part of the improvements in video classification had to do with the work done by the image classification community and the use of deep convolutional networks (CNNs) which produce competitive results with hand- crafted motion features. These networks were adapted to use video frames in various ways and have yielded state of the art classification results. We present two methods that build on this work, and scale it up to work with millions of videos and hundreds of thousands of classes while maintaining a low computational cost. In the context of large scale video processing, training CNNs on video frames is extremely time consuming, due to the large number of frames involved. We propose to avoid this problem by training CNNs on either YouTube thumbnails or Flickr images, and then using these networks' outputs as features for other higher level classifiers. We discuss the challenges of achieving this and propose two models for frame-level and video-level classification. The first is a highly efficient mixture of experts while the latter is based on long short term memory neural networks. We present results on the Sports-1M video dataset (1 million videos, 487 classes) and on a new dataset which has 12 million videos and 150,000 labels.
A Frobenius Model of Information Structure in Categorical Compositional Distributional Semantics
Venue: arXiv cs.CL 2015
Year: 2015

The categorical compositional distributional model of Coecke, Sadrzadeh and Clark provides a linguistically motivated procedure for computing the meaning of a sentence as a function of the distributional meaning of the words therein. The theoretical framework allows for reasoning about compositional aspects of language and offers structural ways of studying the underlying relationships. While the model so far has been applied on the level of syntactic structures, a sentence can bring extra information conveyed in utterances via intonational means. In the current paper we extend the framework in order to accommodate this additional information, using Frobenius algebraic structures canonically induced over the basis of finite-dimensional vector spaces. We detail the theory, provide truth-theoretic and distributional semantics for meanings of intonationally-marked utterances, and present justifications and extensive examples.
Tracking Causal Dependencies in Web Services Orchestrations Defined in ORC
Venue: arXiv cs.PL 2015
Year: 2015

This article shows how the operational semantics of a language like ORC can be instrumented so that the execution of a program produces information on the causal dependencies between events. The concurrent semantics we obtain is based on asymmetric labeled event structures. The approach is illustrated using a Web service orchestration instance and the detection of race conditions.
Time Robustness in MTL and Expressivity in Hybrid System Falsification (Extended Version)
Venue: arXiv cs.SY 2015
Year: 2015

Building on the work by Fainekos and Pappas and the one by Donze and Maler, we introduce AvSTL, an extension of metric interval temporal logic by averaged temporal operators. Its expressivity in capturing both space and time robustness helps solving falsification problems, (i.e. searching for a critical path in hybrid system models); it does so by communicating a designer's intention more faithfully to the stochastic optimization engine employed in a falsification solver. We also introduce a sliding window-like algorithm that keeps the cost of computing truth/robustness values tractable.