OpenRaiser/Intern-Atlas huggingface dataset:
Compositional Abstraction-Based Controller Synthesis for Continuous-Time Systems
Venue: arXiv cs.SY 2017
Year: 2017

Controller synthesis techniques for continuous systems with respect to temporal logic specifications typically use a finite-state symbolic abstraction of the system model. Constructing this abstraction for the entire system is computationally expensive, and does not exploit natural decompositions of many systems into interacting components. We describe a methodology for compositional symbolic abstraction to help scale controller synthesis for temporal logic to larger systems. We introduce a new relation, called (approximate) disturbance bisimulation, as the basis for compositional symbolic abstractions. Disturbance bisimulation strengthens the standard approximate alternating bisimulation relation used in control. It extends naturally to systems which are composed of weakly interconnected sub-components possibly connected in feedback, and models the coupling signals as disturbances. After proving this composability of disturbance bisimulation for metric systems we apply this result to the compositional abstraction of networks of input-to-state stable deterministic non-linear control systems. We give conditions that allow to construct finite-state abstractions compositionally for each component in such a network, so that the abstractions are simultaneously disturbance bisimilar to their continuous counterparts. Combining these two results, we show conditions under which one can compositionally abstract a network of non-linear control systems in a modular way while ensuring that the final composed abstraction is disturbance bisimilar to the original system. We discuss how we get a compositional abstraction-based controller synthesis methodology for networks of such systems against local temporal specifications as a by-product of our construction.
MARTA GANs: Unsupervised Representation Learning for Remote Sensing Image Classification
Venue: arXiv cs.CV 2017
Year: 2017

With the development of deep learning, supervised learning has frequently been adopted to classify remotely sensed images using convolutional networks (CNNs). However, due to the limited amount of labeled data available, supervised learning is often difficult to carry out. Therefore, we proposed an unsupervised model called multiple-layer feature-matching generative adversarial networks (MARTA GANs) to learn a representation using only unlabeled data. MARTA GANs consists of both a generative model $G$ and a discriminative model $D$. We treat $D$ as a feature extractor. To fit the complex properties of remote sensing data, we use a fusion layer to merge the mid-level and global features. $G$ can produce numerous images that are similar to the training data; therefore, $D$ can learn better representations of remotely sensed images using the training data provided by $G$. The classification results on two widely used remote sensing image databases show that the proposed method significantly improves the classification performance compared with other state-of-the-art methods.
Improving Blind Steganalysis in Spatial Domain using a Criterion to Choose the Appropriate Steganalyzer between CNN and SRM+EC
Venue: arXiv cs.MM 2017
Year: 2017

Conventional state-of-the-art image steganalysis approaches usually consist of a classifier trained with features provided by rich image models. As both features extraction and classification steps are perfectly embodied in the deep learning architecture called Convolutional Neural Network (CNN), different studies have tried to design a CNN-based steganalyzer. The network designed by Xu et al. is the first competitive CNN with the combination Spatial Rich Models (SRM) and Ensemble Classifier (EC) providing detection performances of the same order. In this work we propose a criterion to choose either the CNN or the SRM+EC method for a given input image. Our approach is studied with three different steganographic spatial domain algorithms: S-UNIWARD, MiPOD, and HILL, using the Tensorflow computing platform, and exhibits detection capabilities better than each method alone. Furthermore, as SRM+EC and the CNN are both only trained with a single embedding algorithm, namely MiPOD, the proposed method can be seen as an approach for blind steganalysis. In blind detection, error rates are respectively of 16% for S-UNIWARD, 16% for MiPOD, and 17% for HILL on the BOSSBase with a payload of 0.4 bpp. For 0.1 bpp, the respective corresponding error rates are of 39%, 38%, and 41%, and are always better than the ones provided by SRM+EC.
Fundamental Limits of Caching: Improved Bounds with Coded Prefetching
Venue: arXiv cs.IT 2017
Year: 2017

