OpenRaiser/Intern-Atlas huggingface dataset:
Approaching the Coverability Problem Continuously
Venue: arXiv cs.LO 2016
Year: 2016

The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. A cornerstone of our approach is the efficient encoding of a recently developed polynomial-time algorithm for reachability in continuous Petri nets into SMT. We demonstrate the effectiveness of our approach on standard benchmarks from the literature, which shows that our approach decides significantly more instances than any existing tool and is in addition often much faster, in particular on large instances.
Limit Your Consumption! Finding Bounds in Average-energy Games
Venue: arXiv cs.GT 2016
Year: 2016

Energy games are infinite two-player games played in weighted arenas with quantitative objectives that restrict the consumption of a resource modeled by the weights, e.g., a battery that is charged and drained. Typically, upper and/or lower bounds on the battery capacity are part of the problem description. Here, we consider the problem of determining upper bounds on the average accumulated energy or on the capacity while satisfying a given lower bound, i.e., we do not determine whether a given bound is sufficient to meet the specification, but if there exists a sufficient bound to meet it. In the classical setting with positive and negative weights, we show that the problem of determining the existence of a sufficient bound on the long-run average accumulated energy can be solved in doubly-exponential time. Then, we consider recharge games: here, all weights are negative, but there are recharge edges that recharge the energy to some fixed capacity. We show that bounding the long-run average energy in such games is complete for exponential time. Then, we consider the existential version of the problem, which turns out to be solvable in polynomial time: here, we ask whether there is a recharge capacity that allows the system player to win the game. We conclude by studying tradeoffs between the memory needed to implement strategies and the bounds they realize. We give an example showing that memory can be traded for bounds and vice versa. Also, we show that increasing the capacity allows to lower the average accumulated energy.
Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems
Venue: arXiv cs.SE 2016
Year: 2016

Feedback is an essential composition operator in many classes of reactive and other systems. This paper studies feedback in the context of compositional theories with refinement. Such theories allow to reason about systems on a component-by-component basis, and to characterize substitutability as a refinement relation. Although compositional theories of feedback do exist, they are limited either to deterministic systems (functions) or input-receptive systems (total relations). In this work we propose a compositional theory of feedback which applies to non-deterministic and non-input-receptive systems (e.g., partial relations). To achieve this, we use the semantic frameworks of predicate and property transformers, and relations with fail and unknown values. We show how to define instantaneous feedback for stateless systems and feedback with unit delay for stateful systems. Both operations preserve the refinement relation, and both can be applied to non-deterministic and non-input-receptive systems.
Subquadratic Algorithms for Succinct Stable Matching
Venue: arXiv cs.DS 2016
Year: 2016

We consider the stable matching problem when the preference lists are not given explicitly but are represented in a succinct way and ask whether the problem becomes computationally easier and investigate other implications. We give subquadratic algorithms for finding a stable matching in special cases of natural succinct representations of the problem, the $d$-attribute, $d$-list, geometric, and single-peaked models. We also present algorithms for verifying a stable matching in the same models. We further show that for $d = ω(\log n)$ both finding and verifying a stable matching in the $d$-attribute and $d$-dimensional geometric models requires quadratic time assuming the Strong Exponential Time Hypothesis. This suggests that these succinct models are not significantly simpler computationally than the general case for sufficiently large $d$.
On a conjecture of Mohar concerning Kempe equivalence of regular graphs
Venue: arXiv cs.DM 2016
Year: 2016

Let $G$ be a graph with a vertex colouring $α$. Let $a$ and $b$ be two colours. Then a connected component of the subgraph induced by those vertices coloured either $a$ or $b$ is known as a Kempe chain. A colouring of $G$ obtained from $α$ by swapping the colours on the vertices of a Kempe chain is said to have been obtained by a Kempe change. Two colourings of $G$ are Kempe equivalent if one can be obtained from the other by a sequence of Kempe changes. A conjecture of Mohar (2007) asserts that, for $k \geq 3$, all $k$-colourings of a $k$-regular graph that is not complete are Kempe equivalent. It was later shown that all $3$-colourings of a cubic graph that is neither $K_4$ nor the triangular prism are Kempe equivalent. In this paper, we prove that the conjecture holds for each $k\geq 4$. We also report the implications of this result on the validity of the Wang-Swendsen-Kotecký algorithm for the antiferromagnetic Potts model at zero-temperature.
Reversing Single Sessions
Venue: arXiv cs.LO 2016
Year: 2016

