OpenRaiser/Intern-Atlas huggingface dataset:
Stability of SIS Spreading Processes in Networks with Non-Markovian Transmission and Recovery
Venue: arXiv cs.SI 2019
Year: 2019

Although viral spreading processes taking place in networks are often analyzed using Markovian models in which both the transmission and the recovery times follow exponential distributions, empirical studies show that, in many real scenarios, the distribution of these times are not necessarily exponential. To overcome this limitation, we first introduce a generalized susceptible-infected-susceptible (SIS) spreading model that allows transmission and recovery times to follow phase-type distributions. In this context, we derive a lower bound on the exponential decay rate towards the infection-free equilibrium of the spreading model without relying on mean-field approximations. Based on our results, we illustrate how the particular shape of the transmission/recovery distribution influences the exponential rate of convergence towards the equilibrium.
Compositionality, Decompositionality and Refinement in Input/Output Conformance Testing - Technical Report
Venue: arXiv cs.LO 2019
Year: 2019

We propose an input/output conformance testing theory utilizing Modal Interface Automata with Input Refusals (IR-MIA) as novel behavioral formalism for both the specification and the implementation under test. A modal refinement relation on IR-MIA allows distinguishing between obligatory and allowed output behaviors, as well as between implicitly underspecified and explicitly forbidden input behaviors. The theory therefore supports positive and negative conformance testing with optimistic and pessimistic environmental assumptions. We further show that the resulting conformance relation on IR-MIA, called modal-irioco, enjoys many desirable properties concerning component-based behaviors. First, modal-irioco is preserved under modal refinement and constitutes a preorder under certain restrictions which can be ensured by a canonical input completion for IR-MIA. Second, under the same restrictions, modal-irioco is compositional with respect to parallel composition of IR-MIA with multi-cast and hiding. Finally, the quotient operator on IR-MIA, as the inverse to parallel composition, facilitates decompositionality in conformance testing to solve the unknown-component problem.
Priority, Cut, If-Then-Else and Exception Handling in Logic Programming
Venue: arXiv cs.LO 2019
Year: 2019

One of the long-standing problems on logic programming is to express {\it priority}-related operations -- default reasoning, if-then-else, cut, exception handling, etc -- in a high-level way. We argue that this problem can be solved by adopting computability logic and prioritized sequential-disjunctive goal formulas of the form $G_0 \bigtriangledown^* G_1$ where $G_0, G_1$ are goals. These goals have the following intended semantics: sequentially $choose$ the first true goal $G_i$ and execute $G_i$ where $i (= 0\ {\rm or}\ 1)$. These goals thus allow us to specify a task $G_0$ with the failure-handling (exception handling) routine $G_1$. This new goal can also be seen as a logic-equivalent of the $if$-$then$-$else$ statement in imperative language. We also discuss sequential-conjunction clauses which are {\it dual} of sequential-disjunctive goals.
Beginner's Luck: A Language for Property-Based Generators
Venue: arXiv cs.PL 2019
Year: 2019

Property-based random testing a la QuickCheck requires building efficient generators for well-distributed random data satisfying complex logical predicates, but writing these generators can be difficult and error prone. We propose a domain-specific language in which generators are conveniently expressed by decorating predicates with lightweight annotations to control both the distribution of generated values and the amount of constraint solving that happens before each variable is instantiated. This language, called Luck, makes generators easier to write, read, and maintain. We give Luck a formal semantics and prove several fundamental properties, including the soundness and completeness of random generation with respect to a standard predicate semantics. We evaluate Luck on common examples from the property-based testing literature and on two significant case studies, showing that it can be used in complex domains with comparable bug-finding effectiveness and a significant reduction in testing code size compared to handwritten generators.
Deciding whether there are infinitely many prime graphs with forbidden induced subgraphs
Venue: arXiv cs.DM 2019
Year: 2019