We consider a cache network in which a single server is connected to multiple users via a shared error free link. The server has access to a database with $N$ files of equal length $F$, and serves $K$ users each with a cache memory of $MF$ bits. A novel centralized coded caching scheme is proposed for scenarios with more users than files $N\leq K$ and cache capacities satisfying $\frac{1}{K}\leq M\leq\frac{N}{K}$. The proposed scheme outperforms the best rate-memory region known in the literature if $N\leq K\leq\frac{N^{2}+1}{2}$.
Graph Information Ratio
Venue: arXiv cs.IT 2017
Year: 2017

We introduce the notion of information ratio $\text{Ir}(H/G)$ between two (simple, undirected) graphs $G$ and $H$, defined as the supremum of ratios $k/n$ such that there exists a mapping between the strong products $G^k$ to $H^n$ that preserves non-adjacency. Operationally speaking, the information ratio is the maximal number of source symbols per channel use that can be reliably sent over a channel with a confusion graph $H$, where reliability is measured w.r.t. a source confusion graph $G$. Various results are provided, including in particular lower and upper bounds on $\text{Ir}(H/G)$ in terms of different graph properties, inequalities and identities for behavior under strong product and disjoint union, relations to graph cores, and notions of graph criticality. Informally speaking, $\text{Ir}(H/G)$ can be interpreted as a measure of similarity between $G$ and $H$. We make this notion precise by introducing the concept of information equivalence between graphs, a more quantitative version of homomorphic equivalence. We then describe a natural partial ordering over the space of information equivalence classes, and endow it with a suitable metric structure that is contractive under the strong product. Various examples and open problems are discussed.
Self-Interference in Full-Duplex Multi-User MIMO Channels
Venue: arXiv cs.IT 2017
Year: 2017

We consider a multi-user multiple-input multiple-output (MIMO) setup where full-duplex (FD) multi-antenna nodes apply linear beamformers to simultaneously transmit and receive multiple streams over Rician fading channels. The exact first and second positive moments of the residual self-interference (SI), involving the squared norm of a sum of non-identically distributed random variables, are derived in closed-form. The method of moments is hence invoked to provide a Gamma approximation for the residual SI distribution. The proposed theorem holds under arbitrary linear precoder/decoder design, number of antennas and streams, and SI cancellation capability.
Using Coalgebras and the Giry Monad for Interpreting Game Logics --- A Tutorial
Venue: arXiv cs.LO 2017
Year: 2017

The stochastic interpretation of Parikh's game logic should not follow the usual pattern of Kripke models, which in turn are based on the Kleisli morphisms for the Giry monad, rather, a specific and more general approach to probabilistic nondeterminism is required. We outline this approach together with its probabilistic and measure theoretic basis, introducing in a leisurely pace the Giry monad and their Kleisli morphisms together with important techniques for manipulating them. Proof establishing specific techniques are given, and pointers to the extant literature are provided. After working through this tutorial, the reader should find it easier to follow the original literature in this and related areas, and it should be possible for her or him to appreciate measure theoretic arguments for original work in the areas of Markov transition systems, and stochastic effectivity functions.
Topological Analysis and Synthesis of Structures related to Certain Classes of K-Geodetic Computer Networks
Venue: arXiv cs.DM 2017
Year: 2017

A fundamental characteristic of computer networks is their topological structure. The question of the description of the structural characteristics of computer networks represents a problem that is not completely solved. Search methods for structures of computer networks, for which the values of the selected parameters of their operation quality are extreme, have not been completely developed. The construction of computer networks with optimum indices of their operation quality is reduced to the solution of discrete optimization problems over graphs. This paper describes in detail the advantages of the practical use of k-geodetic graphs [2, 3] in the topological design of computer networks as an alternative for the solution of the fundamental problems mentioned above which, we believe, are still open. Also, the topological analysis and synthesis of some classes of these networks have been performed.
High Performance CNFET-based Ternary Full Adders
Venue: arXiv cs.ET 2017
Year: 2017