Session-based communication has gained a widespread acceptance in practice as a means for developing safe communicating systems via structured interactions. In this paper, we investigate how these structured interactions are affected by reversibility, which provides a computational model allowing executed interactions to be undone. In particular, we provide a systematic study of the integration of different notions of reversibility in both binary and multiparty single sessions. The considered forms of reversibility are: one for completely reversing a given session with one backward step, and another for also restoring any intermediate state of the session with either one backward step or multiple ones. We analyse the costs of reversing a session in all these different settings. Our results show that extending binary single sessions to multiparty ones does not affect the reversibility machinery and its costs.
Selfish Knapsack
Venue: arXiv cs.GT 2016
Year: 2016

We consider a selfish variant of the knapsack problem. In our version, the items are owned by agents, and each agent can misrepresent the set of items she owns---either by avoiding reporting some of them (understating), or by reporting additional ones that do not exist (overstating). Each agent's objective is to maximize, within the items chosen for inclusion in the knapsack, the total valuation of her own chosen items. The knapsack problem, in this context, seeks to minimize the worst-case approximation ratio for social welfare at equilibrium. We show that a randomized greedy mechanism has attractive strategic properties: in general, it has a correlated price of anarchy of $2$ (subject to a mild assumption). For overstating-only agents, it becomes strategyproof; we also provide a matching lower bound of $2$ on the (worst-case) approximation ratio attainable by randomized strategyproof mechanisms, and show that no deterministic strategyproof mechanism can provide any constant approximation ratio. We also deal with more specialized environments. For the case of $2$ understating-only agents, we provide a randomized strategyproof $\frac{5+4\sqrt{2}}{7} \approx 1.522$-approximate mechanism, and a lower bound of $\frac{5\sqrt{5}-9}{2} \approx 1.09$. When all agents but one are honest, we provide a deterministic strategyproof $\frac{1+\sqrt{5}}{2} \approx 1.618$-approximate mechanism with a matching lower bound. Finally, we consider a model where agents can misreport their items' properties rather than existence. Specifically, each agent owns a single item, whose value-to-size ratio is publicly known, but whose actual value and size are not. We show that an adaptation of the greedy mechanism is strategyproof and $2$-approximate, and provide a matching lower bound; we also show that no deterministic strategyproof mechanism can provide a constant approximation ratio.
A Bio-Synthetic Modulator Model for Diffusion-based Molecular Communications
Venue: arXiv cs.ET 2016
Year: 2016

In diffusion-based molecular communication (DMC), one important functionality of a transmitter nano-machine is signal modulation. In particular, the transmitter has to be able to control the release of signaling molecules for modulation of the information bits. An important class of control mechanisms in natural cells for releasing molecules is based on ion channels which are pore-forming proteins across the cell membrane whose opening and closing may be controlled by a gating parameter. In this paper, a modulator for DMC based on ion channels is proposed which controls the rate at which molecules are released from the transmitter by modulating a gating parameter signal. Exploiting the capabilities of the proposed modulator, an on-off keying modulation scheme is introduced and the corresponding average modulated signal, i.e., the average release rate of the molecules from the transmitter, is derived in the Laplace domain. By making a simplifying assumption, a closed-form expression for the average modulated signal in the time domain is obtained which constitutes an upper bound on the total number of released molecules regardless of this assumption. The derived average modulated signal is compared to results obtained with a particle based simulator. The numerical results show that the derived upper bound is tight if the number of ion channels distributed across the transmitter (cell) membrane is small.
Kron reduction methods for plug-and-play control of ac islanded microgrids with arbitrary topology
Venue: arXiv cs.SY 2016
Year: 2016

In this paper, we provide an extension of the scalable algorithm proposed in (Riverso et al., 2015) for the design of Plug-and-Play (PnP) controllers for AC Islanded microGrids (ImGs). The method in (Riverso et al., 2015) assumes DGUs are arranged in a load-connected topology, i.e. loads can appear only at the output terminals of inverters. For handling totally general interconnections of DGUs and loads, we describe an approach based on Kron Reduction (KR), a network reduction method giving an equivalent load-connected model of the original ImG. However, existing KR approaches can fail in preserving the structure of transfer functions representing transmission lines. To avoid this drawback, we introduce an approximate KR algorithm, still capable to represent exactly the asymptotic periodic behavior of electric signals even if they are unbalanced. Our results are backed up with simulations illustrating features of the new KR approach as well as its use for designing PnP controllers in a 21-bus ImG derived from an IEEE test feeder.
Ideal Composition of a Group for Maximal Knowledge Building in Crowdsourced Environments
Venue: arXiv cs.HC 2016
Year: 2016

