OpenRaiser/Intern-Atlas huggingface dataset:
Group Strategyproof Pareto-Stable Marriage with Indifferences via the Generalized Assignment Game
Venue: arXiv cs.GT 2017
Year: 2017

We study the variant of the stable marriage problem in which the preferences of the agents are allowed to include indifferences. We present a mechanism for producing Pareto-stable matchings in stable marriage markets with indifferences that is group strategyproof for one side of the market. Our key technique involves modeling the stable marriage market as a generalized assignment game. We also show that our mechanism can be implemented efficiently. These results can be extended to the college admissions problem with indifferences.
On the steganographic image based approach to PDF files protection
Venue: arXiv cs.MM 2017
Year: 2017

Digital images can be copied without authorization and have to be protected. Two schemes for watermarking images in PDF document were considered. Both schemes include a converter to extract images from PDF pages and return the protected images back. Frequency and spatial domain embedding were used for hiding a message presented by a binary pattern. We considered visible and invisible watermarking and found that spatial domain LSB technique can be more preferable than frequency embedding using DWT.
Small-Signal Analysis of the Microgrid Secondary Control Considering a Communication Time Delay
Venue: arXiv cs.SY 2017
Year: 2017

This paper presents a small-signal analysis of an islanded microgrid composed of two or more voltage source inverters connected in parallel. The primary control of each inverter is integrated through internal current and voltage loops using PR compensators, a virtual impedance, and an external power controller based on frequency and voltage droops. The frequency restoration function is implemented at the secondary control level, which executes a consensus algorithm that consists of a load-frequency control and a single time delay communication network. The consensus network consists of a time-invariant directed graph and the output power of each inverter is the information shared among the units, which is affected by the time delay. The proposed small-signal model is validated through simulation results and experimental results. A root locus analysis is presented that shows the behavior of the system considering control parameters and time delay variation.
Productive Corecursion in Logic Programming
Venue: arXiv cs.LO 2017
Year: 2017

Logic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/coinductive soundness of formulae is a challenging task. For example, the existing state-of-the-art algorithms can only semi-decide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental and important undecidable property is productivity. If a derivation is infinite and coinductively sound, we may ask whether the computed answer it determines actually computes an infinite formula. If it does, the infinite computation is productive. This intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing. Recently, an algorithm was presented that semi-decides a weaker property -- of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this paper we strengthen these recent results. We propose a method that semi-decides productivity of individual derivations for regular formulae. Thus we at last give an algorithmic counterpart to the notion of productivity of derivations in logic programming. This is the first algorithmic solution to the problem since it was raised more than 30 years ago. We also present an implementation of this algorithm.
Automatic Generation of Natural Language Explanations
Venue: arXiv cs.CL 2017
Year: 2017

An important task for recommender system is to generate explanations according to a user's preferences. Most of the current methods for explainable recommendations use structured sentences to provide descriptions along with the recommendations they produce. However, those methods have neglected the review-oriented way of writing a text, even though it is known that these reviews have a strong influence over user's decision. In this paper, we propose a method for the automatic generation of natural language explanations, for predicting how a user would write about an item, based on user ratings from different items' features. We design a character-level recurrent neural network (RNN) model, which generates an item's review explanations using long-short term memories (LSTM). The model generates text reviews given a combination of the review and ratings score that express opinions about different factors or aspects of an item. Our network is trained on a sub-sample from the large real-world dataset BeerAdvocate. Our empirical evaluation using natural language processing metrics shows the generated text's quality is close to a real user written review, identifying negation, misspellings, and domain specific vocabulary.
Fairness at Equilibrium in the Labor Market
Venue: arXiv cs.GT 2017
Year: 2017