This paper investigates the use of carbon nanotube field effect transistors (CNFETs) for the design of ternary full adder cells. The proposed circuits have been designed based on the unique properties of CNFETs such as having desired threshold voltages by adjusting diameter of the CNFETs gate nanotubes. The proposed circuits are examined using HSPICE simulator with the standard 32 nm CNFET technology. The proposed methods are simulated at different conditions such as different supply voltages, different temperature and operational frequencies. Simulation results show that the proposed designs are faster than the state of the art CNFET based ternary full adders.
Challenges ahead Electron Microscopy for Structural Biology from the Image Processing point of view
Venue: arXiv cs.CV 2017
Year: 2017

Since the introduction of Direct Electron Detectors (DEDs), the resolution and range of macromolecules amenable to this technique has significantly widened, generating a broad interest that explains the well over a dozen reviews in top journal in the last two years. Similarly, the number of job offers to lead EM groups and/or coordinate EM facilities has exploded, and FEI (the main microscope manufacturer for Life Sciences) has received more than 100 orders of high-end electron microscopes by summer 2016. Strategic corporate movements are also happening, with very big players entering the market through key acquisitions (Thermo Fisher has recently bought FEI for \$4.2B), partly attracted by new Pharma interest in the field, now perceived to be in a position to impact structure-based drug design. The scientific perspectives are indeed extremely positive but, in these moments of well-founded generalized optimists, we want to make a reflection on some of the hurdles ahead us, since they certainly exist and they indeed limit the informational content of cryoEM projects. Here we focus on image processing aspects, particularly in the so-called area of Single Particle Analysis, discussing some of the current resolution and high-throughput limiting factors.
Analysis of a Stochastic Model of Replication in Large Distributed Storage Systems: A Mean-Field Approach
Venue: arXiv cs.DC 2017
Year: 2017

Distributed storage systems such as Hadoop File System or Google File System (GFS) ensure data availability and durability using replication. This paper is focused on the analysis of the efficiency of replication mechanism that determines the location of the copies of a given file at some server. The variability of the loads of the nodes of the network is investigated for several policies. Three replication mechanisms are tested against simulations in the context of a real implementation of a such a system: Random, Least Loaded and Power of Choice. The simulations show that some of these policies may lead to quite unbalanced situations: if $β$ is the average number of copies per node it turns out that, at equilibrium, the load of the nodes may exhibit a high variability. It is shown in this paper that a simple variant of a power of choice type algorithm has a striking effect on the loads of the nodes: at equilibrium, the distribution of the load of a node has a bounded support, most of nodes have a load less than $2β$ which is an interesting property for the design of the storage space of these systems. Mathematical models are introduced and investigated to explain this interesting phenomenon. The analysis of these systems turns out to be quite complicated mainly because of the large dimensionality of the state spaces involved. Our study relies on probabilistic methods, mean-field analysis, to analyze the asymptotic behavior of an arbitrary node of the network when the total number of nodes gets large. An additional ingredient is the use of stochastic calculus with marked Poisson point processes to establish some of our results.
A Resource Management Protocol for Mobile Cloud Using Auto-Scaling
Venue: arXiv cs.DC 2017
Year: 2017

Cloud radio access networks (C-RAN) and Mobile Cloud Computing (MCC) have emerged as promising candidates for the next generation access network techniques. MCC enables resource limited mobile devices to offload computationally intensive tasks to the cloud, while C-RAN offers a technology that addresses the increasing mobile traffic. In this paper, we propose a protocol for task offloading and for managing resources in both C-RAN and mobile cloud together using a centralised controller. Experiments on resource management using cloud auto-scaling shows that resource (CPU, RAM, Storage) scaling times vary.
Collecting a Swarm in a Grid Environment Using Shared, Global Inputs
Venue: arXiv cs.RO 2017
Year: 2017