Crowdsourcing has revolutionized the process of knowledge building on the web. Wikipedia and StackOverflow are witness to this uprising development. However, the dynamics behind the process of crowdsourcing in the domain of knowledge building is an area relatively unexplored. It has been observed that an ecosystem exists in the collaborative knowledge building environments (KBE), which puts users of a KBE into various categories based on their expertise. Classical cognitive theories indicate triggering among the knowledge units to be one of the most important reasons behind accelerated knowledge building in collaborative KBEs. We use the concept of ecosystem and the triggering phenomenon to highlight the necessity for the right mix of users in a KBE. We provide a hill climbing based algorithm which gives the ideal mixture of users in a KBE, given the amount of triggering that takes place among the users of various categories. The study will help the portal designers to accordingly build suitable crowdsourced environments.
Psychological Determinants and Consequences of Complex Networks
Venue: arXiv cs.SI 2016
Year: 2016

This paper presents two models that exemplify psychological factors as a determinant and as a consequence of social network characteristics. There is an endogeneity considered in network formation: while the social experiences have impacts on people, their current psychological states and traits affect network evolution. The first model is an agent-based model over Bianconi-Barabasi networks, used to explain the relation between network size, extroversion, and age of individuals. The second model deals with the emergence of urban tribes as a consequence of a smaller propensity to communicate with different with different traits and opinions.
Three-Way Channels with Multiple Unicast Sessions: Capacity Approximation via Network Transformation
Venue: arXiv cs.IT 2016
Year: 2016

