OpenRaiser/Intern-Atlas huggingface dataset:
Session Types for Link Failures (Technical Report)
Venue: arXiv cs.LO 2017
Year: 2017

We strive to use session type technology to prove behavioural properties of fault-tolerant distributed algorithms. Session types are designed to abstractly capture the structure of (even multi-party) communication protocols. The goal of session types is the analysis and verification of the protocols' behavioural properties. One important such property is progress, i.e., the absence of (unintended) deadlock. Distributed algorithms often resemble (compositions of) multi-party communication protocols. In contrast to protocols that are typically studied with session types, they are often designed to cope with system failures. An essential behavioural property is (successful) termination, despite failures, but it is often elaborate to prove for distributed algorithms. We extend multi-party session types (and multi-party session types with nested sessions) by optional blocks that cover a limited class of link and crash failures. This allows us to automatically derive termination of distributed algorithms that come within these limits. To illustrate our approach, we prove termination for an implementation of the *rotating coordinator* Consensus algorithm.
A Selectable Sloppy Heap
Venue: arXiv cs.DS 2017
Year: 2017

We study the selection problem, namely that of computing the $i$th order statistic of $n$ given elements. Here we offer a data structure called \emph{selectable sloppy heap} handling a dynamic version in which upon request: (i)~a new element is inserted or (ii)~an element of a prescribed quantile group is deleted from the data structure. Each operation is executed in (ideal!) constant time---and is thus independent of $n$ (the number of elements stored in the data structure)---provided that the number of quantile groups is fixed. This is the first result of this kind accommodating both insertion and deletion in constant time. As such, our data structure outperforms the soft heap data structure of Chazelle (which only offers constant amortized complexity for a fixed error rate $0<\varepsilon \leq 1/2$) in applications such as dynamic percentile maintenance. The design demonstrates how slowing down a certain computation can speed up the data structure.
Understanding the limits of LoRaWAN
Venue: arXiv cs.NI 2017
Year: 2017

The quick proliferation of LPWAN networks, being LoRaWAN one of the most adopted, raised the interest of the industry, network operators and facilitated the development of novel services based on large scale and simple network structures. LoRaWAN brings the desired ubiquitous connectivity to enable most of the outdoor IoT applications and its growth and quick adoption are real proofs of that. Yet the technology has some limitations that need to be understood in order to avoid over-use of the technology. In this article we aim to provide an impartial overview of what are the limitations of such technology, and in a comprehensive manner bring use case examples to show where the limits are.
An Energy stable Monolithic Eulerian Fluid-Structure Numerical Scheme *
Venue: arXiv cs.CE 2017
Year: 2017

The conservation laws of continuum mechanic written in an Eulerian frame make no difference between fluids and solids except in the expression of the stress tensors, usually with Newton's hypothesis for the fluids and Helmholtz potentials of energy for hyperelastic solids. By taking the velocities as unknown , monolithic methods for fluid structure interactions (FSI) are built. In this article such a formulation is analyzed when the fluid is compressible and the fluid is incompressible. The idea is not new but the progress of mesh generators and numerical schemes like the Characteristics-Galerkin method render this approach feasible and reasonably robust. In this article the method and its discretization are presented, stability is discussed by through an energy estimate. A numerical section discusses implementation issues and presents a few simple tests.
Walking on Partial Footholds Including Line Contacts with the Humanoid Robot Atlas
Venue: arXiv cs.RO 2017
Year: 2017

We present a method for humanoid robot walking on partial footholds such as small stepping stones and rocks with sharp surfaces. Our algorithm does not rely on prior knowledge of the foothold, but information about an expected foothold can be used to improve the stepping performance. After a step is taken, the robot explores the new contact surface by attempting to shift the center of pressure around the foot. The available foothold is inferred by the way in which the foot rotates about contact edges and/or by the achieved center of pressure locations on the foot during exploration. This estimated contact area is then used by a whole body momentum-based control algorithm. To walk and balance on partial footholds, we combine fast, dynamic stepping with the use of upper body angular momentum to regain balance. We applied this method to the Atlas humanoid designed by Boston Dynamics to walk over small contact surfaces, such as line and point contacts. We present experimental results and discuss performance limitations.
SSDH: Semi-supervised Deep Hashing for Large Scale Image Retrieval
Venue: arXiv cs.CV 2017
Year: 2017