This paper investigates efficient techniques to collect and concentrate an under-actuated particle swarm despite obstacles. Concentrating a swarm of particles is of critical importance in health-care for targeted drug delivery, where micro-scale particles must be steered to a goal location. Individual particles must be small in order to navigate through micro-vasculature, but decreasing size brings new challenges. Individual particles are too small to contain on-board power or computation and are instead controlled by a global input, such as an applied fluidic flow or electric field. To make progress, this paper considers a swarm of robots initialized in a grid world in which each position is either free-space or obstacle. This paper provides algorithms that collect all the robots to one position and compares these algorithms on the basis of efficiency and implementation time.
Duplicate matching and estimating features for detection of copy-move images forgery
Venue: arXiv cs.MM 2017
Year: 2017

Copy-move forgery is the most popular and simplest image manipulation method. In this type of forgery, an area from the image copied, then after post processing such as rotation and scaling, placed on the destination. The goal of Copy-move forgery is to hide or duplicate one or more objects in the image. Key-point based Copy-move forgery detection methods have five main steps: preprocessing, feature extraction, matching, transform estimation and post processing that matching and transform estimation have important effect on the detection. More over the error could happens in some steps due to the noise. The existing methods process these steps separately and in case of having an error in a step, this error could be propagated to the following steps and affects the detection. To solve the above mentioned problem, in this paper the steps of the detection system interact with each other and if an error happens in a step, following steps are trying to detect and solve it. We formulate this interaction by defining and optimizing a cost function. This function includes matching and transform estimation steps. Then in an iterative procedure the steps are executed and in case of detecting error, the error will be corrected. The efficiency of the proposed method analyzed in diverse cases such as pixel image precision level on the simple forgery images, robustness to the rotation and scaling, detecting professional forgery images and the precision of the transformation matrix. The results indicate the better efficiency of the proposed method.
Two-Bit Networks for Deep Learning on Resource-Constrained Embedded Devices
Venue: arXiv cs.LG 2017
Year: 2017

With the rapid proliferation of Internet of Things and intelligent edge devices, there is an increasing need for implementing machine learning algorithms, including deep learning, on resource-constrained mobile embedded devices with limited memory and computation power. Typical large Convolutional Neural Networks (CNNs) need large amounts of memory and computational power, and cannot be deployed on embedded devices efficiently. We present Two-Bit Networks (TBNs) for model compression of CNNs with edge weights constrained to (-2, -1, 1, 2), which can be encoded with two bits. Our approach can reduce the memory usage and improve computational efficiency significantly while achieving good performance in terms of classification accuracy, thus representing a reasonable tradeoff between model size and performance.
The leveled approach. Using and evaluating text mining tools AVResearcherXL and Texcavator for historical research on public perceptions of drugs
Venue: arXiv cs.HC 2017
Year: 2017

We introduce our explorative historical leveled approach that we use to understand drug debates in the Royal Dutch Library's digital newspaper archive. In this approach we alternate between distant reading and close reading. Furthermore, we use this approach to evaluate two text mining tools: AVResearcherXL and Texcavator.
Packing Unequal Circles into a Square Container by Partitioning Narrow Action Spaces and Circle Items
Venue: arXiv cs.CG 2017
Year: 2017

We address the NP-hard problem of finding a non-overlapping dense packing pattern for n Unequal Circle items in a two-dimensional Square Container (PUC-SC) such that the size of the container is minimized. Based on our previous work on an Action Space based Global Optimization (ASGO) that approximates each circle item as a square item to efficiently find the large unoccupied spaces, we propose an optimization algorithm based on the Partitioned Action Space and Partitioned Circle Items (PAS-PCI). The PAS is to partition the narrow action space on the long side to find two equal action spaces to fully utilize the unoccupied spaces. The PCI is to partition the circle items into four groups based on size for the basin hopping strategy. Experiments on two sets of benchmark instances show the effectiveness of the proposed method. In comparison with our previous algorithm ASGO on the 68 tested instances that ASGO published, PAS-PCI not only gains smaller containers in 64 instances and matches the other 4 but also runs faster in most instances. In comparison with the best record of the Packomania website on a total of 98 instances, PAS-PCI finds smaller containers on 82 and matches the other 16. Note that we updated 19 records for (47-48, 51-54, 57, 61-72) that had been kept unchanged since 2013.
Leveraging Multi-aspect Time-related Influence in Location Recommendation
Venue: arXiv cs.CY 2017
Year: 2017

