OpenRaiser/Intern-Atlas huggingface dataset:
Temporal Logic as Filtering
Venue: arXiv cs.LO 2016
Year: 2016

We show that metric temporal logic can be viewed as linear time-invariant filtering, by interpreting addition, multiplication, and their neutral elements, over the (max,min,0,1) idempotent dioid. Moreover, by interpreting these operators over the field of reals (+,*,0,1), one can associate various quantitative semantics to a metric-temporal-logic formula, depending on the filter's kernel used: square, rounded-square, Gaussian, low-pass, band-pass, or high-pass. This remarkable connection between filtering and metric temporal logic allows us to freely navigate between the two, and to regard signal-feature detection as logical inference. To the best of our knowledge, this connection has not been established before. We prove that our qualitative, filtering semantics is identical to the classical MTL semantics. We also provide a quantitative semantics for MTL, which measures the normalized, maximum number of times a formula is satisfied within its associated kernel, by a given signal. We show that this semantics is sound, in the sense that, if its measure is 0, then the formula is not satisfied, and it is satisfied otherwise. We have implemented both of our semantics in Matlab, and illustrate their properties on various formulas and signals, by plotting their computed measures.
Beyond Level Planarity
Venue: arXiv cs.DS 2016
Year: 2016

In this paper we settle the computational complexity of two open problems related to the extension of the notion of level planarity to surfaces different from the plane. Namely, we show that the problems of testing the existence of a level embedding of a level graph on the surface of the rolling cylinder or on the surface of the torus, respectively known by the name of $\textit{Cyclic Level Planarity}$ and $\textit{Torus Level Planarity}$, are polynomial-time solvable. Moreover, we show a complexity dichotomy for testing the $\textit{Simultaneous Level Planarity}$ of a set of level graphs, with respect to both the number of level graphs and the number of levels.
Multivariate Fronthaul Quantization for Downlink C-RAN
Venue: arXiv cs.IT 2016
Year: 2016

The Cloud-Radio Access Network (C-RAN) cellular architecture relies on the transfer of complex baseband signals to and from a central unit (CU) over digital fronthaul links to enable the virtualization of the baseband processing functionalities of distributed radio units (RUs). The standard design of digital fronthauling is based on either scalar quantization or on more sophisticated point to-point compression techniques operating on baseband signals. Motivated by network-information theoretic results, techniques for fronthaul quantization and compression that improve over point-to-point solutions by allowing for joint processing across multiple fronthaul links at the CU have been recently proposed for both the uplink and the downlink. For the downlink, a form of joint compression, known in network information theory as multivariate compression, was shown to be advantageous under a non-constructive asymptotic information-theoretic framework. In this paper, instead, the design of a practical symbol-by-symbol fronthaul quantization algorithm that implements the idea of multivariate compression is investigated for the C-RAN downlink. As compared to current standards, the proposed multivariate quantization (MQ) only requires changes in the CU processing while no modification is needed at the RUs. The algorithm is extended to enable the joint optimization of downlink precoding and quantization, reduced-complexity MQ via successive block quantization, and variable-length compression. Numerical results, which include performance evaluations over standard cellular models, demonstrate the advantages of MQ and the merits of a joint optimization with precoding.
A theory on power in networks
Venue: arXiv cs.SI 2016
Year: 2016

The eigenvector centrality equation $λx = A \, x$ is a successful compromise between simplicity and expressivity. It claims that central actors are those connected with central others. For at least 70 years, this equation has been explored in disparate contexts, including econometrics, sociometry, bibliometrics, Web information retrieval, and network science. We propose an equally elegant counterpart: the power equation $x = A x^÷$, where $x^÷$ is the vector whose entries are the reciprocal of those of $x$. It asserts that power is in the hands of those connected with powerless others. It is meaningful, for instance, in bargaining situations, where it is advantageous to be connected to those who have few options. We tell the parallel, mostly unexplored story of this intriguing equation.
Switching control for incremental stabilization of nonlinear systems via contraction theory
Venue: arXiv cs.SY 2016
Year: 2016

In this paper we present a switching control strategy to incrementally stabilize a class of nonlinear dynamical systems. Exploiting recent results on contraction analysis of switched Filippov systems derived using regularization, sufficient conditions are presented to prove incremental stability of the closed-loop system. Furthermore, based on these sufficient conditions, a design procedure is proposed to design a switched control action that is active only where the open-loop system is not sufficiently incrementally stable in order to reduce the required control effort. The design procedure to either locally or globally incrementally stabilize a dynamical system is then illustrated by means of a representative example.
Program Synthesis from Polymorphic Refinement Types
Venue: arXiv cs.PL 2016
Year: 2016