Hashing methods have been widely used for efficient similarity retrieval on large scale image database. Traditional hashing methods learn hash functions to generate binary codes from hand-crafted features, which achieve limited accuracy since the hand-crafted features cannot optimally represent the image content and preserve the semantic similarity. Recently, several deep hashing methods have shown better performance because the deep architectures generate more discriminative feature representations. However, these deep hashing methods are mainly designed for supervised scenarios, which only exploit the semantic similarity information, but ignore the underlying data structures. In this paper, we propose the semi-supervised deep hashing (SSDH) approach, to perform more effective hash function learning by simultaneously preserving semantic similarity and underlying data structures. The main contributions are as follows: (1) We propose a semi-supervised loss to jointly minimize the empirical error on labeled data, as well as the embedding error on both labeled and unlabeled data, which can preserve the semantic similarity and capture the meaningful neighbors on the underlying data structures for effective hashing. (2) A semi-supervised deep hashing network is designed to extensively exploit both labeled and unlabeled data, in which we propose an online graph construction method to benefit from the evolving deep features during training to better capture semantic neighbors. To the best of our knowledge, the proposed deep network is the first deep hashing method that can perform hash code learning and feature learning simultaneously in a semi-supervised fashion. Experimental results on 5 widely-used datasets show that our proposed approach outperforms the state-of-the-art hashing methods.
Computing minimum cuts in hypergraphs
Venue: arXiv cs.DS 2017
Year: 2017

We study algorithmic and structural aspects of connectivity in hypergraphs. Given a hypergraph $H=(V,E)$ with $n = |V|$, $m = |E|$ and $p = \sum_{e \in E} |e|$ the best known algorithm to compute a global minimum cut in $H$ runs in time $O(np)$ for the uncapacitated case and in $O(np + n^2 \log n)$ time for the capacitated case. We show the following new results. 1. Given an uncapacitated hypergraph $H$ and an integer $k$ we describe an algorithm that runs in $O(p)$ time to find a subhypergraph $H'$ with sum of degrees $O(kn)$ that preserves all edge-connectivities up to $k$ (a $k$-sparsifier). This generalizes the corresponding result of Nagamochi and Ibaraki from graphs to hypergraphs. Using this sparsification we obtain an $O(p + λn^2)$ time algorithm for computing a global minimum cut of $H$ where $λ$ is the minimum cut value. 2. We generalize Matula's argument for graphs to hypergraphs and obtain a $(2+ε)$-approximation to the global minimum cut in a capacitated hypergraph in $O(\frac{1}ε (p \log n + n \log^2 n))$ time. 3. We show that a hypercactus representation of all the global minimum cuts of a capacitated hypergraph can be computed in $O(np + n^2 \log n)$ time and $O(p)$ space. We utilize vertex ordering based ideas to obtain our results. Unlike graphs we observe that there are several different orderings for hypergraphs which yield different insights.
TopicResponse: A Marriage of Topic Modelling and Rasch Modelling for Automatic Measurement in MOOCs
Venue: arXiv cs.LG 2017
Year: 2017

This paper explores the suitability of using automatically discovered topics from MOOC discussion forums for modelling students' academic abilities. The Rasch model from psychometrics is a popular generative probabilistic model that relates latent student skill, latent item difficulty, and observed student-item responses within a principled, unified framework. According to scholarly educational theory, discovered topics can be regarded as appropriate measurement items if (1) students' participation across the discovered topics is well fit by the Rasch model, and if (2) the topics are interpretable to subject-matter experts as being educationally meaningful. Such Rasch-scaled topics, with associated difficulty levels, could be of potential benefit to curriculum refinement, student assessment and personalised feedback. The technical challenge that remains, is to discover meaningful topics that simultaneously achieve good statistical fit with the Rasch model. To address this challenge, we combine the Rasch model with non-negative matrix factorisation based topic modelling, jointly fitting both models. We demonstrate the suitability of our approach with quantitative experiments on data from three Coursera MOOCs, and with qualitative survey results on topic interpretability on a Discrete Optimisation MOOC.
Near-Optimal Self-Stabilising Counting and Firing Squads
Venue: arXiv cs.DC 2017
Year: 2017