Recent literature on computational notions of fairness has been broadly divided into two distinct camps, supporting interventions that address either individual-based or group-based fairness. Rather than privilege a single definition, we seek to resolve both within the particular domain of employment discrimination. To this end, we construct a dual labor market model composed of a Temporary Labor Market, in which firm strategies are constrained to ensure group-level fairness, and a Permanent Labor Market, in which individual worker fairness is guaranteed. We show that such restrictions on hiring practices induces an equilibrium that Pareto-dominates those arising from strategies that employ statistical discrimination or a "group-blind" criterion. Individual worker reputations produce externalities for collective reputation, generating a feedback loop termed a "self-fulfilling prophecy." Our model produces its own feedback loop, raising the collective reputation of an initially disadvantaged group via a fairness intervention that need not be permanent. Moreover, we show that, contrary to popular assumption, the asymmetric equilibria resulting from hiring practices that disregard group-fairness may be immovable without targeted intervention. The enduring nature of such equilibria that are both inequitable and Pareto inefficient suggest that fairness interventions are of critical importance in moving the labor market to be more socially just and efficient.
Automated Lane Detection in Crowds using Proximity Graphs
Venue: arXiv cs.CV 2017
Year: 2017

Studying the behavior of crowds is vital for understanding and predicting human interactions in public areas. Research has shown that, under certain conditions, large groups of people can form collective behavior patterns: local interactions between individuals results in global movements patterns. To detect these patterns in a crowd, we assume each person is carrying an on-body device that acts a local proximity sensor, e.g., smartphone or bluetooth badge, and represent the texture of the crowd as a proximity graph. Our goal is extract information about crowds from these proximity graphs. In this work, we focus on one particular type of pattern: lane formation. We present a formal definition of a lane, proposed a simple probabilistic model that simulates lanes moving through a stationary crowd, and present an automated lane-detection method. Our preliminary results show that our method is able to detect lanes of different shapes and sizes. We see our work as an initial step towards rich pattern recognition using proximity graphs.
How to Generate Pseudorandom Permutations Over Other Groups: Even-Mansour and Feistel Revisited
Venue: arXiv cs.CR 2017
Year: 2017

Recent results by Alagic and Russell have given some evidence that the Even-Mansour cipher may be secure against quantum adversaries with quantum queries, if considered over other groups than $(\mathbb{Z}/2)^n$. This prompts the question as to whether or not other classical schemes may be generalized to arbitrary groups and whether classical results still apply to those generalized schemes. In this paper, we generalize the Even-Mansour cipher and the Feistel cipher. We show that Even and Mansour's original notions of secrecy are obtained on a one-key, group variant of the Even-Mansour cipher. We generalize the result by Kilian and Rogaway, that the Even-Mansour cipher is pseudorandom, to super pseudorandomness, also in the one-key, group case. Using a Slide Attack we match the bound found above. After generalizing the Feistel cipher to arbitrary groups we resolve an open problem of Patel, Ramzan, and Sundaram by showing that the $3$-round Feistel cipher over an arbitrary group is not super pseudorandom. Finally, we generalize a result by Gentry and Ramzan showing that the Even-Mansour cipher can be implemented using the Feistel cipher as the public permutation. In this last result, we also consider the one-key case over a group and generalize their bound.
Edge-ICN and its application to the Internet of Things
Venue: arXiv cs.NI 2017
Year: 2017

While research on Information-Centric Networking (ICN) flourishes, its adoption seems to be an elusive goal. In this paper we propose Edge-ICN: a novel approach for deploying ICN in a single large network, such as the network of an Internet Service Provider. Although Edge-ICN requires nothing beyond an SDN-based network supporting the OpenFlow protocol, with ICN-aware nodes only at the edges of the network, it still offers the same benefits as a clean-slate ICN architecture but without the deployment hassles. Moreover, by proxying legacy traffic and transparently forwarding it through the Edge-ICN nodes, all existing applications can operate smoothly, while offering significant advantages to applications such as native support for scalable anycast, multicast, and multi-source forwarding. In this context, we show how the proposed functionality at the edge of the network can specifically benefit CoAP-based IoT applications. Our measurements show that Edge-ICN induces on average the same control plane overhead for name resolution as a centralized approach, while also enabling IoT applications to build on anycast, multicast, and multi-source forwarding primitives.
Verifying Strong Eventual Consistency in Distributed Systems
Venue: arXiv cs.DC 2017
Year: 2017

Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.
MPG - A Framework for Reasoning on 6 DOF Pose Uncertainty
Venue: arXiv cs.RO 2017
Year: 2017

