OpenRaiser/Intern-Atlas huggingface dataset:
Extracting Unsatisfiable Cores for LTL via Temporal Resolution
Venue: arXiv cs.LO 2015
Year: 2015

Unsatisfiable cores (UCs) are a well established means for debugging in a declarative setting. Still, there are few tools that perform automated extraction of UCs for LTL. Existing tools compute a UC as an unsatisfiable subset of the set of top-level conjuncts of an LTL formula. Using resolution graphs to extract UCs is common in other domains such as SAT. In this article we construct and optimize resolution graphs for temporal resolution as implemented in the temporal resolution-based solver TRP++, and we use them to extract UCs for propositional LTL. The resulting UCs are more fine-grained than the UCs obtained from existing tools because UC extraction also simplifies top-level conjuncts instead of treating them as atomic entities. For example, given an unsatisfiable LTL formula of the form $ϕ\equiv ({\bf G} ψ) \wedge {\bf F} ψ'$ existing tools return $ϕ$ as a UC irrespective of the complexity of $ψ$ and $ψ'$, whereas the approach presented in this article continues to remove parts not required for unsatisfiability inside $ψ$ and $ψ'$. Our approach also identifies groups of occurrences of a proposition that do not interact in a proof of unsatisfiability. We implement our approach in TRP++. Our experimental evaluation demonstrates that our approach (i) extracts UCs that are often significantly smaller than the input formula with an acceptable overhead and (ii) produces more fine-grained UCs than competing tools while remaining at least competitive in terms of run time and memory usage. The source code of our tool is publicly available.
On the Diversity-Multiplexing Tradeoff of Unconstrained Multiple-Access Channels
Venue: arXiv cs.IT 2015
Year: 2015

In this work the optimal diversity-multiplexing tradeoff (DMT) is investigated for the multiple-input multiple-output fading multiple-access channels with no power constraints (infinite constellations). For K users (K>1), M transmit antennas for each user, and N receive antennas, infinite constellations in general and lattices in particular are shown to attain the optimal DMT of finite constellations for the case N equals or greater than (K+1)M-1, i.e., user limited regime. On the other hand for N<(K+1)M-1 it is shown that infinite constellations can not attain the optimal DMT. This is in contrast to the point-to-point case in which infinite constellations are DMT optimal for any M and N. In general, this work shows that when the network is heavily loaded, i.e. K>max(1,(N-M+1)/M), taking into account the shaping region in the decoding process plays a crucial role in pursuing the optimal DMT. By investigating the cases where infinite constellations are optimal and suboptimal, this work also gives a geometrical interpretation to the DMT of infinite constellations in multiple-access channels.
Quantitative Timed Simulation Functions and Refinement Metrics for Timed Systems (Full Version)
Venue: arXiv cs.SY 2015
Year: 2015

We introduce quantatitive timed refinement and timed simulation (directed) metrics, incorporating zenoness check s, for timed systems. These metrics assign positive real numbers between zero and infinity which quantify the \emph{timing mismatches} between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the "steady-state" maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the \emph{global times}, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata.
Graphical Models for Game Theory
Venue: arXiv cs.GT 2015
Year: 2015

In this work, we introduce graphical modelsfor multi-player game theory, and give powerful algorithms for computing their Nash equilibria in certain cases. An n-player game is given by an undirected graph on n nodes and a set of n local matrices. The interpretation is that the payoff to player i is determined entirely by the actions of player i and his neighbors in the graph, and thus the payoff matrix to player i is indexed only by these players. We thus view the global n-player game as being composed of interacting local games, each involving many fewer players. Each player's action may have global impact, but it occurs through the propagation of local influences.Our main technical result is an efficient algorithm for computing Nash equilibria when the underlying graph is a tree (or can be turned into a tree with few node mergings). The algorithm runs in time polynomial in the size of the representation (the graph and theassociated local game matrices), and comes in two related but distinct flavors. The first version involves an approximation step, and computes a representation of all approximate Nash equilibria (of which there may be an exponential number in general). The second version allows the exact computation of Nash equilibria at the expense of weakened complexity bounds. The algorithm requires only local message-passing between nodes (and thus can be implemented by the players themselves in a distributed manner). Despite an analogy to inference in Bayes nets that we develop, the analysis of our algorithm is more involved than that for the polytree algorithm in, owing partially to the fact that we must either compute, or select from, an exponential number of potential solutions. We discuss a number of extensions, such as the computation of equilibria with desirable global properties (e.g. maximizing global return), and directions for further research.
On the Identifiability of Overcomplete Dictionaries via the Minimisation Principle Underlying K-SVD
Venue: arXiv cs.IT 2015
Year: 2015