We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification---and hence synthesis---of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a new algorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. The tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input.
A Coinductive Approach to Computing with Compact Sets
Venue: arXiv cs.LO 2016
Year: 2016

Exact representations of real numbers such as the signed digit representation or more generally linear fractional representations or the infinite Gray code represent real numbers as infinite streams of digits. In earlier work by the first author it was shown how to extract certified algorithms working with the signed digit representations from constructive proofs. In this paper we lay the foundation for doing a similar thing with nonempty compact sets. It turns out that a representation by streams of finitely many digits is impossible and instead trees are needed.
Mixed Robust/Average Submodular Partitioning: Fast Algorithms, Guarantees, and Applications to Parallel Machine Learning and Multi-Label Image Segmentation
Venue: arXiv cs.DS 2016
Year: 2016

We study two mixed robust/average-case submodular partitioning problems that we collectively call Submodular Partitioning. These problems generalize both purely robust instances of the problem (namely max-min submodular fair allocation (SFA) and min-max submodular load balancing (SLB) and also generalize average-case instances (that is the submodular welfare problem (SWP) and submodular multiway partition (SMP). While the robust versions have been studied in the theory community, existing work has focused on tight approximation guarantees, and the resultant algorithms are not, in general, scalable to very large real-world applications. This is in contrast to the average case, where most of the algorithms are scalable. In the present paper, we bridge this gap, by proposing several new algorithms (including those based on greedy, majorization-minimization, minorization-maximization, and relaxation algorithms) that not only scale to large sizes but that also achieve theoretical approximation guarantees close to the state-of-the-art, and in some cases achieve new tight bounds. We also provide new scalable algorithms that apply to additive combinations of the robust and average-case extreme objectives. We show that these problems have many applications in machine learning (ML). This includes: 1) data partitioning and load balancing for distributed machine algorithms on parallel machines; 2) data clustering; and 3) multi-label image segmentation with (only) Boolean submodular functions via pixel partitioning. We empirically demonstrate the efficacy of our algorithms on real-world problems involving data partitioning for distributed optimization of standard machine learning objectives (including both convex and deep neural network objectives), and also on purely unsupervised (i.e., no supervised or semi-supervised learning, and no interactive segmentation) image segmentation.
Bounds for Batch Codes with Restricted Query Size
Venue: arXiv cs.IT 2016
Year: 2016

We present new upper bounds on the parameters of batch codes with restricted query size. These bounds are an improvement on the Singleton bound. The techniques for derivations of these bounds are based on the ideas in the literature for codes with locality. By employing additional ideas, we obtain further improvements, which are specific for batch codes.
Robust Shift-and-Invert Preconditioning: Faster and More Sample Efficient Algorithms for Eigenvector Computation
Venue: arXiv cs.DS 2016
Year: 2016

We provide faster algorithms and improved sample complexities for approximating the top eigenvector of a matrix. Offline Setting: Given an $n \times d$ matrix $A$, we show how to compute an $ε$ approximate top eigenvector in time $\tilde O ( [nnz(A) + \frac{d \cdot sr(A)}{gap^2}]\cdot \log 1/ε)$ and $\tilde O([\frac{nnz(A)^{3/4} (d \cdot sr(A))^{1/4}}{\sqrt{gap}}]\cdot \log1/ε)$. Here $sr(A)$ is the stable rank and $gap$ is the multiplicative eigenvalue gap. By separating the $gap$ dependence from $nnz(A)$ we improve on the classic power and Lanczos methods. We also improve prior work using fast subspace embeddings and stochastic optimization, giving significantly improved dependencies on $sr(A)$ and $ε$. Our second running time improves this further when $nnz(A) \le \frac{d\cdot sr(A)}{gap^2}$. Online Setting: Given a distribution $D$ with covariance matrix $Σ$ and a vector $x_0$ which is an $O(gap)$ approximate top eigenvector for $Σ$, we show how to refine to an $ε$ approximation using $\tilde O(\frac{v(D)}{gap^2} + \frac{v(D)}{gap \cdot ε})$ samples from $D$. Here $v(D)$ is a natural variance measure. Combining our algorithm with previous work to initialize $x_0$, we obtain a number of improved sample complexity and runtime results. For general distributions, we achieve asymptotically optimal accuracy as a function of sample size as the number of samples grows large. Our results center around a robust analysis of the classic method of shift-and-invert preconditioning to reduce eigenvector computation to approximately solving a sequence of linear systems. We then apply fast SVRG based approximate system solvers to achieve our claims. We believe our results suggest the general effectiveness of shift-and-invert based approaches and imply that further computational gains may be reaped in practice.
A Model for Social Network Formation: Efficiency, Stability and Dynamics
Venue: arXiv cs.SI 2016
Year: 2016