Reasoning about the pose, i.e. position and orientation of objects is one of the cornerstones of robotic manipulation under uncertainty. In a number of joint research projects our group is developing a robotic perception system that perceives and models an unprepared kitchen scenario with many objects. Since no single sensor or measurement provides sufficient information, a technique is needed to fuse a number of uncertain estimates of the pose, i.e. estimates with a widely stretched probability density function ($pdf$). The most frequently used approaches to describe the $pdfs$ are sample based description and multivariate normal (Gaussian) distributions. Sample based descriptions in 6D can describe basically any type of $pdfs$, but they require a large number of samples and there are no analytic formulae to fuse several $pdfs$. For Gaussian distributions these formulae exist, but the Gaussian distributions are unimodal and don't model widely spread distributions well. In this paper we present a framework for probabilistic modeling of 6D poses that combines the expressive power of the sample based description with the conciseness and algorithmic power of the Gaussian models. As parameterization of the 6D poses we select the dual quaternions, i.e. any pose is represented by two quaternions. The orientation part of a pose is described by a unit quaternion. The translation part is described by a purely imaginary quaternion. A basic probability density function over the poses is constructed by selecting a tangent point on the 3D sphere representing unit quaternions and taking the Cartesian set product of the tangent space with the 3D space of translations. In this 6D Euclidean space a 6D Gaussian distribution is defined. Projecting this Gaussian back to the unit sphere and renormalizing induces a distribution over 6D poses, called a Projected Gaussian.
A Generalised Seizure Prediction with Convolutional Neural Networks for Intracranial and Scalp Electroencephalogram Data Analysis
Venue: arXiv cs.CV 2017
Year: 2017

Seizure prediction has attracted a growing attention as one of the most challenging predictive data analysis efforts in order to improve the life of patients living with drug-resistant epilepsy and tonic seizures. Many outstanding works have been reporting great results in providing a sensible indirect (warning systems) or direct (interactive neural-stimulation) control over refractory seizures, some of which achieved high performance. However, many works put heavily handcraft feature extraction and/or carefully tailored feature engineering to each patient to achieve very high sensitivity and low false prediction rate for a particular dataset. This limits the benefit of their approaches if a different dataset is used. In this paper we apply Convolutional Neural Networks (CNNs) on different intracranial and scalp electroencephalogram (EEG) datasets and proposed a generalized retrospective and patient-specific seizure prediction method. We use Short-Time Fourier Transform (STFT) on 30-second EEG windows with 50% overlapping to extract information in both frequency and time domains. A standardization step is then applied on STFT components across the whole frequency range to prevent high frequencies features being influenced by those at lower frequencies. A convolutional neural network model is used for both feature extraction and classification to separate preictal segments from interictal ones. The proposed approach achieves sensitivity of 81.4%, 81.2%, 82.3% and false prediction rate (FPR) of 0.06/h, 0.16/h, 0.22/h on Freiburg Hospital intracranial EEG (iEEG) dataset, Children's Hospital of Boston-MIT scalp EEG (sEEG) dataset, and Kaggle American Epilepsy Society Seizure Prediction Challenge's dataset, respectively. Our prediction method is also statistically better than an unspecific random predictor for most of patients in all three datasets.
On the Compactness, Efficiency, and Representation of 3D Convolutional Networks: Brain Parcellation as a Pretext Task
Venue: arXiv cs.CV 2017
Year: 2017

Deep convolutional neural networks are powerful tools for learning visual representations from images. However, designing efficient deep architectures to analyse volumetric medical images remains challenging. This work investigates efficient and flexible elements of modern convolutional networks such as dilated convolution and residual connection. With these essential building blocks, we propose a high-resolution, compact convolutional network for volumetric image segmentation. To illustrate its efficiency of learning 3D representation from large-scale image data, the proposed network is validated with the challenging task of parcellating 155 neuroanatomical structures from brain MR images. Our experiments show that the proposed network architecture compares favourably with state-of-the-art volumetric segmentation networks while being an order of magnitude more compact. We consider the brain parcellation task as a pretext task for volumetric image segmentation; our trained network potentially provides a good starting point for transfer learning. Additionally, we show the feasibility of voxel-level uncertainty estimation using a sampling approximation through dropout.
Shared-memory Graph Truss Decomposition
Venue: arXiv cs.DC 2017
Year: 2017