This article gives theoretical insights into the performance of K-SVD, a dictionary learning algorithm that has gained significant popularity in practical applications. The particular question studied here is when a dictionary $Φ\in \mathbb{R}^{d \times K}$ can be recovered as local minimum of the minimisation criterion underlying K-SVD from a set of $N$ training signals $y_n =Φx_n$. A theoretical analysis of the problem leads to two types of identifiability results assuming the training signals are generated from a tight frame with coefficients drawn from a random symmetric distribution. First, asymptotic results showing, that in expectation the generating dictionary can be recovered exactly as a local minimum of the K-SVD criterion if the coefficient distribution exhibits sufficient decay. Second, based on the asymptotic results it is demonstrated that given a finite number of training samples $N$, such that $N/\log N = O(K^3d)$, except with probability $O(N^{-Kd})$ there is a local minimum of the K-SVD criterion within distance $O(KN^{-1/4})$ to the generating dictionary.
Learnable Pooling Regions for Image Classification
Venue: arXiv cs.CV 2015
Year: 2015

Biologically inspired, from the early HMAX model to Spatial Pyramid Matching, pooling has played an important role in visual recognition pipelines. Spatial pooling, by grouping of local codes, equips these methods with a certain degree of robustness to translation and deformation yet preserving important spatial information. Despite the predominance of this approach in current recognition systems, we have seen little progress to fully adapt the pooling strategy to the task at hand. This paper proposes a model for learning task dependent pooling scheme -- including previously proposed hand-crafted pooling schemes as a particular instantiation. In our work, we investigate the role of different regularization terms showing that the smooth regularization term is crucial to achieve strong performance using the presented architecture. Finally, we propose an efficient and parallel method to train the model. Our experiments show improved performance over hand-crafted pooling schemes on the CIFAR-10 and CIFAR-100 datasets -- in particular improving the state-of-the-art to 56.29% on the latter.
Spatial Coupling as a Proof Technique
Venue: arXiv cs.IT 2015
Year: 2015

The aim of this paper is to show that spatial coupling can be viewed not only as a means to build better graphical models, but also as a tool to better understand uncoupled models. The starting point is the observation that some asymptotic properties of graphical models are easier to prove in the case of spatial coupling. In such cases, one can then use the so-called interpolation method to transfer known results for the spatially coupled case to the uncoupled one. Our main use of this framework is for LDPC codes, where we use interpolation to show that the average entropy of the codeword conditioned on the observation is asymptotically the same for spatially coupled as for uncoupled ensembles. We give three applications of this result for a large class of LDPC ensembles. The first one is a proof of the so-called Maxwell construction stating that the MAP threshold is equal to the Area threshold of the BP GEXIT curve. The second is a proof of the equality between the BP and MAP GEXIT curves above the MAP threshold. The third application is the intimately related fact that the replica symmetric formula for the conditional entropy in the infinite block length limit is exact.
State-Dependent Z Channel
Venue: arXiv cs.IT 2015
Year: 2015

In this paper we study the Z channel with side information non-causally available at the encoders. We use Marton encoding along with Gelfand-Pinsker random binning scheme and Chong-Motani-Garg-El Gamal (CMGE) jointly decoding to find an achievable rate region. We will see that our achievable rate region gives the achievable rate of the multiple access channel with side information and also degraded broadcast channel with side information. We will also derive an inner bound and an outer bound on the capacity region of the state-dependent degraded discrete memoryless Z channel and also will observe that our outer bound meets the inner bound for the rates corresponding to the second transmitter. Also, by assuming the high signal to noise ratio and strong interference regime, and using the lattice strategies, we derive an achievable rate region for the Gaussian degraded Z channel with additive interference non-causally available at both of the encoders. Our method is based on lattice transmission scheme, jointly decoding at the first decoder and successive decoding at the second decoder. Using such coding scheme we remove the effect of the interference completely.
How to Meet Asynchronously at Polynomial Cost
Venue: arXiv cs.DS 2015
Year: 2015

