OpenRaiser/Intern-Atlas huggingface dataset:
Simple Distributed Delta + 1 Coloring in the SINR Model
Venue: arXiv cs.DS 2015
Year: 2015

In wireless ad hoc or sensor networks, distributed node coloring is a fundamental problem closely related to establishing efficient communication through TDMA schedules. For networks with maximum degree Delta, a Delta + 1 coloring is the ultimate goal in the distributed setting as this is always possible. In this work we propose Delta + 1 coloring algorithms for the synchronous and asynchronous setting. All algorithms have a runtime of O(Delta log n) time slots. This improves on the previous algorithms for the SINR model either in terms of the number of required colors or the runtime and matches the runtime of local broadcasting in the SINR model (which can be seen as a lower bound).
Deep Neural Networks for Anatomical Brain Segmentation
Venue: arXiv cs.CV 2015
Year: 2015

We present a novel approach to automatically segment magnetic resonance (MR) images of the human brain into anatomical regions. Our methodology is based on a deep artificial neural network that assigns each voxel in an MR image of the brain to its corresponding anatomical region. The inputs of the network capture information at different scales around the voxel of interest: 3D and orthogonal 2D intensity patches capture the local spatial context while large, compressed 2D orthogonal patches and distances to the regional centroids enforce global spatial consistency. Contrary to commonly used segmentation methods, our technique does not require any non-linear registration of the MR images. To benchmark our model, we used the dataset provided for the MICCAI 2012 challenge on multi-atlas labelling, which consists of 35 manually segmented MR images of the brain. We obtained competitive results (mean dice coefficient 0.725, error rate 0.163) showing the potential of our approach. To our knowledge, our technique is the first to tackle the anatomical segmentation of the whole brain using deep neural networks.
Real root finding for rank defects in linear Hankel matrices
Venue: arXiv cs.SC 2015
Year: 2015

Let $H\_0, ..., H\_n$ be $m \times m$ matrices with entries in $\QQ$ and Hankel structure, i.e. constant skew diagonals. We consider the linear Hankel matrix $H(\vecx)=H\_0+\X\_1H\_1+...+\X\_nH\_n$ and the problem of computing sample points in each connected component of the real algebraic set defined by the rank constraint ${\sf rank}(H(\vecx))\leq r$, for a given integer $r \leq m-1$. Computing sample points in real algebraic sets defined by rank defects in linear matrices is a general problem that finds applications in many areas such as control theory, computational geometry, optimization, etc. Moreover, Hankel matrices appear in many areas of engineering sciences. Also, since Hankel matrices are symmetric, any algorithmic development for this problem can be seen as a first step towards a dedicated exact algorithm for solving semi-definite programming problems, i.e. linear matrix inequalities. Under some genericity assumptions on the input (such as smoothness of an incidence variety), we design a probabilistic algorithm for tackling this problem. It is an adaptation of the so-called critical point method that takes advantage of the special structure of the problem. Its complexity reflects this: it is essentially quadratic in specific degree bounds on an incidence variety. We report on practical experiments and analyze how the algorithm takes advantage of this special structure. A first implementation outperforms existing implementations for computing sample points in general real algebraic sets: it tackles examples that are out of reach of the state-of-the-art.
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Venue: arXiv cs.LO 2015
Year: 2015

We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API to allow for incremental solving based on clause groups. A clause group is a set of clauses which is incrementally added to or removed from a previously solved QBF. Our implementation of the novel API is related to incremental SAT solving based on selector variables and assumptions. However, the API entirely hides selector variables and assumptions from the user, which facilitates the integration of DepQBF in other tools. We present implementation details and, for the first time, report on experiments related to the computation of MUCs of QBFs using DepQBF's novel clause group API.
Implicit Contextual Integrity in Online Social Networks
Venue: arXiv cs.SI 2015
Year: 2015

Many real incidents demonstrate that users of Online Social Networks need mechanisms that help them manage their interactions by increasing the awareness of the different contexts that coexist in Online Social Networks and preventing them from exchanging inappropriate information in those contexts or disseminating sensitive information from some contexts to others. Contextual integrity is a privacy theory that conceptualises the appropriateness of information sharing based on the contexts in which this information is to be shared. Computational models of Contextual Integrity assume the existence of well-defined contexts, in which individuals enact pre-defined roles and information sharing is governed by an explicit set of norms. However, contexts in Online Social Networks are known to be implicit, unknown a priori and ever changing; users relationships are constantly evolving; and the information sharing norms are implicit. This makes current Contextual Integrity models not suitable for Online Social Networks. In this paper, we propose the first computational model of Implicit Contextual Integrity, presenting an information model and an Information Assistant Agent that uses the information model to learn implicit contexts, relationships and the information sharing norms to help users avoid inappropriate information exchanges and undesired information disseminations. Through an experimental evaluation, we validate the properties of Information Assistant Agents, which are shown to: infer the information sharing norms even if a small proportion of the users follow the norms and in presence of malicious users; help reduce the exchange of inappropriate information and the dissemination of sensitive information with only a partial view of the system and the information received and sent by their users; and minimise the burden to the users in terms of raising unnecessary alerts.
Consensus using Asynchronous Failure Detectors
Venue: arXiv cs.DC 2015
Year: 2015