A homogeneous set of a graph $G$ is a set $X$ of vertices such that $2\le \lvert X\rvert <\lvert V(G)\rvert$ and no vertex in $V(G)-X$ has both a neighbor and a non-neighbor in $X$. A graph is prime if it has no homogeneous set. We present an algorithm to decide whether a class of graphs given by a finite set of forbidden induced subgraphs contains infinitely many non-isomorphic prime graphs.
Dijkstra Monads for Free
Venue: arXiv cs.PL 2019
Year: 2019

Dijkstra monads enable a dependent type theory to be enhanced with support for specifying and verifying effectful code via weakest preconditions. Together with their closely related counterparts, Hoare monads, they provide the basis on which verification tools like F*, Hoare Type Theory (HTT), and Ynot are built. We show that Dijkstra monads can be derived "for free" by applying a continuation-passing style (CPS) translation to the standard monadic definitions of the underlying computational effects. Automatically deriving Dijkstra monads in this way provides a correct-by-construction and efficient way of reasoning about user-defined effects in dependent type theories. We demonstrate these ideas in EMF*, a new dependently typed calculus, validating it via both formal proof and a prototype implementation within F*. Besides equipping F* with a more uniform and extensible effect system, EMF* enables a novel mixture of intrinsic and extrinsic proofs within F*.
A Corroborative Approach to Verification and Validation of Human--Robot Teams
Venue: arXiv cs.RO 2019
Year: 2019

We present an approach for the verification and validation (V&V) of robot assistants in the context of human-robot interactions (HRI), to demonstrate their trustworthiness through corroborative evidence of their safety and functional correctness. Key challenges include the complex and unpredictable nature of the real world in which assistant and service robots operate, the limitations on available V&V techniques when used individually, and the consequent lack of confidence in the V&V results. Our approach, called corroborative V&V, addresses these challenges by combining several different V&V techniques; in this paper we use formal verification (model checking), simulation-based testing, and user validation in experiments with a real robot. We demonstrate our corroborative V&V approach through a handover task, the most critical part of a complex cooperative manufacturing scenario, for which we propose some safety and liveness requirements to verify and validate. We construct formal models, simulations and an experimental test rig for the HRI. To capture requirements we use temporal logic properties, assertion checkers and textual descriptions. This combination of approaches allows V&V of the HRI task at different levels of modelling detail and thoroughness of exploration, thus overcoming the individual limitations of each technique. Should the resulting V&V evidence present discrepancies, an iterative process between the different V&V techniques takes place until corroboration between the V&V techniques is gained from refining and improving the assets (i.e., system and requirement models) to represent the HRI task in a more truthful manner. Therefore, corroborative V&V affords a systematic approach to 'meta-V&V,' in which different V&V techniques can be used to corroborate and check one another, increasing the level of certainty in the results of V&V.
The logical strength of Büchi's decidability theorem
Venue: arXiv cs.LO 2019
Year: 2019