Consider a fully-connected synchronous distributed system consisting of $n$ nodes, where up to $f$ nodes may be faulty and every node starts in an arbitrary initial state. In the synchronous $C$-counting problem, all nodes need to eventually agree on a counter that is increased by one modulo $C$ in each round for given $C>1$. In the self-stabilising firing squad problem, the task is to eventually guarantee that all non-faulty nodes have simultaneous responses to external inputs: if a subset of the correct nodes receive an external "go" signal as input, then all correct nodes should agree on a round (in the not-too-distant future) in which to jointly output a "fire" signal. Moreover, no node should generate a "fire" signal without some correct node having previously received a "go" signal as input. We present a framework reducing both tasks to binary consensus at very small cost. For example, we obtain a deterministic algorithm for self-stabilising Byzantine firing squads with optimal resilience $f<n/3$, asymptotically optimal stabilisation and response time $O(f)$, and message size $O(\log f)$. As our framework does not restrict the type of consensus routines used, we also obtain efficient randomised solutions, and it is straightforward to adapt our framework for other types of permanent faults.
Node Placement and Distributed Magnetic Beamforming Optimization for Wireless Power Transfer
Venue: arXiv cs.SY 2017
Year: 2017

In multiple-input single-output (MISO) wireless power transfer (WPT) via magnetic resonant coupling (MRC), multiple transmitters are deployed to enhance the efficiency of power transfer to the electric load at a single receiver by jointly optimizing their source currents/voltages to constructively combine the induced magnetic fields at the receiver, known as magnetic beamforming. In practice, since the transmitters (power chargers) are usually at fixed locations and the receiver (e.g. mobile phone) is desired to be freely located in a target region for wireless charging, its received power can fluctuate significantly over locations even with adaptive magnetic beamforming applied. To achieve uniform coverage, the transmitters need to be optimally placed in the region, which motivates this paper. First, we derive the optimal magnetic beamforming solution in closed-form for a distributed MISO WPT system with given locations of the transmitters and receiver to maximize the deliverable power to the receiver load subject to a given sum-power constraint at all transmitters. With the optimal magnetic beamforming solution, we then jointly optimize the locations of all transmitters to maximize the minimum power deliverable to the receiver when it is being moved over a given one-dimensional (1D) region, i.e., a line of finite length. Although the formulated node placement problem is non-convex, we propose an iterative algorithm for solving it efficiently. Extensive simulation results are provided which show the significant performance gains by the proposed design with optimized transmitter locations and magnetic beamforming as compared to other benchmark schemes with non-adaptive or heuristic currents allocation and transmitters placement. Last, we extend the node placement problem to the more general case of two-dimensional (2D) region, and draw the key insights.
Fast and robust pushbroom hyperspectral imaging via DMD-based scanning
Venue: arXiv cs.CV 2017
Year: 2017

We describe a new pushbroom hyperspectral imaging device that has no macro moving part. The main components of the proposed hyperspectral imager are a digital micromirror device (DMD), a CMOS image sensor with no filter as the spectral sensor, a CMOS color (RGB) image sensor as the auxiliary image sensor, and a diffraction grating. Using the image sensor pair, the device can simultaneously capture hyperspectral data as well as RGB images of the scene. The RGB images captured by the auxiliary image sensor can facilitate geometric co-registration of the hyperspectral image slices captured by the spectral sensor. In addition, the information discernible from the RGB images can lead to capturing the spectral data of only the regions of interest within the scene. The proposed hyperspectral imaging architecture is cost-effective, fast, and robust. It also enables a trade-off between resolution and speed. We have built an initial prototype based on the proposed design. The prototype can capture a hyperspectral image datacube with a spatial resolution of 192x192 pixels and a spectral resolution of 500 bands in less than thirty seconds.
On the Complexity of Constrained Determinantal Point Processes
Venue: arXiv cs.DS 2017
Year: 2017