The FLP result shows that crash-tolerant consensus is impossible to solve in asynchronous systems, and several solutions have been proposed for crash-tolerant consensus under alternative (stronger) models. One popular approach is to augment the asynchronous system with appropriate failure detectors, which provide (potentially unreliable) information about process crashes in the system, to circumvent the FLP impossibility. In this paper, we demonstrate the exact mechanism by which (sufficiently powerful) asynchronous failure detectors enable solving crash-tolerant consensus. Our approach, which borrows arguments from the FLP impossibility proof and the famous result from CHT, which shows that $Ω$ is a weakest failure detector to solve consensus, also yields a natural proof to $Ω$ as a weakest asynchronous failure detector to solve consensus. The use of I/O automata theory in our approach enables us to model execution in a more detailed fashion than CHT and also addresses the latent assumptions and assertions in the original result in CHT.
Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness
Venue: arXiv cs.LO 2015
Year: 2015

This work proposes tractable bisimulations for the higher-order pi-calculus with session primitives (HOpi) and offers a complete study of the expressivity of its most significant subcalculi. First we develop three typed bisimulations, which are shown to coincide with contextual equivalence. These characterisations demonstrate that observing as inputs only a specific finite set of higher-order values (which inhabit session types) suffices to reason about HOp} processes. Next, we identify HO, a minimal, second-order subcalculus of HOpi in which higher-order applications/abstractions, name-passing, and recursion are absent. We show that HO can encode HOpi extended with higher-order applications and abstractions and that a first-order session pi-calculus can encode HOpi. Both encodings are fully abstract. We also prove that the session pi-calculus with passing of shared names cannot be encoded into HOpi without shared names. We show that HOpi, HO, and pi are equally expressive; the expressivity of HO enables effective reasoning about typed equivalences for higher-order processes.
Verifying the Safety of a Flight-Critical System
Venue: arXiv cs.SE 2015
Year: 2015

This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft control system named Transport Class Model (TCM), and involved several stages: formalizing and disambiguating requirements in collaboration with do- main experts; processing models for their use by formal verification tools; applying compositional techniques at the architectural and component level to scale verification. Performed in the context of a major NASA milestone, this study of formal verification in practice is one of the most challenging that our group has performed, and it took several person months to complete it. This paper describes the methodology that we followed and the lessons that we learned.
Scalable Multilabel Prediction via Randomized Methods
Venue: arXiv cs.LG 2015
Year: 2015

Modeling the dependence between outputs is a fundamental challenge in multilabel classification. In this work we show that a generic regularized nonlinearity mapping independent predictions to joint predictions is sufficient to achieve state-of-the-art performance on a variety of benchmark problems. Crucially, we compute the joint predictions without ever obtaining any independent predictions, while incorporating low-rank and smoothness regularization. We achieve this by leveraging randomized algorithms for matrix decomposition and kernel approximation. Furthermore, our techniques are applicable to the multiclass setting. We apply our method to a variety of multiclass and multilabel data sets, obtaining state-of-the-art results.
Multi-view Face Detection Using Deep Convolutional Neural Networks
Venue: arXiv cs.CV 2015
Year: 2015

In this paper we consider the problem of multi-view face detection. While there has been significant research on this problem, current state-of-the-art approaches for this task require annotation of facial landmarks, e.g. TSM [25], or annotation of face poses [28, 22]. They also require training dozens of models to fully capture faces in all orientations, e.g. 22 models in HeadHunter method [22]. In this paper we propose Deep Dense Face Detector (DDFD), a method that does not require pose/landmark annotation and is able to detect faces in a wide range of orientations using a single model based on deep convolutional neural networks. The proposed method has minimal complexity; unlike other recent deep learning object detection methods [9], it does not require additional components such as segmentation, bounding-box regression, or SVM classifiers. Furthermore, we analyzed scores of the proposed face detector for faces in different orientations and found that 1) the proposed method is able to detect faces from different angles and can handle occlusion to some extent, 2) there seems to be a correlation between dis- tribution of positive examples in the training set and scores of the proposed face detector. The latter suggests that the proposed methods performance can be further improved by using better sampling strategies and more sophisticated data augmentation techniques. Evaluations on popular face detection benchmark datasets show that our single-model face detector algorithm has similar or better performance compared to the previous methods, which are more complex and require annotations of either different poses or facial landmarks.
An SVD-based Fragile Watermarking Scheme With Grouped Blocks
Venue: arXiv cs.CR 2015
Year: 2015

