OpenRaiser/Intern-Atlas huggingface dataset:
America Tweets China: A Fine-Grained Analysis of the State and Individual Characteristics Regarding Attitudes towards China
Venue: arXiv cs.SI 2015
Year: 2015

The U.S.-China relationship is arguably the most important bilateral relationship in the 21st century. Typically it is measured through opinion polls, for example, by Gallup and Pew Institute. In this paper, we propose a new method to measure U.S.-China relations using data from Twitter, one of the most popular social networks. Compared with traditional opinion polls, our method has two distinctive advantages. First, our sample size is significantly larger. National opinion polls have at most a few thousand samples. Our data set has 724,146 samples. The large size of our data set enables us to perform state level analysis, which so far even large opinion polls have left unexplored. Second, our method can control for fixed state and date effects. We first demonstrate the existence of inter-state and inter-day variances and then control for these variances in our regression analysis. Empirically, our study is able to replicate the stylized results from opinion polls as well as generate new insights. At the state level, we find New York, Michigan, Indiana and Arizona are the top four most China-friendly states. Wyoming, South Dakota, Kansas and Nevada are most homogeneous. At the individual level, we find attitudes towards China improve as an individual's Twitter experience grows longer and more intense. We also find individuals of Chinese ethnicity are statistically more China-friendly.
Simulator Semantics for System Level Formal Verification
Venue: arXiv cs.SE 2015
Year: 2015

Many simulation based Bounded Model Checking approaches to System Level Formal Verification (SLFV) have been devised. Typically such approaches exploit the capability of simulators to save computation time by saving and restoring the state of the system under simulation. However, even though such approaches aim to (bounded) formal verification, as a matter of fact, the simulator behaviour is not formally modelled and the proof of correctness of the proposed approaches basically relies on the intuitive notion of simulator behaviour. This gap makes it hard to check if the optimisations introduced to speed up the simulation do not actually omit checking relevant behaviours of the system under verification. The aim of this paper is to fill the above gap by presenting a formal semantics for simulators.
The expressive power of modal logic with inclusion atoms
Venue: arXiv cs.LO 2015
Year: 2015

Modal inclusion logic is the extension of basic modal logic with inclusion atoms, and its semantics is defined on Kripke models with teams. A team of a Kripke model is just a subset of its domain. In this paper we give a complete characterisation for the expressive power of modal inclusion logic: a class of Kripke models with teams is definable in modal inclusion logic if and only if it is closed under k-bisimulation for some integer k, it is closed under unions, and it has the empty team property. We also prove that the same expressive power can be obtained by adding a single unary nonemptiness operator to modal logic. Furthermore, we establish an exponential lower bound for the size of the translation from modal inclusion logic to modal logic with the nonemptiness operator.
Average-energy games
Venue: arXiv cs.LO 2015
Year: 2015

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP inter coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.
Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL
Venue: arXiv cs.LO 2015
Year: 2015

We continue the investigation of parameterized extensions of Linear Temporal Logic (LTL) that retain the attractive algorithmic properties of LTL: a polynomial space model checking algorithm and a doubly-exponential time algorithm for solving games. Alur et al. and Kupferman et al. showed that this is the case for Parametric LTL (PLTL) and PROMPT-LTL respectively, which have temporal operators equipped with variables that bound their scope in time. Later, this was also shown to be true for Parametric LDL (PLDL), which extends PLTL to be able to express all omega-regular properties. Here, we generalize PLTL to systems with costs, i.e., we do not bound the scope of operators in time, but bound the scope in terms of the cost accumulated during time. Again, we show that model checking and solving games for specifications in PLTL with costs is not harder than the corresponding problems for LTL. Finally, we discuss PLDL with costs and extensions to multiple cost functions.
Secure Transmission for Relay Wiretap Channels in the Presence of Spatially Random Eavesdroppers
Venue: arXiv cs.IT 2015
Year: 2015

We propose a secure transmission scheme for a relay wiretap channel, where a source communicates with a destination via a decode-and-forward relay in the presence of spatially random-distributed eavesdroppers. We assume that the source is equipped with multiple antennas, whereas the relay, the destination, and the eavesdroppers are equipped with a single antenna each. In the proposed scheme, in addition to information signals, the source transmits artificial noise signals in order to confuse the eavesdroppers. With the target of maximizing the secrecy throughput of the relay wiretap channel, we derive a closed-form expression for the transmission outage probability and an easy-to-compute expression for the secrecy outage probability. Using these expressions, we determine the optimal power allocation factor and wiretap code rates that guarantee the maximum secrecy throughput, while satisfying a secrecy outage probability constraint. Furthermore, we examine the impact of source antenna number on the secrecy throughput, showing that adding extra transmit antennas at the source brings about a significant increase in the secrecy throughput.
New Complexity Results and Algorithms for the Minimum Tollbooth Problem
Venue: arXiv cs.GT 2015
Year: 2015