We introduce a simple network formation model for social networks. Agents are nodes, connecting to another agent by building a directed edge (or accepting a connection from another agent) has a cost, and reaching (or being reached by) other agents via short directed paths has a benefit; in effect, an agent wants to reach others quickly, but without the cost of directly connecting each and every one. We prove that asynchronous edge dynamics always converge to a stable network; in fact, for nontrivial ranges of parameters this convergence is fast. Moreover, the set of fixed points of the dynamics form a nontrivial class of networks. For the static game, we give classes of efficient networks for nontrivial parameter ranges and further study their stability. We close several problems, and leave many interesting ones open.
Submodular Functions: from Discrete to Continous Domains
Venue: arXiv cs.LG 2016
Year: 2016

Submodular set-functions have many applications in combinatorial optimization, as they can be minimized and approximately maximized in polynomial time. A key element in many of the algorithms and analyses is the possibility of extending the submodular set-function to a convex function, which opens up tools from convex optimization. Submodularity goes beyond set-functions and has naturally been considered for problems with multiple labels or for functions defined on continuous domains, where it corresponds essentially to cross second-derivatives being nonpositive. In this paper, we show that most results relating submodularity and convexity for set-functions can be extended to all submodular functions. In particular, (a) we naturally define a continuous extension in a set of probability measures, (b) show that the extension is convex if and only if the original function is submodular, (c) prove that the problem of minimizing a submodular function is equivalent to a typically non-smooth convex optimization problem, and (d) propose another convex optimization problem with better computational properties (e.g., a smooth dual problem). Most of these extensions from the set-function situation are obtained by drawing links with the theory of multi-marginal optimal transport, which provides also a new interpretation of existing results for set-functions. We then provide practical algorithms to minimize generic submodular functions on discrete domains, with associated convergence rates.
A geometric approach to the dynamics of flapping wing micro aerial vehicles: Modelling and reduction
Venue: arXiv cs.SY 2016
Year: 2016

This paper presents a geometric framework for analysis of dynamics of flapping wing micro aerial vehicles (FWMAV) which achieve locomotion in the special Euclidean group SE(3) using internal shape changes. We review the special structure of the configuration manifold of such systems. This work addresses to extend the work in geometric locomotion to the aerial locomotion problem. Furthermore, there seems to be limited work in modelling of flapping wing bodies in a geometric framework. We derive the dynamic model of the FWMAV using Lagrangian reduction theory defined on symmetry groups. The reduction is achieved by applying Hamilton's variation principle on a reduced Lagrangian. The resultant dynamics is governed by the Euler-Poincare and Euler-Lagrange equations.
Searching input values hitting suspicious Intervals in programs with floating-point operations
Venue: arXiv cs.PL 2016
Year: 2016

Programs with floating-point computations are often derived from mathematical models or designed with the semantics of the real numbers in mind. However, for a given input, the computed path with floating-point numbers may differ from the path corresponding to the same computation with real numbers. A common practice when validating such programs consists in estimating the accuracy of floating-point computations with respect to the same sequence of operations in an ide-alized semantics of real numbers. However, state-of-the-art tools compute an over-approximation of the error introduced by floating-point operations. As a consequence, totally inappropriate behaviors of a program may be dreaded but the developer does not know whether these behaviors will actually occur, or not. In this paper, we introduce a new constraint-based approach that searches for test cases in the part of the over-approximation where errors due to floating-point arithmetic would lead to inappropriate behaviors.
How Robust are Reconstruction Thresholds for Community Detection?
Venue: arXiv cs.DS 2016
Year: 2016

The stochastic block model is one of the oldest and most ubiquitous models for studying clustering and community detection. In an exciting sequence of developments, motivated by deep but non-rigorous ideas from statistical physics, Decelle et al. conjectured a sharp threshold for when community detection is possible in the sparse regime. Mossel, Neeman and Sly and Massoulie proved the conjecture and gave matching algorithms and lower bounds. Here we revisit the stochastic block model from the perspective of semirandom models where we allow an adversary to make `helpful' changes that strengthen ties within each community and break ties between them. We show a surprising result that these `helpful' changes can shift the information-theoretic threshold, making the community detection problem strictly harder. We complement this by showing that an algorithm based on semidefinite programming (which was known to get close to the threshold) continues to work in the semirandom model (even for partial recovery). This suggests that algorithms based on semidefinite programming are robust in ways that any algorithm meeting the information-theoretic threshold cannot be. These results point to an interesting new direction: Can we find robust, semirandom analogues to some of the classical, average-case thresholds in statistics? We also explore this question in the broadcast tree model, and we show that the viewpoint of semirandom models can help explain why some algorithms are preferred to others in practice, in spite of the gaps in their statistical performance on random models.
Extension of Overbeck's Attack for Gabidulin Based Cryptosystems
Venue: arXiv cs.CR 2016
Year: 2016