Point-Of-Interest (POI) recommendation aims to mine a user's visiting history and find her/his potentially preferred places. Although location recommendation methods have been studied and improved pervasively, the challenges w.r.t employing various influences including temporal aspect still remain. Inspired by the fact that time includes numerous granular slots (e.g. minute, hour, day, week and etc.), in this paper, we define a new problem to perform recommendation through exploiting all diversified temporal factors. In particular, we argue that most existing methods only focus on a limited number of time-related features and neglect others. Furthermore, considering a specific granularity (e.g. time of a day) in recommendation cannot always apply to each user or each dataset. To address the challenges, we propose a probabilistic generative model, named after Multi-aspect Time-related Influence (MATI) to promote POI recommendation. We also develop a novel optimization algorithm based on Expectation Maximization (EM). Our MATI model firstly detects a user's temporal multivariate orientation using her check-in log in Location-based Social Networks(LBSNs). It then performs recommendation using temporal correlations between the user and proposed locations. Our method is adaptable to various types of recommendation systems and can work efficiently in multiple time-scales. Extensive experimental results on two large-scale LBSN datasets verify the effectiveness of our method over other competitors.
Source Code Verification for Embedded Systems using Prolog
Venue: arXiv cs.SE 2017
Year: 2017

System relevant embedded software needs to be reliable and, therefore, well tested, especially for aerospace systems. A common technique to verify programs is the analysis of their abstract syntax tree (AST). Tree structures can be elegantly analyzed with the logic programming language Prolog. Moreover, Prolog offers further advantages for a thorough analysis: On the one hand, it natively provides versatile options to efficiently process tree or graph data structures. On the other hand, Prolog's non-determinism and backtracking eases tests of different variations of the program flow without big effort. A rule-based approach with Prolog allows to characterize the verification goals in a concise and declarative way. In this paper, we describe our approach to verify the source code of a flash file system with the help of Prolog. The flash file system is written in C++ and has been developed particularly for the use in satellites. We transform a given abstract syntax tree of C++ source code into Prolog facts and derive the call graph and the execution sequence (tree), which then are further tested against verification goals. The different program flow branching due to control structures is derived by backtracking as subtrees of the full execution sequence. Finally, these subtrees are verified in Prolog. We illustrate our approach with a case study, where we search for incorrect applications of semaphores in embedded software using the real-time operating system RODOS. We rely on computation tree logic (CTL) and have designed an embedded domain specific language (DSL) in Prolog to express the verification goals.
A Practical Study of Control in Objected-Oriented--Functional--Logic Programming with Paisley
Venue: arXiv cs.PL 2017
Year: 2017

Paisley is an extensible lightweight embedded domain-specific language for nondeterministic pattern matching in Java. Using simple APIs and programming idioms, it brings the power of functional-logic processing of arbitrary data objects to the Java platform, without constraining the underlying object-oriented semantics. Here we present an extension to the Paisley framework that adds pattern-based control flow. It exploits recent additions to the Java language, namely functional interfaces and lambda expressions, for an explicit and transparent continuation-passing style approach to control. We evaluate the practical impact of the novel features on a real-world case study that reengineers a third-party open-source project to use Paisley in place of conventional object-oriented data query idioms. We find the approach viable for incremental refactoring of legacy code, with significant qualitative improvements regarding separation of concerns, clarity and intentionality, thus making for easier code understanding, testing and debugging.