This paper proposes a novel fragile watermarking scheme for digital image authentication which is based on Singular Value Decomposition(SVD) and grouped blocks. The watermark bits which include two types of bits are inserted into the least significant bit(LSB) plane of the host image using the adaptive chaotic map to determine the positions. The groped blocks break the block-wise independence and therefore can withstand the Vector Quantization attack(VQ attack). The inserting positions are related to the statistical information of image block data, in order to increase the security and provide an auxiliary way to authenticate the image data. The effectiveness of the proposed scheme is checked by a variety of attacks, and the experimental results prove that it has a remarkable tamper detection ability and also has a precise locating ability.
Lower bounds on the size of semi-quantum finite automata
Venue: arXiv cs.FL 2015
Year: 2015

In the literature, there exist several interesting hybrid models of finite automata which have both quantum and classical states. We call them semi-quantum automata. In this paper, we compare the descriptional power of these models with that of DFA. Specifically, we present a uniform method that gives a lower bound on the size of the three existing main models of semi-quantum automata, and this bound shows that semi-quantum automata can be at most exponentially more concise than DFA. Compared with a recent work (Bianchi, Mereghetti, Palano, Theoret. Comput. Sci., 551(2014), 102-115), our method shows the following two advantages: (i) our method is much more concise; and (ii) our method is universal, since it is applicable to the three existing main models of semi-quantum automata, instead of only a specific model.
Invariance of the spark, NSP order and RIP order under elementary transformations of matrices
Venue: arXiv cs.IT 2015
Year: 2015

The theory of compressed sensing tells us that recovering all k-sparse signals requires a sensing matrix to satisfy that its spark is greater than 2k, or its order of the null space property (NSP) or the restricted isometry property (RIP) is 2k or above. If we perform elementary row or column operations on the sensing matrix, what are the changes of its spark, NSP order and RIP order? In this paper, we study this problem and discover that these three quantitative indexes of sensing matrices all possess invariance under all matrix elementary transformations except column-addition ones. Putting this result in form of matrix products, we get the types of matrices which multiply a sensing matrix and make the products still have the same properties of sparse recovery as the sensing matrix. According to these types of matrices, we made an interesting discovery that sensing matrices with deterministic constructions do not possess the property universality which belongs to sensing matrices with random constructions.
Coded Retransmission in Wireless Networks Via Abstract MDPs: Theory and Algorithms
Venue: arXiv cs.IT 2015
Year: 2015

Consider a transmission scheme with a single transmitter and multiple receivers over a faulty broadcast channel. For each receiver, the transmitter has a unique infinite stream of packets, and its goal is to deliver them at the highest throughput possible. While such multiple-unicast models are unsolved in general, several network coding based schemes were suggested. In such schemes, the transmitter can either send an uncoded packet, or a coded packet which is a function of a few packets. The packets sent can be received by the designated receiver (with some probability) or heard and stored by other receivers. Two functional modes are considered; the first presumes that the storage time is unlimited, while in the second it is limited by a given Time to Expire (TTE) parameter. We model the transmission process as an infinite-horizon Markov Decision Process (MDP). Since the large state space renders exact solutions computationally impractical, we introduce policy restricted and induced MDPs with significantly reduced state space, and prove that with proper reward function they have equal optimal value function (hence equal optimal throughput). We then derive a reinforcement learning algorithm, which learns the optimal policy for the induced MDP. This optimal strategy of the induced MDP, once applied to the policy restricted one, significantly improves over uncoded schemes. Next, we enhance the algorithm by means of analysis of the structural properties of the resulting reward functional. We demonstrate that our method scales well in the number of users, and automatically adapts to the packet loss rates, unknown in advance. In addition, the performance is compared to the recent bound by Wang, which assumes much stronger coding (e.g., intra-session and buffering of coded packets), yet is shown to be comparable.
Topological Interference Management with just Retransmission: What are the "Best" Topologies?
Venue: arXiv cs.IT 2015
Year: 2015