The inefficiency of the Wardrop equilibrium of nonatomic routing games can be eliminated by placing tolls on the edges of a network so that the socially optimal flow is induced as an equilibrium flow. A solution where the minimum number of edges are tolled may be preferable over others due to its ease of implementation in real networks. In this paper we consider the minimum tollbooth (MINTB) problem, which seeks social optimum inducing tolls with minimum support. We prove for single commodity networks with linear latencies that the problem is NP-hard to approximate within a factor of $1.1377$ through a reduction from the minimum vertex cover problem. Insights from network design motivate us to formulate a new variation of the problem where, in addition to placing tolls, it is allowed to remove unused edges by the social optimum. We prove that this new problem remains NP-hard even for single commodity networks with linear latencies, using a reduction from the partition problem. On the positive side, we give the first exact polynomial solution to the MINTB problem in an important class of graphs---series-parallel graphs. Our algorithm solves MINTB by first tabulating the candidate solutions for subgraphs of the series-parallel network and then combining them optimally.
Mapping Generative Models onto a Network of Digital Spiking Neurons
Venue: arXiv cs.NE 2015
Year: 2015

Stochastic neural networks such as Restricted Boltzmann Machines (RBMs) have been successfully used in applications ranging from speech recognition to image classification. Inference and learning in these algorithms use a Markov Chain Monte Carlo procedure called Gibbs sampling, where a logistic function forms the kernel of this sampler. On the other side of the spectrum, neuromorphic systems have shown great promise for low-power and parallelized cognitive computing, but lack well-suited applications and automation procedures. In this work, we propose a systematic method for bridging the RBM algorithm and digital neuromorphic systems, with a generative pattern completion task as proof of concept. For this, we first propose a method of producing the Gibbs sampler using bio-inspired digital noisy integrate-and-fire neurons. Next, we describe the process of mapping generative RBMs trained offline onto the IBM TrueNorth neurosynaptic processor -- a low-power digital neuromorphic VLSI substrate. Mapping these algorithms onto neuromorphic hardware presents unique challenges in network connectivity and weight and bias quantization, which, in turn, require architectural and design strategies for the physical realization. Generative performance metrics are analyzed to validate the neuromorphic requirements and to best select the neuron parameters for the model. Lastly, we describe a design automation procedure which achieves optimal resource usage, accounting for the novel hardware adaptations. This work represents the first implementation of generative RBM inference on a neuromorphic VLSI substrate.
Opinion mining from twitter data using evolutionary multinomial mixture models
Venue: arXiv cs.IR 2015
Year: 2015

Image of an entity can be defined as a structured and dynamic representation which can be extracted from the opinions of a group of users or population. Automatic extraction of such an image has certain importance in political science and sociology related studies, e.g., when an extended inquiry from large-scale data is required. We study the images of two politically significant entities of France. These images are constructed by analyzing the opinions collected from a well known social media called Twitter. Our goal is to build a system which can be used to automatically extract the image of entities over time. In this paper, we propose a novel evolutionary clustering method based on the parametric link among Multinomial mixture models. First we propose the formulation of a generalized model that establishes parametric links among the Multinomial distributions. Afterward, we follow a model-based clustering approach to explore different parametric sub-models and select the best model. For the experiments, first we use synthetic temporal data. Next, we apply the method to analyze the annotated social media data. Results show that the proposed method is better than the state-of-the-art based on the common evaluation metrics. Additionally, our method can provide interpretation about the temporal evolution of the clusters.
Ordering stakeholder viewpoint concerns for holistic and incremental Enterprise Architecture: the W6H framework
Venue: arXiv cs.SE 2015
Year: 2015

Context: Enterprise Architecture (EA) is a discipline which has evolved to structure the business and its alignment with the IT systems. One of the popular enterprise architecture frameworks is Zachman framework (ZF). This framework focuses on describing the enterprise from six viewpoint perspectives of the stakeholders. These six perspectives are based on English language interrogatives 'what', 'where', 'who', 'when', 'why', and 'how' (thus the term W5H Journalists and police investigators use the W5H to describe an event. However, EA is not an event, creation and evolution of EA challenging. Moreover, the ordering of viewpoints is not defined in the existing EA frameworks, making data capturing process difficult. Our goals are to 1) assess if W5H is sufficient to describe modern EA and 2) explore the ordering and precedence among the viewpoint concerns. Method: we achieve our goals by bringing tools from the Linguistics, focusing on a full set of English Language interrogatives to describe viewpoint concerns and the inter-relationships and dependencies among these. Application of these tools is validated using pedagogical EA examples. Results: 1) We show that addition of the seventh interrogative 'which' to the W5H set (we denote this extended set as W6H) yields extra and necessary information enabling creation of holistic EA. 2) We discover that particular ordering of the interrogatives, established by linguists (based on semantic and lexical analysis of English language interrogatives), define starting points and the order in which viewpoints should be arranged for creating complete EA. 3) We prove that adopting W6H enables creation of EA for iterative and agile SDLCs, e.g. Scrum. Conclusions: We believe that our findings complete creation of EA using ZF by practitioners, and provide theoreticians with tools needed to improve other EA frameworks, e.g., TOGAF and DoDAF.
Parameterized Algorithms for Min-Max Multiway Cut and List Digraph Homomorphism
Venue: arXiv cs.DS 2015
Year: 2015