Determinantal Point Processes (DPPs) are probabilistic models that arise in quantum physics and random matrix theory and have recently found numerous applications in computer science. DPPs define distributions over subsets of a given ground set, they exhibit interesting properties such as negative correlation, and, unlike other models, have efficient algorithms for sampling. When applied to kernel methods in machine learning, DPPs favor subsets of the given data with more diverse features. However, many real-world applications require efficient algorithms to sample from DPPs with additional constraints on the subset, e.g., partition or matroid constraints that are important to ensure priors, resource or fairness constraints on the sampled subset. Whether one can efficiently sample from DPPs in such constrained settings is an important problem that was first raised in a survey of DPPs by \cite{KuleszaTaskar12} and studied in some recent works in the machine learning literature. The main contribution of our paper is the first resolution of the complexity of sampling from DPPs with constraints. We give exact efficient algorithms for sampling from constrained DPPs when their description is in unary. Furthermore, we prove that when the constraints are specified in binary, this problem is #P-hard via a reduction from the problem of computing mixed discriminants implying that it may be unlikely that there is an FPRAS. Our results benefit from viewing the constrained sampling problem via the lens of polynomials. Consequently, we obtain a few algorithms of independent interest: 1) to count over the base polytope of regular matroids when there are additional (succinct) budget constraints and, 2) to evaluate and compute the mixed characteristic polynomials, that played a central role in the resolution of the Kadison-Singer problem, for certain special cases.
Efficient Multiple Incremental Computation for Kernel Ridge Regression with Bayesian Uncertainty Modeling
Venue: arXiv cs.LG 2017
Year: 2017

This study presents an efficient incremental/decremental approach for big streams based on Kernel Ridge Regression (KRR), a frequently used data analysis in cloud centers. To avoid reanalyzing the whole dataset whenever sensors receive new training data, typical incremental KRR used a single-instance mechanism for updating an existing system. However, this inevitably increased redundant computational time, not to mention applicability to big streams. To this end, the proposed mechanism supports incremental/decremental processing for both single and multiple samples (i.e., batch processing). A large scale of data can be divided into batches, processed by a machine, without sacrificing the accuracy. Moreover, incremental/decremental analyses in empirical and intrinsic space are also proposed in this study to handle different types of data either with a large number of samples or high feature dimensions, whereas typical methods focused only on one type. At the end of this study, we further the proposed mechanism to statistical Kernelized Bayesian Regression, so that uncertainty modeling with incremental/decremental computation becomes applicable. Experimental results showed that computational time was significantly reduced, better than the original nonincremental design and the typical single incremental method. Furthermore, the accuracy of the proposed method remained the same as the baselines. This implied that the system enhanced efficiency without sacrificing the accuracy. These findings proved that the proposed method was appropriate for variable streaming data analysis, thereby demonstrating the effectiveness of the proposed method.
A note on sub-orthogonal lattices
Venue: arXiv cs.IT 2017
Year: 2017

It is shown that, given any $k$-dimensional lattice $Λ$, there is a lattice sequence $Λ_w$, $w\in \mathbb Z$, with sub-orthogonal lattice $Λ_o \subset Λ$, converging to $Λ$ (unless equivalence), also we discuss the conditions for faster convergence.
Distributed Scheduling of Event Analytics across Edge and Cloud
Venue: arXiv cs.DC 2017
Year: 2017