We present PKT, a new shared-memory parallel algorithm and OpenMP implementation for the truss decomposition of large sparse graphs. A k-truss is a dense subgraph definition that can be considered a relaxation of a clique. Truss decomposition refers to a partitioning of all the edges in the graph based on their k-truss membership. The truss decomposition of a graph has many applications. We show that our new approach PKT consistently outperforms other truss decomposition approaches for a collection of large sparse graphs and on a 24-core shared-memory server. PKT is based on a recently proposed algorithm for k-core decomposition.
InferSpark: Statistical Inference at Scale
Venue: arXiv cs.DB 2017
Year: 2017

The Apache Spark stack has enabled fast large-scale data processing. Despite a rich library of statistical models and inference algorithms, it does not give domain users the ability to develop their own models. The emergence of probabilistic programming languages has showed the promise of developing sophisticated probabilistic models in a succinct and programmatic way. These frameworks have the potential of automatically generating inference algorithms for the user defined models and answering various statistical queries about the model. It is a perfect time to unite these two great directions to produce a programmable big data analysis framework. We thus propose, InferSpark, a probabilistic programming framework on top of Apache Spark. Efficient statistical inference can be easily implemented on this framework and inference process can leverage the distributed main memory processing power of Spark. This framework makes statistical inference on big data possible and speed up the penetration of probabilistic programming into the data engineering domain.
Controlling a Population
Venue: arXiv cs.FL 2017
Year: 2017

We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such populations: no matter how individual agents react to the actions of the controller , the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a non-deterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2-player game. The first player (Controller) chooses actions, and the second player (Agents) resolves non-determinism for each agent. The game with m agents is called the m-population game. This gives rise to a parameterized control problem (where control refers to 2 player games), namely the population control problem: can Controller control the m-population game for all $m $\in$ N$ whatever Agents does? In this paper, we prove that the population control problem is decidable, and it is a EXPTIME-complete problem. As far as we know, this is one of the first results on parameterized control. Our algorithm, not based on cutoff techniques, produces winning strategies which are symbolic, that is, they do not need to count precisely how the population is spread between states. We also show that if there is no winning strategy, then there is a population size M such that Controller wins the m-population game if and only if $m $\le$ M$. Surprisingly, M can be doubly exponential in the number of states of the NFA, with tight upper and lower bounds.
A spatiotemporal model with visual attention for video classification
Venue: arXiv cs.CV 2017
Year: 2017

High level understanding of sequential visual input is important for safe and stable autonomy, especially in localization and object detection. While traditional object classification and tracking approaches are specifically designed to handle variations in rotation and scale, current state-of-the-art approaches based on deep learning achieve better performance. This paper focuses on developing a spatiotemporal model to handle videos containing moving objects with rotation and scale changes. Built on models that combine Convolutional Neural Networks (CNNs) and Recurrent Neural Networks (RNNs) to classify sequential data, this work investigates the effectiveness of incorporating attention modules in the CNN stage for video classification. The superiority of the proposed spatiotemporal model is demonstrated on the Moving MNIST dataset augmented with rotation and scaling.
AE regularity of interval matrices
Venue: arXiv cs.NA 2017
Year: 2017

Consider a linear system of equations with interval coefficients, and each interval coefficient is associated with either a universal or an existential quantifier. The AE solution set and AE solvability of the system is defined by $\forall\exists$-quantification. Herein, we deal with the problem what properties must the coefficient matrix have in order that there is guaranteed an existence of an AE solution. Based on this motivation, we introduce a concept of AE regularity, which implies that the AE solution set is nonempty and the system is AE solvable for every right-hand side. We discuss characterization of AE regularity, and we also focus on various classes of matrices that are implicitly AE regular. Some of these classes are polynomially decidable, and therefore give an efficient way for checking AE regularity. We also state open problems related to computational complexity and characterization.