In this paper we design {\sf FPT}-algorithms for two parameterized problems. The first is \textsc{List Digraph Homomorphism}: given two digraphs $G$ and $H$ and a list of allowed vertices of $H$ for every vertex of $G$, the question is whether there exists a homomorphism from $G$ to $H$ respecting the list constraints. The second problem is a variant of \textsc{Multiway Cut}, namely \textsc{Min-Max Multiway Cut}: given a graph $G$, a non-negative integer $\ell$, and a set $T$ of $r$ terminals, the question is whether we can partition the vertices of $G$ into $r$ parts such that (a) each part contains one terminal and (b) there are at most $\ell$ edges with only one endpoint in this part. We parameterize \textsc{List Digraph Homomorphism} by the number $w$ of edges of $G$ that are mapped to non-loop edges of $H$ and we give a time $2^{O(\ell\cdot\log h+\ell^2\cdot \log \ell)}\cdot n^{4}\cdot \log n$ algorithm, where $h$ is the order of the host graph $H$. We also prove that \textsc{Min-Max Multiway Cut} can be solved in time $2^{O((\ell r)^2\log \ell r)}\cdot n^{4}\cdot \log n$. Our approach introduces a general problem, called {\sc List Allocation}, whose expressive power permits the design of parameterized reductions of both aforementioned problems to it. Then our results are based on an {\sf FPT}-algorithm for the {\sc List Allocation} problem that is designed using a suitable adaptation of the {\em randomized contractions} technique (introduced by [Chitnis, Cygan, Hajiaghayi, Pilipczuk, and Pilipczuk, FOCS 2012]).
Formal Support for Standardizing Protocols with State
Venue: arXiv cs.CR 2015
Year: 2015

Many cryptographic protocols are designed to achieve their goals using only messages passed over an open network. Numerous tools, based on well-understood foundations, exist for the design and analysis of protocols that rely purely on message passing. However, these tools encounter difficulties when faced with protocols that rely on non-local, mutable state to coordinate several local sessions. We adapt one of these tools, {\cpsa}, to provide automated support for reasoning about state. We use Ryan's Envelope Protocol as an example to demonstrate how the message-passing reasoning can be integrated with state reasoning to yield interesting and powerful results. Keywords: protocol analysis tools, stateful protocols, TPM, PKCS#11.
Constructing Abstraction Hierarchies Using a Skill-Symbol Loop
Venue: arXiv cs.AI 2015
Year: 2015

We describe a framework for building abstraction hierarchies whereby an agent alternates skill- and representation-acquisition phases to construct a sequence of increasingly abstract Markov decision processes. Our formulation builds on recent results showing that the appropriate abstract representation of a problem is specified by the agent's skills. We describe how such a hierarchy can be used for fast planning, and illustrate the construction of an appropriate hierarchy for the Taxi domain.
Interactive Museum Exhibits with Microcontrollers: A Use-Case Scenario
Venue: arXiv cs.CY 2015
Year: 2015

The feasibility of using microcontrollers in real life applications is becoming more widespread. These applications have grown from do-it-yourself (DIY) projects of computer enthusiasts or robotics projects to larger scale efforts and deployments. This project developed and deployed a prototype application that allows the public to interact with features of a model and view videos from a first-person perspective on the train. Through testing the microcontrollers and their usage in a public setting, it was demonstrated that interactive features could be implemented in model train exhibits, which are featured in traditional museum environments that lack technical infrastructure. Specifically, the Arduino and Raspberry Pi provide the necessary linkages between the Internet and hardware, allowing for a greater interactive experience for museum visitors. These results provide an important use-case scenario that cultural heritage institutions can utilize when implementing microcontrollers on a larger scale, for the purpose of increasing visitors experience through greater interaction and engagement.
Connectivity Preserving Iterative Compaction and Finding 2 Disjoint Rooted Paths in Linear Time
Venue: arXiv cs.DS 2015
Year: 2015