Internet of Things (IoT) domains generate large volumes of high velocity event streams from sensors, which need to be analyzed with low latency to drive decisions. Complex Event Processing (CEP) is a Big Data technique to enable such analytics, and is traditionally performed on Cloud Virtual Machines (VM). Leveraging captive IoT edge resources in combination with Cloud VMs can offer better performance, flexibility and monetary costs for CEP. Here, we formulate an optimization problem for energy-aware placement of CEP queries, composed as an analytics dataflow, across a collection of edge and Cloud resources, with the goal of minimizing the end-to-end latency for the dataflow. We propose a Genetic Algorithm (GA) meta-heuristic to solve this problem, and compare it against a brute-force optimal algorithm (BF). We perform detailed real-world benchmarks on the compute, network and energy capacity of edge and Cloud resources. These results are used to define a realistic and comprehensive simulation study that validates the BF and GA solutions for 45 diverse CEP dataflows, LAN and WAN setup, and different edge resource availability. We compare the GA and BF solutions against random and Cloud-only baselines for different configurations, for a total of 1764 simulation runs. Our study shows that GA is within 97% of the optimal BF solution that takes hours, maps dataflows with 4 - 50 queries in 1 - 26 secs, and only fails to offer a feasible solution <= 20% of the time.
Molecular Model Checking a Temporal Logic
Venue: arXiv cs.LO 2017
Year: 2017

The molecular computing has been successfully employed to solve more and more complex computation problems. However, as an important complex problem, the model checking are still far from fully resolved under the circumstance of molecular computing, since it is still a lack of method. To address this issue, a model checking method is presented for checking the basic constructs in a given temporal logic using molecular computing. Through the design of the new encoding and calling this process, we get a molecule-based approach for checking all of the basic constructs of this logic.
OCR of historical printings with an application to building diachronic corpora: A case study using the RIDGES herbal corpus
Venue: arXiv cs.CL 2017
Year: 2017

This article describes the results of a case study that applies Neural Network-based Optical Character Recognition (OCR) to scanned images of books printed between 1487 and 1870 by training the OCR engine OCRopus [@breuel2013high] on the RIDGES herbal text corpus [@OdebrechtEtAlSubmitted]. Training specific OCR models was possible because the necessary *ground truth* is available as error-corrected diplomatic transcriptions. The OCR results have been evaluated for accuracy against the ground truth of unseen test sets. Character and word accuracies (percentage of correctly recognized items) for the resulting machine-readable texts of individual documents range from 94% to more than 99% (character level) and from 76% to 97% (word level). This includes the earliest printed books, which were thought to be inaccessible by OCR methods until recently. Furthermore, OCR models trained on one part of the corpus consisting of books with different printing dates and different typesets *(mixed models)* have been tested for their predictive power on the books from the other part containing yet other fonts, mostly yielding character accuracies well above 90%. It therefore seems possible to construct generalized models trained on a range of fonts that can be applied to a wide variety of historical printings still giving good results. A moderate postcorrection effort of some pages will then enable the training of individual models with even better accuracies. Using this method, diachronic corpora including early printings can be constructed much faster and cheaper than by manual transcription. The OCR methods reported here open up the possibility of transforming our printed textual cultural heritage into electronic text by largely automatic means, which is a prerequisite for the mass conversion of scanned books.
Analysis and Control of Aircraft Longitudinal Dynamics with Large Flight Envelopes
Venue: arXiv cs.SY 2017
Year: 2017

The paper contributes towards the development of a unified control approach for longitudinal aircraft dynamics with large flight envelopes. Prior to the control design, we analyze the existence and the uniqueness of the equilibrium orientation along a reference velocity. We show that shape symmetries and aerodynamic stall phenomena imply the existence of the equilibrium orientation irrespective of the reference velocity. The equilibrium orientation, however, is not in general unique, and this may trigger an aircraft loss-of-control for specific reference velocities. Conditions that ensure the local and the global uniqueness of the equilibrium orientation are stated. We show that the uniqueness of the equilibrium orientation is intimately related to the so-called spherical equivalency, i.e. the existence of a thrust change of variable rendering the direction of the transformed external force independent of the vehicle's orientation, as in the case of spherical shapes. Once this transformation is applied, control laws for reference velocities can be designed. These laws extend the so-called vectored--thrust control paradigm %developed for systems subject to orientation-independent external forces, e.g. spherical shapes, to the case of generic body shapes subject to steady aerodynamics.