A network of 3 nodes mutually communicating with each other is studied. This multi-way network is a suitable model for 3-user device-to-device communications. The main goal of this paper is to characterize the capacity region of the underlying Gaussian 3-way channel (3WC) within a constant gap. To this end, a capacity outer bound is derived using cut-set bounds and genie-aided bounds. For achievability, the 3WC is first transformed into an equivalent star-channel. This latter is then decomposed into a set of `successive' sub-channels, leading to a sub-channel allocation problem. Using backward decoding, interference neutralization, and known results on the capacity of the star-channel relying of physical-layer network coding, an achievable rate region for the 3WC is obtained. It is then shown that the achievable rate region is within a constant gap of the developed outer bound, leading to the desired capacity approximation. Interestingly, in contrast to the Gaussian two-way channel (TWC), adaptation is necessary in the 3WC. Furthermore, message splitting is another ingredient of the developed scheme for the 3WC which is not required in the TWC. The two setups are, however, similar in terms of their sum-capacity pre-log which is equal to 2. Finally, some interesting networks and their approximate capacities are recovered as special cases of the 3WC, such as the cooperative BC and MAC.
Deep Recurrent Regression for Facial Landmark Detection
Venue: arXiv cs.CV 2016
Year: 2016

We propose a novel end-to-end deep architecture for face landmark detection, based on a deep convolutional and deconvolutional network followed by carefully designed recurrent network structures. The pipeline of this architecture consists of three parts. Through the first part, we encode an input face image to resolution-preserved deconvolutional feature maps via a deep network with stacked convolutional and deconvolutional layers. Then, in the second part, we estimate the initial coordinates of the facial key points by an additional convolutional layer on top of these deconvolutional feature maps. In the last part, by using the deconvolutional feature maps and the initial facial key points as input, we refine the coordinates of the facial key points by a recurrent network that consists of multiple Long-Short Term Memory (LSTM) components. Extensive evaluations on several benchmark datasets show that the proposed deep architecture has superior performance against the state-of-the-art methods.
Analog Spatial Cancellation for Tackling the Near-Far Problem in Wirelessly Powered Communications (Extended Version)
Venue: arXiv cs.IT 2016
Year: 2016

The implementation of wireless power transfer in wireless communication systems opens up a new research area, known as wirelessly powered communications (WPC). In next-generation heterogeneous networks where ultra-dense small-cell base stations are deployed, simultaneous-wireless-information-and-power-transfer (SWIPT) is feasible over short ranges. One challenge for designing a WPC system is the severe near-far problem where a user attempts to decode an information-transfer (IT) signal in the presence of extremely strong SWIPT signals. Jointly quantizing the mixed signals causes the IT signal to be completely corrupted by quantization noise and thus the SWIPT signals have to be suppressed in the analog domain. This motivates the design of a framework in this paper for analog spatial cancellation in a multi-antenna WPC system. In the framework, an analog circuit consisting of simple phase shifters and adders, is adapted to cancel the SWIPT signals by multiplying it with a cancellation matrix having unit-modulus elements and full rank, where the full rank retains the spatial-multiplexing gain of the IT channel. The unit-modulus constraints render the conventional zero-forcing method unsuitable. Therefore, the paper presents a novel systematic approach for constructing cancellation matrices. For the single-SWIPT-interferer case, the matrices are obtained as truncated Fourier/Hadamard matrices after compensating for propagation phase shifts over the SWIPT channel. For the more challenging multiple-SWIPT-interferer case, it is proposed that each row of the cancellation matrix is constructed as a Kronecker-product of component vectors, with each component vectors designed to null the signal from a corresponding SWIPT interferer similarly as in the preceding case.
Narrow Gauge and Analytical Branching Strategies for Mixed Integer Programming
Venue: arXiv cs.DS 2016
Year: 2016

State-of-the-art branch and bound algorithms for mixed integer programming make use of special methods for making branching decisions. Strategies that have gained prominence include modern variants of so-called strong branching (Applegate, et al.,1995) and reliability branching (Achterberg, Koch and Martin, 2005; Hendel, 2015), which select variables for branching by solving associated linear programs and exploit pseudo-costs (Benichou et al., 1971). We suggest new branching criteria and propose alternative branching approaches called narrow gauge and analytical branching. The perspective underlying our approaches is to focus on prioritization of child nodes to examine fewer candidate variables at the current node of the B&B tree, balanced with procedures to extrapolate the implications of choosing these candidates by generating a small-depth look-ahead tree. Our procedures can also be used in rules to select among open tree nodes (those whose child nodes have not yet been generated). We incorporate pre- and post-winnowing procedures to progressively isolate preferred branching candidates, and employ derivative (created) variables whose branches are able to explore the solution space more deeply.
User Capacity of Wireless Physical-layer Identification: An Information-theoretic Perspective
Venue: arXiv cs.CR 2016
Year: 2016

Wireless Physical Layer Identification (WPLI) system aims at identifying or classifying authorized devices based on the unique Radio Frequency Fingerprints (RFFs) extracted from their radio frequency signals at the physical layer. Current works of WPLI focus on demonstrating system feasibility based on experimental error performance of WPLI with a fixed number of users. While an important question remains to be answered: what's the user number that WPLI can accommodate using different RFFs and receiving equipment. The user capacity of the WPLI can be a major concern for practical system designers and can also be a key metric to evaluate the classification performance of WPLI. In this work, we establish a theoretical understanding on user capacity of WPLI in an information-theoretic perspective. We apply information-theoretic modeling on RFF features of WPLI. An information-theoretic approach is consequently proposed based on mutual information between RFF and user identity to characterize the user capacity of WPLI. Based on this theoretical tool, the achievable user capacity of WPLI is characterized under practical constrains of off-the-shelf receiving devices. Field experiments on classification error performance are conducted for the validation of the information-theoretic user capacity characterization.
Why Is Dual-Pivot Quicksort Fast?
Venue: arXiv cs.DS 2016
Year: 2016

I discuss the new dual-pivot Quicksort that is nowadays used to sort arrays of primitive types in Java. I sketch theoretical analyses of this algorithm that offer a possible, and in my opinion plausible, explanation why (a) dual-pivot Quicksort is faster than the previously used (classic) Quicksort and (b) why this improvement was not already found much earlier.
Transforming Wikipedia into an Ontology-based Information Retrieval Search Engine for Local Experts using a Third-Party Taxonomy
Venue: arXiv cs.IR 2016
Year: 2016

Wikipedia is widely used for finding general information about a wide variety of topics. Its vocation is not to provide local information. For example, it provides plot, cast, and production information about a given movie, but not showing times in your local movie theatre. Here we describe how we can connect local information to Wikipedia, without altering its content. The case study we present involves finding local scientific experts. Using a third-party taxonomy, independent from Wikipedia's category hierarchy, we index information connected to our local experts, present in their activity reports, and we re-index Wikipedia content using the same taxonomy. The connections between Wikipedia pages and local expert reports are stored in a relational database, accessible through as public SPARQL endpoint. A Wikipedia gadget (or plugin) activated by the interested user, accesses the endpoint as each Wikipedia page is accessed. An additional tab on the Wikipedia page allows the user to open up a list of teams of local experts associated with the subject matter in the Wikipedia page. The technique, though presented here as a way to identify local experts, is generic, in that any third party taxonomy, can be used in this to connect Wikipedia to any non-Wikipedia data source.
Efficient Multiscale Gaussian Process Regression using Hierarchical Clustering
Venue: arXiv cs.LG 2016
Year: 2016

Standard Gaussian Process (GP) regression, a powerful machine learning tool, is computationally expensive when it is applied to large datasets, and potentially inaccurate when data points are sparsely distributed in a high-dimensional feature space. To address these challenges, a new multiscale, sparsified GP algorithm is formulated, with the goal of application to large scientific computing datasets. In this approach, the data is partitioned into clusters and the cluster centers are used to define a reduced training set, resulting in an improvement over standard GPs in terms of training and evaluation costs. Further, a hierarchical technique is used to adaptively map the local covariance representation to the underlying sparsity of the feature space, leading to improved prediction accuracy when the data distribution is highly non-uniform. A theoretical investigation of the computational complexity of the algorithm is presented. The efficacy of this method is then demonstrated on smooth and discontinuous analytical functions and on data from a direct numerical simulation of turbulent combustion.