In this paper we show how to combine two algorithmic techniques to obtain linear time algorithms for various optimization problems on graphs, and present a subroutine which will be useful in doing so. The first technique is iterative shrinking. In the first phase of an iterative shrinking algorithm, we construct a sequence of graphs of decreasing size $G_1,\ldots,G_\ell$ where $G_1$ is the initial input, $G_\ell$ is a graph on which the problem is easy, and $G_i$ is obtained from $G_{i+1}$ via some shrinking algorithm. In the second phase we work through the sequence in reverse, repeatedly constructing a solution for a graph from the solution for its successor. In an iterative compaction algorithm, we insist that the graphs decrease by a constant fraction of the entire graph. Another approach to solving optimization problems is to exploit the structural properties implied by the connectivity of the input graph. This approach can be used on graphs which are not highly connected by decomposing an input graph into its highly connected pieces, solving subproblems on these specially structured pieces and then combining their solutions. We combine these two techniques by developing compaction algorithms which when applied to the highly connected pieces preserve their connectivity properties. The structural properties this connectivity implies can be helpful both in finding further compactions in later iterations and when we are manipulating solutions in the second phase of an iterative compaction algorithm. To illustrate how this compaction algorithm can be used as a subroutine, we present a linear time algorithm that given four vertices $\{s_1,s_2,t_1,t_2\}$ of a graph $G$, either finds a pair of disjoint paths $P_1$ and $P_2$ of $G$ such that $P_i$ has endpoints $s_i$ and $t_i$, or returns a planar embedding of an auxiliary graph which shows that no such pair exists.
Practical Algorithms for Linear Boolean-width
Venue: arXiv cs.CC 2015
Year: 2015

In this paper, we give a number of new exact algorithms and heuristics to compute linear boolean decompositions, and experimentally evaluate these algorithms. The experimental evaluation shows that significant improvements can be made with respect to running time without increasing the width of the generated decompositions. We also evaluated dynamic programming algorithms on linear boolean decompositions for several vertex subset problems. This evaluation shows that such algorithms are often much faster (up to several orders of magnitude) compared to theoretical worst case bounds.
On exact counting and quasi-quantum complexity
Venue: arXiv cs.CC 2015
Year: 2015

We present characterisations of "exact" gap-definable classes, in terms of indeterministic models of computation which slightly modify the standard model of quantum computation. This follows on work of Aaronson [arXiv:quant-ph/0412187], who shows that the counting class PP can be characterised in terms of bounded-error "quantum" algorithms which use invertible (and possibly non-unitary) transformations, or postselections on events of non-zero probability. Our work considers similar modifications of the quantum computational model, but in the setting of exact algorithms, and algorithms with zero error and constant success probability. We show that the gap-definable counting classes [J. Comput. Syst. Sci. 48 (1994), p.116] which bound exact and zero-error quantum algorithms can be characterised in terms of "quantum-like" algorithms involving nonunitary gates, and that postselection and nonunitarity have equivalent power for exact quantum computation only if these classes collapse.
A note on the dynamic dominant resource fairness mechanism
Venue: arXiv cs.GT 2015
Year: 2015

Multi-resource fair allocation has beena hot topic of resource allocation. Most recently, a dynamic dominant resource fairness (DRF) mechanism is proposed for dynamic multi-resource fair allocation. In this paper, we prove that the competitive ratio of the dynamic DRF mechanism is the reciprocal of the number of resource types, for two different objectives. Moreover, we develop a linear-time algorithm to find a dynamic DRF solution at each step.
A Revisit of Infinite Population Models for Evolutionary Algorithms on Continuous Optimization Problems
Venue: arXiv cs.NE 2015
Year: 2015

Infinite population models are important tools for studying population dynamics of evolutionary algorithms. They describe how the distributions of populations change between consecutive generations. In general, infinite population models are derived from Markov chains by exploiting symmetries between individuals in the population and analyzing the limit as the population size goes to infinity. In this paper, we study the theoretical foundations of infinite population models of evolutionary algorithms on continuous optimization problems. First, we show that the convergence proofs in a widely cited study were in fact problematic and incomplete. We further show that the modeling assumption of exchangeability of individuals cannot yield the transition equation. Then, in order to analyze infinite population models, we build an analytical framework based on convergence in distribution of random elements which take values in the metric space of infinite sequences. The framework is concise and mathematically rigorous. It also provides an infrastructure for studying the convergence of the stacking of operators and of iterating the algorithm which previous studies failed to address. Finally, we use the framework to prove the convergence of infinite population models for the mutation operator and the $k$-ary recombination operator. We show that these operators can provide accurate predictions for real population dynamics as the population size goes to infinity, provided that the initial population is identically and independently distributed.