Two mobile agents starting at different nodes of an unknown network have to meet. This task is known in the literature as rendezvous. Each agent has a different label which is a positive integer known to it, but unknown to the other agent. Agents move in an asynchronous way: the speed of agents may vary and is controlled by an adversary. The cost of a rendezvous algorithm is the total number of edge traversals by both agents until their meeting. The only previous deterministic algorithm solving this problem has cost exponential in the size of the graph and in the larger label. In this paper we present a deterministic rendezvous algorithm with cost polynomial in the size of the graph and in the length of the smaller label. Hence we decrease the cost exponentially in the size of the graph and doubly exponentially in the labels of agents. As an application of our rendezvous algorithm we solve several fundamental problems involving teams of unknown size larger than 1 of labeled agents moving asynchronously in unknown networks. Among them are the following problems: team size, in which every agent has to find the total number of agents, leader election, in which all agents have to output the label of a single agent, perfect renaming in which all agents have to adopt new different labels from the set {1, . . . , k}, where k is the number of agents, and gossiping, in which each agent has initially a piece of information (value) and all agents have to output all the values. Using our rendezvous algorithm we solve all these problems at cost polynomial in the size of the graph and in the smallest length of all labels of participating agents.
Baselining Network-Wide Traffic by Time-Frequency Constrained Stable Principal Component Pursuit
Venue: arXiv cs.NI 2015
Year: 2015

The Internet traffic analysis is important to network management,and extracting the baseline traffic patterns is especially helpful for some significant network applications.In this paper, we study on the baseline problem of the traffic matrix satisfying a refined traffic matrix decomposition model,since this model extends the assumption of the baseline traffic component to characterize its smoothness, and is more realistic than the existing traffic matrix models. We develop a novel baseline scheme, named Stable Principal Component Pursuit with Time-Frequency Constraints (SPCP-TFC), which extends the Stable Principal Component Pursuit (SPCP) by applying new time-frequency constraints. Then we design an efficient numerical algorithm for SPCP-TFC. At last, we evaluate this baseline scheme through simulations, and show it has superior performance than the existing baseline schemes RBL and PCA.
A Definition and Graphical Representation for Causality
Venue: arXiv cs.AI 2015
Year: 2015

We present a precise definition of cause and effect in terms of a fundamental notion called unresponsiveness. Our definition is based on Savage's (1954) formulation of decision theory and departs from the traditional view of causation in that our causal assertions are made relative to a set of decisions. An important consequence of this departure is that we can reason about cause locally, not requiring a causal explanation for every dependency. Such local reasoning can be beneficial because it may not be necessary to determine whether a particular dependency is causal to make a decision. Also in this paper, we examine the graphical encoding of causal relationships. We show that influence diagrams in canonical form are an accurate and efficient representation of causal relationships. In addition, we establish a correspondence between canonical form and Pearl's causal theory.
Learning Bayesian Networks: The Combination of Knowledge and Statistical Data
Venue: arXiv cs.AI 2015
Year: 2015

We describe algorithms for learning Bayesian networks from a combination of user knowledge and statistical data. The algorithms have two components: a scoring metric and a search procedure. The scoring metric takes a network structure, statistical data, and a user's prior knowledge, and returns a score proportional to the posterior probability of the network structure given the data. The search procedure generates networks for evaluation by the scoring metric. Our contributions are threefold. First, we identify two important properties of metrics, which we call event equivalence and parameter modularity. These properties have been mostly ignored, but when combined, greatly simplify the encoding of a user's prior knowledge. In particular, a user can express her knowledge-for the most part-as a single prior Bayesian network for the domain. Second, we describe local search and annealing algorithms to be used in conjunction with scoring metrics. In the special case where each node has at most one parent, we show that heuristic search can be replaced with a polynomial algorithm to identify the networks with the highest score. Third, we describe a methodology for evaluating Bayesian-network learning algorithms. We apply this approach to a comparison of metrics and search procedures.
A Decision-Based View of Causality
Venue: arXiv cs.AI 2015
Year: 2015

Most traditional models of uncertainty have focused on the associational relationship among variables as captured by conditional dependence. In order to successfully manage intelligent systems for decision making, however, we must be able to predict the effects of actions. In this paper, we attempt to unite two branches of research that address such predictions: causal modeling and decision analysis. First, we provide a definition of causal dependence in decision-analytic terms, which we derive from consequences of causal dependence cited in the literature. Using this definition, we show how causal dependence can be represented within an influence diagram. In particular, we identify two inadequacies of an ordinary influence diagram as a representation for cause. We introduce a special class of influence diagrams, called causal influence diagrams, which corrects one of these problems, and identify situations where the other inadequacy can be eliminated. In addition, we describe the relationships between Howard Canonical Form and existing graphical representations of cause.
Riemannian metrics for neural networks I: feedforward networks
Venue: arXiv cs.NE 2015
Year: 2015