We study the strength of axioms needed to prove various results related to automata on infinite words and Büchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak second-order arithmetic theory $RCA_0$: (1) the induction scheme for $Σ^0_2$ formulae of arithmetic, (2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings, (3) Büchi's complementation theorem for nondeterministic automata on infinite words, (4) the decidability of the depth-$n$ fragment of the MSO theory of $(N, {\le})$, for each $n \ge 5$. Moreover, each of (1)-(4) implies McNaughton's determinisation theorem for automata on infinite words, as well as the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem.
No Time to Observe: Adaptive Influence Maximization with Partial Feedback
Venue: arXiv cs.SI 2019
Year: 2019

Although influence maximization problem has been extensively studied over the past ten years, majority of existing work adopt one of the following models: \emph{full-feedback model} or \emph{zero-feedback model}. In the zero-feedback model, we have to commit the seed users all at once in advance, this strategy is also known as non-adaptive policy. In the full-feedback model, we select one seed at a time and wait until the diffusion completes, before selecting the next seed. Full-feedback model has better performance but potentially huge delay, zero-feedback model has zero delay but poorer performance since it does not utilize the observation that may be made during the seeding process. To fill the gap between these two models, we propose \emph{Partial-feedback Model}, which allows us to select a seed at any intermediate stage. We develop two novel greedy policies that, for the first time, achieve bounded approximation ratios under both uniform and non-uniform cost settings.
Efficient computation of longest single-arm-gapped palindromes in a string
Venue: arXiv cs.DS 2019
Year: 2019

In this paper, we introduce new types of approximate palindromes called single-arm-gapped palindromes (shortly SAGPs). A SAGP contains a gap in either its left or right arm, which is in the form of either $wguc u^R w^R$ or $wuc u^Rgw^R$, where $w$ and $u$ are non-empty strings, $w^R$ and $u^R$ are respectively the reversed strings of $w$ and $u$, $g$ is a string called a gap, and $c$ is either a single character or the empty string. Here we call $wu$ and $u^R w^R$ the arm of the SAGP, and $|uv|$ the length of the arm. We classify SAGPs into two groups: those which have $ucu^R$ as a maximal palindrome (type-1), and the others (type-2). We propose several algorithms to compute type-1 SAGPs with longest arms occurring in a given string, based on suffix arrays. Then, we propose a linear-time algorithm to compute all type-1 SAGPs with longest arms, based on suffix trees. Also, we show how to compute type-2 SAGPs with longest arms in linear time. We also perform some preliminary experiments to show practical performances of the proposed methods.
Envy-Free Division of Land
Venue: arXiv cs.GT 2019
Year: 2019

Classic cake-cutting algorithms enable people with different preferences to divide among them a heterogeneous resource (``cake''), such that the resulting division is fair according to each agent's individual preferences. However, these algorithms either ignore the geometry of the resource altogether, or assume it is one-dimensional. In practice, it is often required to divide multi-dimensional resources, such as land-estates or advertisement spaces in print or electronic media. In such cases, the geometric shape of the allotted piece is of crucial importance. For example, when building houses or designing advertisements, in order to be useful, the allotments should be squares or rectangles with bounded aspect-ratio. We thus introduce the problem of fair land division --- fair division of a multi-dimensional resource wherein the allocated piece must have a pre-specified geometric shape. We present constructive division algorithms that satisfy the two most prominent fairness criteria, namely envy-freeness and proportionality. In settings where proportionality cannot be achieved due to the geometric constraints, our algorithms provide a partially-proportional division, guaranteeing that the fraction allocated to each agent be at least a certain positive constant. We prove that in many natural settings the envy-freeness requirement is compatible with the best attainable partial-proportionality.
Approximation Algorithms for Multi-Multiway Cut and Multicut Problems on Directed Graphs
Venue: arXiv cs.DS 2019
Year: 2019

In this paper, we present two approximation algorithms for the directed multi-multiway cut and directed multicut problems. The so called region growing paradigm \cite{1} is modified and used for these two cut problems on directed graphs. By using this paradigm, we give for each problem an approximation algorithm such that both algorithms have the approximate factor $O(k)$ the same as the previous works done on these problems. However, the previous works need to solve $k$ linear programming, whereas our algorithms require only one linear programming. Therefore, our algorithms improve the running time of the previous algorithms.
Clinical and Educational Applications of LIVEIA: An Immersive Visualization Environment
Venue: arXiv cs.CY 2019
Year: 2019

The association between light and psychological states has a long history and permeates our language. LIVEIA (Light-based Immersive Visualization Environment for Imaginative Actualization) is a new immersive, interactive technology that uses physical light as a metaphor for visualizing peoples' inner lives and relationships. This paper outlines its educational value, as a tool for understanding and explaining aspects of how people think and interact, and its potential therapeutic value as a form of art therapy in which the artwork has straightforwardly interpretable symbolic meanings.
Operational Calculus for Differentiable Programming
Venue: arXiv cs.FL 2019
Year: 2019

In this work we present a theoretical model for differentiable programming. We construct an algebraic language that encapsulates formal semantics of differentiable programs by way of Operational Calculus. The algebraic nature of Operational Calculus can alter the properties of the programs that are expressed within the language and transform them into their solutions. In our model programs are elements of programming spaces and viewed as maps from the virtual memory space to itself. Virtual memory space is an algebra of programs, an algebraic data structure one can calculate with. We define the operator of differentiation ($\partial$) on programming spaces and, using its powers, implement the general shift operator and the operator of program composition. We provide the formula for the expansion of a differentiable program into an infinite tensor series in terms of the powers of $\partial$. We express the operator of program composition in terms of the generalized shift operator and $\partial$, which implements a differentiable composition in the language. Such operators serve as abstractions over the tensor series algebra, as main actors in our language. We demonstrate our models usefulness in differentiable programming by using it to analyse iterators, deriving fractional iterations and their iterating velocities, and explicitly solve the special case of ReduceSum.
On-line algorithms for multiplication and division in real and complex numeration systems
Venue: arXiv cs.DS 2019
Year: 2019

A positional numeration system is given by a base and by a set of digits. The base is a real or complex number $β$ such that $|β|>1$, and the digit set $A$ is a finite set of digits including $0$. Thus a number can be seen as a finite or infinite string of digits. An on-line algorithm processes the input piece-by-piece in a serial fashion. On-line arithmetic, introduced by Trivedi and Ercegovac, is a mode of computation where operands and results flow through arithmetic units in a digit serial manner, starting with the most significant digit. In this paper, we first formulate a generalized version of the on-line algorithms for multiplication and division of Trivedi and Ercegovac for the cases that $β$ is any real or complex number, and digits are real or complex. We then define the so-called OL Property, and show that if $(β, A)$ has the OL Property, then on-line multiplication and division are feasible by the Trivedi-Ercegovac algorithms. For a real base $β$ and a digit set $A$ of contiguous integers, the system $(β, A)$ has the OL Property if $\# A > |β|$. For a complex base $β$ and symmetric digit set $A$ of contiguous integers, the system $(β, A)$ has the OL Property if $\# A > β\overlineβ + |β+ \overlineβ|$. Provided that addition and subtraction are realizable in parallel in the system $(β, A)$ and that preprocessing of the denominator is possible, our on-line algorithms for multiplication and division have linear time complexity. Three examples are presented in detail: base $β=\frac{3+\sqrt{5}}{2}$ with digits $A=\{-1,0,1\}$; base $β=2i$ with digits $A = \{-2,-1, 0,1,2\}$; and base $β= -\frac{3}{2} + i \frac{\sqrt{3}}{2} = -1 + ω$, where $ω= \exp{\frac{2iπ}{3}}$, with digits $A = \{0, \pm 1, \pm ω, \pm ω^2 \}$.
Bit Allocation for Increased Power Efficiency in 5G Receivers with Variable-Resolution ADCs
Venue: arXiv cs.IT 2019
Year: 2019

In future high-capacity wireless systems based on mmWave or massive multiple input multiple output (MIMO), the power consumption of receiver Analog to Digital Converters (ADC) is a concern. Although hybrid or analog systems with fewer ADCs have been proposed, fully digital receivers with many lower resolution ADCs (and lower power) may be a more versatile solution. In this paper, focusing on an uplink scenario, we propose to take the optimization of ADC resolution one step further by enabling variable resolutions in the ADCs that sample the signal received at each antenna. This allows to give more bits to the antennas that capture the strongest incoming signal and fewer bits to the antennas that capture little signal energy and mostly noise. Simulation results show that, depending on the unquantized link SNR, a power saving in the order of 20-80% can be obtained by our variable resolution proposal in comparison with a reference fully digital receiver with a fixed low number of bits in all its ADCs.
Rethinking Sketching as Sampling: A Graph Signal Processing Approach
Venue: arXiv cs.IT 2019
Year: 2019

Sampling of signals belonging to a low-dimensional subspace has well-documented merits for dimensionality reduction, limited memory storage, and online processing of streaming network data. When the subspace is known, these signals can be modeled as bandlimited graph signals. Most existing sampling methods are designed to minimize the error incurred when reconstructing the original signal from its samples. Oftentimes these parsimonious signals serve as inputs to computationally-intensive linear operators. Hence, interest shifts from reconstructing the signal itself towards approximating the output of the prescribed linear operator efficiently. In this context, we propose a novel sampling scheme that leverages graph signal processing, exploiting the low-dimensional (bandlimited) structure of the input as well as the transformation whose output we wish to approximate. We formulate problems to jointly optimize sample selection and a sketch of the target linear transformation, so when the latter is applied to the sampled input signal the result is close to the desired output. Similar sketching as sampling ideas are also shown effective in the context of linear inverse problems. Because these designs are carried out off line, the resulting sampling plus reduced-complexity processing pipeline is particularly useful for data that are acquired or processed in a sequential fashion, where the linear operator has to be applied fast and repeatedly to successive inputs or response signals. Numerical tests showing the effectiveness of the proposed algorithms include classification of handwritten digits from as few as 20 out of 784 pixels in the input images and selection of sensors from a network deployed to carry out a distributed parameter estimation task.
Learning a Deep Embedding Model for Zero-Shot Learning
Venue: arXiv cs.CV 2019
Year: 2019

Zero-shot learning (ZSL) models rely on learning a joint embedding space where both textual/semantic description of object classes and visual representation of object images can be projected to for nearest neighbour search. Despite the success of deep neural networks that learn an end-to-end model between text and images in other vision problems such as image captioning, very few deep ZSL model exists and they show little advantage over ZSL models that utilise deep feature representations but do not learn an end-to-end embedding. In this paper we argue that the key to make deep ZSL models succeed is to choose the right embedding space. Instead of embedding into a semantic space or an intermediate space, we propose to use the visual space as the embedding space. This is because that in this space, the subsequent nearest neighbour search would suffer much less from the hubness problem and thus become more effective. This model design also provides a natural mechanism for multiple semantic modalities (e.g., attributes and sentence descriptions) to be fused and optimised jointly in an end-to-end manner. Extensive experiments on four benchmarks show that our model significantly outperforms the existing models. Code is available at https://github.com/lzrobots/DeepEmbeddingModel_ZSL
A Faster Algorithm for Cuckoo Insertion and Bipartite Matching in Large Graphs
Venue: arXiv cs.DS 2019
Year: 2019

Hash tables are ubiquitous in computer science for efficient access to large datasets. However, there is always a need for approaches that offer compact memory utilisation without substantial degradation of lookup performance. Cuckoo hashing is an efficient technique of creating hash tables with high space utilisation and offer a guaranteed constant access time. We are given $n$ locations and $m$ items. Each item has to be placed in one of the $k\ge2$ locations chosen by $k$ random hash functions. By allowing more than one choice for a single item, cuckoo hashing resembles multiple choice allocations schemes. In addition it supports dynamically changing the location of an item among its possible locations. We propose and analyse an insertion algorithm for cuckoo hashing that runs in \emph{linear time} with high probability and in expectation. Previous work on total allocation time has analysed breadth first search, and it was shown to be linear only in \emph{expectation}. Our algorithm finds an assignment (with probability 1) whenever it exists. In contrast, the other known insertion method, known as \emph{random walk insertion}, may run indefinitely even for a solvable instance. We also present experimental results comparing the performance of our algorithm with the random walk method, also for the case when each location can hold more than one item. As a corollary we obtain a linear time algorithm (with high probability and in expectation) for finding perfect matchings in a special class of sparse random bipartite graphs. We support this by performing experiments on a real world large dataset for finding maximum matchings in general large bipartite graphs. We report an order of magnitude improvement in the running time as compared to the \emph{Hopkraft-Karp} matching algorithm.
Deep Variational Information Bottleneck
Venue: arXiv cs.LG 2019
Year: 2019

We present a variational approximation to the information bottleneck of Tishby et al. (1999). This variational approach allows us to parameterize the information bottleneck model using a neural network and leverage the reparameterization trick for efficient training. We call this method "Deep Variational Information Bottleneck", or Deep VIB. We show that models trained with the VIB objective outperform those that are trained with other forms of regularization, in terms of generalization performance and robustness to adversarial attack.