We study the problem of interference management in fast fading wireless networks, in which the transmitters are only aware of network topology. We consider a class of retransmission-based schemes, where transmitters in the network are only allowed to resend their symbols in order to assist with the neutralization of interference at the receivers. We introduce a necessary and sufficient condition on the network topology, under which half symmetric degrees-of-freedom (DoF) is achievable through the considered retransmission-based schemes. This corresponds to the "best" topologies since half symmetric DoF is the highest possible value for the symmetric DoF in the presence of interference. We show that when the condition is satisfied, there always exists a set of carefully chosen transmitters in the network, such that by retransmission of their symbols at an appropriate time slot, we can neutralize all the interfering signals at the receivers. Quite surprisingly, we also show that for any given network topology, if we cannot achieve half symmetric DoF by retransmission-based schemes, then there does not exist any linear scheme that can do so. We also consider a practical network scenario that models cell edge users in a heterogeneous network, and show that the characterized condition on the network topology occurs frequently. Furthermore, we numerically evaluate the achievable rates of the DoF-optimal retransmission-based scheme in such network scenario, and show that its throughput gain is not restricted to the asymptotic DoF analysis.
A Fast Distributed Solver for Symmetric Diagonally Dominant Linear Equations
Venue: arXiv cs.DC 2015
Year: 2015

In this paper, we propose a fast distributed solver for linear equations given by symmetric diagonally dominant M-Matrices. Our approach is based on a distributed implementation of the parallel solver of Spielman and Peng by considering a specific approximated inverse chain which can be computed efficiently in a distributed fashion. Representing the system of equations by a graph $\mathbb{G}$, the proposed distributed algorithm is capable of attaining $ε$-close solutions (for arbitrary $ε$) in time proportional to $n^{3}$ (number of nodes in $\mathbb{G}$), $α$ (upper bound on the size of the R-Hop neighborhood), and $\frac{{W}_{max}}{{W}_{min}}$ (maximum and minimum weight of edges in $\mathbb{G}$).
The NUbots Team Description Paper 2015
Venue: arXiv cs.RO 2015
Year: 2015

The NUbots are an interdisciplinary RoboCup team from The University of Newcastle, Australia. The team has a history of strong contributions in the areas of machine learning and computer vision. The NUbots have participated in RoboCup leagues since 2002, placing first several times in the past. In 2014 the NUbots also partnered with the University of Newcastle Mechatronics Laboratory to participate in the RobotX Marine Robotics Challenge, which resulted in several new ideas and improvements to the NUbots vision system for RoboCup. This paper summarizes the history of the NUbots team, describes the roles and research of the team members, gives an overview of the NUbots' robots, their software system, and several associated research projects.
Timeability of Extensive-Form Games
Venue: arXiv cs.GT 2015
Year: 2015

Extensive-form games constitute the standard representation scheme for games with a temporal component. But do all extensive-form games correspond to protocols that we can implement in the real world? We often rule out games with imperfect recall, which prescribe that an agent forget something that she knew before. In this paper, we show that even some games with perfect recall can be problematic to implement. Specifically, we show that if the agents have a sense of time passing (say, access to a clock), then some extensive-form games can no longer be implemented; no matter how we attempt to time the game, some information will leak to the agents that they are not supposed to have. We say such a game is not exactly timeable. We provide easy-to-check necessary and sufficient conditions for a game to be exactly timeable. Most of the technical depth of the paper concerns how to approximately time games, which we show can always be done, though it may require large amounts of time. Specifically, we show that for some games the time required to approximately implement the game grows as a power tower of height proportional to the number of players and with a parameter that measures the precision of the approximation at the top of the power tower. In practice, that makes the games untimeable. Besides the conceptual contribution to game theory, we believe our methodology can have applications to preventing information leakage in security protocols.
Time Petri Net Models for a New Queuless and Uncentralized Resource Discovery System
Venue: arXiv cs.DC 2015
Year: 2015

In this report, we detail the model using Petri Nets of a new fully distributed resource reservation system. The basic idea of the considered distributed system is to let a user reserve a set of resources on a local network and to use them, without any specific, central administration component such as a front-end node. Resources can be, for instance, computing resources (cores, nodes, GPUs...) or some memory on a server. In order to verify some qualitative and quantitative properties provided by this system, we need to model it. We detail the algorithms used by this system and the Petri Net models we made of it.
On Distributed Density in Tuple-based Coordination Languages
Venue: arXiv cs.PL 2015
Year: 2015

Inspired by the chemical metaphor, this paper proposes an extension of Linda-like languages in the aim of modeling the coordination of complex distributed systems. The new language manipulates finite sets of tuples and distributes a density among them. This new concept adds to the non-determinism inherent in the selection of matched tuples a non-determinism to the tell, ask and get primitives on the consideration of different tuples. Furthermore, thanks to de Boer and Palamidessi's notion of modular embedding, we establish that this new language strictly increases the expressiveness of the Dense Bach language introduced earlier and, consequently, Linda-like languages.