We describe four algorithms for neural network training, each adapted to different scalability constraints. These algorithms are mathematically principled and invariant under a number of transformations in data and network representation, from which performance is thus independent. These algorithms are obtained from the setting of differential geometry, and are based on either the natural gradient using the Fisher information matrix, or on Hessian methods, scaled down in a specific way to allow for scalability while keeping some of their key mathematical properties.
Application of the SP theory of intelligence to the understanding of natural vision and the development of computer vision
Venue: arXiv cs.CV 2015
Year: 2015

The SP theory of intelligence aims to simplify and integrate concepts in computing and cognition, with information compression as a unifying theme. This article discusses how it may be applied to the understanding of natural vision and the development of computer vision. The theory, which is described quite fully elsewhere, is described here in outline but with enough detail to ensure that the rest of the article makes sense. Low level perceptual features such as edges or corners may be identified by the extraction of redundancy in uniform areas in a manner that is comparable with the run-length encoding technique for information compression. The concept of multiple alignment in the SP theory may be applied to the recognition of objects, and to scene analysis, with a hierarchy of parts and sub-parts, and at multiple levels of abstraction. The theory has potential for the unsupervised learning of visual objects and classes of objects, and suggests how coherent concepts may be derived from fragments. As in natural vision, both recognition and learning in the SP system is robust in the face of errors of omission, commission and substitution. The theory suggests how, via vision, we may piece together a knowledge of the three-dimensional structure of objects and of our environment, it provides an account of how we may see things that are not objectively present in an image, and how we recognise something despite variations in the size of its retinal image. And it has things to say about the phenomena of lightness constancy and colour constancy, the role of context in recognition, and ambiguities in visual perception. A strength of the SP theory is that it provides for the integration of vision with other sensory modalities and with other aspects of intelligence.
Group-Sparse Model Selection: Hardness and Relaxations
Venue: arXiv cs.LG 2015
Year: 2015

Group-based sparsity models are proven instrumental in linear regression problems for recovering signals from much fewer measurements than standard compressive sensing. The main promise of these models is the recovery of "interpretable" signals through the identification of their constituent groups. In this paper, we establish a combinatorial framework for group-model selection problems and highlight the underlying tractability issues. In particular, we show that the group-model selection problem is equivalent to the well-known NP-hard weighted maximum coverage problem (WMC). Leveraging a graph-based understanding of group models, we describe group structures which enable correct model selection in polynomial time via dynamic programming. Furthermore, group structures that lead to totally unimodular constraints have tractable discrete as well as convex relaxations. We also present a generalization of the group-model that allows for within group sparsity, which can be used to model hierarchical sparsity. Finally, we study the Pareto frontier of group-sparse approximations for two tractable models, among which the tree sparsity model, and illustrate selection and computation trade-offs between our framework and the existing convex relaxations.
Strategic Intelligence on Emerging Technologies: Scientometric Overlay Mapping
Venue: arXiv cs.DL 2015
Year: 2015

This paper examines the use of scientometric overlay mapping as a tool of 'strategic intelligence' to aid the governance of emerging technologies. We develop an integrative synthesis of different overlay mapping techniques and associated perspectives on technological emergence across the geographical, social, and cognitive spaces. To do so, we longitudinally analyse (with publication and patent data) three case-studies of emerging technologies in the medical domain. These are: RNA interference (RNAi), Human Papilloma Virus (HPV) testing technologies for cervical cancer, and Thiopurine Methyltransferase (TPMT) genetic testing. Given the flexibility (i.e. adaptability to different sources of data) and granularity (i.e. applicability across multiple levels of data aggregation) of overlay mapping techniques, we argue that these techniques can favour the integration and comparison of results from different contexts and cases, thus potentially functioning as platform for a 'distributed' strategic intelligence for analysts and decision-makers.
The traveling salesman problem for lines, balls and planes
Venue: arXiv cs.CG 2015
Year: 2015

We revisit the traveling salesman problem with neighborhoods (TSPN) and propose several new approximation algorithms. These constitute either first approximations (for hyperplanes, lines, and balls in $\mathbb{R}^d$, for $d\geq 3$) or improvements over previous approximations achievable in comparable times (for unit disks in the plane). \smallskip (I) Given a set of $n$ hyperplanes in $\mathbb{R}^d$, a TSP tour whose length is at most $O(1)$ times the optimal can be computed in $O(n)$ time, when $d$ is constant. \smallskip (II) Given a set of $n$ lines in $\mathbb{R}^d$, a TSP tour whose length is at most $O(\log^3 n)$ times the optimal can be computed in polynomial time for all $d$. \smallskip (III) Given a set of $n$ unit balls in $\mathbb{R}^d$, a TSP tour whose length is at most $O(1)$ times the optimal can be computed in polynomial time, when $d$ is constant.