We present a new attack against cryptosystems based on the rank metric. Our attack allows us to cryptanalyze two variants of the GPT cryptosystem which were designed to resist the attack of Overbeck.
Listing All Spanning Trees in Halin Graphs - Sequential and Parallel view
Venue: arXiv cs.DM 2016
Year: 2016

For a connected labelled graph $G$, a {\em spanning tree} $T$ is a connected and an acyclic subgraph that spans all vertices of $G$. In this paper, we consider a classical combinatorial problem which is to list all spanning trees of $G$. A Halin graph is a graph obtained from a tree with no degree two vertices and by joining all leaves with a cycle. We present a sequential and parallel algorithm to enumerate all spanning trees in Halin graphs. Our approach enumerates without repetitions and we make use of $O((2pd)^{p})$ processors for parallel algorithmics, where $d$ and $p$ are the depth, the number of leaves, respectively, of the Halin graph. We also prove that the number of spanning trees in Halin graphs is $O((2pd)^{p})$.
Prediction and Characterization of High-Activity Events in Social Media Triggered by Real-World News
Venue: arXiv cs.SI 2016
Year: 2016

On-line social networks publish information on a high volume of real-world events almost instantly, becoming a primary source for breaking news. Some of these real-world events can end up having a very strong impact on on-line social networks. The effect of such events can be analyzed from several perspectives, one of them being the intensity and characteristics of the collective activity that it produces in the social platform. We research 5,234 real-world news events encompassing 43 million messages discussed on the Twitter microblogging service for approximately 1 year. We show empirically that exogenous news events naturally create collective patterns of bursty behavior in combination with long periods of inactivity in the network. This type of behavior agrees with other patterns previously observed in other types of natural collective phenomena, as well as in individual human communications. In addition, we propose a methodology to classify news events according to the different levels of intensity in activity that they produce. In particular, we analyze the most highly active events and observe a consistent and strikingly different collective reaction from users when they are exposed to such events. This reaction is independent of an event's reach and scope. We further observe that extremely high-activity events have characteristics that are quite distinguishable at the beginning stages of their outbreak. This allows us to predict with high precision, the top 8% of events that will have the most impact in the social network by just using the first 5% of the information of an event's lifetime evolution. This strongly implies that high-activity events are naturally prioritized collectively by the social network, engaging users early on, way before they are brought to the mainstream audience.
2-Trees: Structural Insights and the study of Hamiltonian Paths
Venue: arXiv cs.DM 2016
Year: 2016

For a connected graph, a path containing all vertices is known as \emph{Hamiltonian path}. For general graphs, there is no known necessary and sufficient condition for the existence of Hamiltonian paths and the complexity of finding a Hamiltonian path in general graphs is NP-Complete. We present a necessary and sufficient condition for the existence of Hamiltonian paths in 2-trees. Using our characterization, we also present a linear-time algorithm for the existence of Hamiltonian paths in 2-trees. Our characterization is based on a deep understanding of the structure of 2-trees and the combinatorics presented here may be used in other combinatorial problems restricted to 2-trees.
Autotuning OpenCL Workgroup Size for Stencil Patterns
Venue: arXiv cs.DC 2016
Year: 2016

Selecting an appropriate workgroup size is critical for the performance of OpenCL kernels, and requires knowledge of the underlying hardware, the data being operated on, and the implementation of the kernel. This makes portable performance of OpenCL programs a challenging goal, since simple heuristics and statically chosen values fail to exploit the available performance. To address this, we propose the use of machine learning-enabled autotuning to automatically predict workgroup sizes for stencil patterns on CPUs and multi-GPUs. We present three methodologies for predicting workgroup sizes. The first, using classifiers to select the optimal workgroup size. The second and third proposed methodologies employ the novel use of regressors for performing classification by predicting the runtime of kernels and the relative performance of different workgroup sizes, respectively. We evaluate the effectiveness of each technique in an empirical study of 429 combinations of architecture, kernel, and dataset, comparing an average of 629 different workgroup sizes for each. We find that autotuning provides a median 3.79x speedup over the best possible fixed workgroup size, achieving 94% of the maximum performance.