OpenRaiser/Intern-Atlas huggingface dataset:
A Software Parallel Programming Approach to FPGA-Accelerated Computing
Venue: arXiv cs.DC 2014
Year: 2014

This paper introduces an effort to incorporate reconfigurable logic (FPGA) components into a software programming model. For this purpose, we have implemented a hardware engine for remote memory communication between hardware computation nodes and CPUs. The hardware engine is compatible with the API of GASNet, a popular communication library used for parallel computing applications. We have further implemented our own x86 and ARMv7 software versions of the GASNet Core API, enabling us to write distributed applications with software and hardware GASNet components transparently communicating with each other.
Reaching Consensus via non-Bayesian Asynchronous Learning in Social Networks
Venue: arXiv cs.GT 2014
Year: 2014

We study the outcomes of information aggregation in online social networks. Our main result is that networks with certain realistic structural properties avoid information cascades and enable a population to effectively aggregate information. In our model, each individual in a network holds a private, independent opinion about a product or idea, biased toward a ground truth. Individuals declare their opinions asynchronously, can observe the stated opinions of their neighbors, and are free to update their declarations over time. Supposing that individuals conform with the majority report of their neighbors, we ask whether the population will eventually arrive at consensus on the ground truth. We show that the answer depends on the network structure: there exist networks for which consensus is unlikely, or for which declarations converge on the incorrect opinion with positive probability. On the other hand, we prove that for networks that are sparse and expansive, the population will converge to the correct opinion with high probability.
A Bayesian Ensemble Regression Framework on the Angry Birds Game
Venue: arXiv cs.AI 2014
Year: 2014

An ensemble inference mechanism is proposed on the Angry Birds domain. It is based on an efficient tree structure for encoding and representing game screenshots, where it exploits its enhanced modeling capability. This has the advantage to establish an informative feature space and modify the task of game playing to a regression analysis problem. To this direction, we assume that each type of object material and bird pair has its own Bayesian linear regression model. In this way, a multi-model regression framework is designed that simultaneously calculates the conditional expectations of several objects and makes a target decision through an ensemble of regression models. Learning procedure is performed according to an online estimation strategy for the model parameters. We provide comparative experimental results on several game levels that empirically illustrate the efficiency of the proposed methodology.
The descriptive theory of represented spaces
Venue: arXiv cs.LO 2014
Year: 2014

This is a survey on the ongoing development of a descriptive theory of represented spaces, which is intended as an extension of both classical and effective descriptive set theory to deal with both sets and functions between represented spaces. Most material is from work-in-progress, and thus there may be a stronger focus on projects involving the author than an objective survey would merit.
Heat and Noise on Cubes and Spheres: The Sensitivity of Randomly Rotated Polynomial Threshold Functions
Venue: arXiv cs.CC 2014
Year: 2014

We establish a precise relationship between spherical harmonics and Fourier basis functions over a hypercube randomly embedded in the sphere. In particular, we give a bound on the expected Boolean noise sensitivity of a randomly rotated function in terms of its "spherical sensitivity," which we define according to its evolution under the spherical heat equation. As an application, we prove an average case of the Gotsman-Linial conjecture, bounding the sensitivity of polynomial threshold functions subjected to a random rotation.
Interpreting Tree Ensembles with inTrees
Venue: arXiv cs.LG 2014
Year: 2014

Tree ensembles such as random forests and boosted trees are accurate but difficult to understand, debug and deploy. In this work, we provide the inTrees (interpretable trees) framework that extracts, measures, prunes and selects rules from a tree ensemble, and calculates frequent variable interactions. An rule-based learner, referred to as the simplified tree ensemble learner (STEL), can also be formed and used for future prediction. The inTrees framework can applied to both classification and regression problems, and is applicable to many types of tree ensembles, e.g., random forests, regularized random forests, and boosted trees. We implemented the inTrees algorithms in the "inTrees" R package.
New Ideas for Brain Modelling 2
Venue: arXiv cs.AI 2014
Year: 2014

This paper describes a relatively simple way of allowing a brain model to self-organise its concept patterns through nested structures. For a simulation, time reduction is helpful and it would be able to show how patterns may form and then fire in sequence, as part of a search or thought process. It uses a very simple equation to show how the inhibitors in particular, can switch off certain areas, to allow other areas to become the prominent ones and thereby define the current brain state. This allows for a small amount of control over what appears to be a chaotic structure inside of the brain. It is attractive because it is still mostly mechanical and therefore can be added as an automatic process, or the modelling of that. The paper also describes how the nested pattern structure can be used as a basic counting mechanism. Another mathematical conclusion provides a basis for maintaining memory or concept patterns. The self-organisation can space itself through automatic processes. This might allow new neurons to be added in a more even manner and could help to maintain the concept integrity. The process might also help with finding memory structures afterwards. This extended version integrates further with the existing cognitive model and provides some new conclusions.
Towards Decision Support Technology Platform for Modular Systems
Venue: arXiv cs.SY 2014
Year: 2014

The survey methodological paper addresses a glance to a general decision support platform technology for modular systems (modular/composite alterantives/solutions) in various applied domains. The decision support platform consists of seven basic combinatorial engineering frameworks (system synthesis, system modeling, evaluation, detection of bottleneck, improvement/extension, multistage design, combinatorial evolution and forecasting). The decision support platform is based on decision support procedures (e.g., multicriteria selection/sorting, clustering), combinatorial optimization problems (e.g., knapsack, multiple choice problem, clique, assignment/allocation, covering, spanning trees), and their combinations. The following is described: (1) general scheme of the decision support platform technology; (2) brief descriptions of modular (composite) systems (or composite alternatives); (3) trends in moving from chocie/selection of alternatives to processing of composite alternatives which correspond to hierarchical modular products/systems; (4) scheme of resource requirements (i.e., human, information-computer); and (5) basic combinatorial engineering frameworks and their applications in various domains.
Desingularization of Ore Operators
Venue: arXiv cs.SC 2014
Year: 2014

We show that Ore operators can be desingularized by calculating a least common left multiple with a random operator of appropriate order. Our result generalizes a classical result about apparent singularities of linear differential equations, and it gives rise to a surprisingly simple desingularization algorithm.
Staged Evolution with Quality Gates for Model Libraries
Venue: arXiv cs.SE 2014
Year: 2014

Model evolution is widely considered as a subject under research. Despite its role in research, common purpose concepts, approaches, solutions, and methodologies are missing. Limiting the scope to model libraries makes model evolution and related quality concerns manageable, as we show below. In this paper, we put forward our quality staged model evolution theory for model libraries. It is founded on evolution graphs, which offer a structure for model evolution in model libraries through evolution steps. These evolution steps eventually form a sequence, which can be partitioned into stages by quality gates. Each quality gate is defined by a lightweight quality model and respective characteristics fostering reusability.
A Cross-Layer Approach for Distributed Energy-Efficient Power Control in Interference Networks
Venue: arXiv cs.NI 2014
Year: 2014

In contrast with existing works which rely on the same type of energy-efficiency measure to design distributed power control policies, the present work takes into account the presence of a finite packet buffer at the transmitter side and the impact of transport protocols. This approach is relevant when the transmitters have a non-zero energy cost even when the radiated power is zero. A generalized energy-efficiency performance metric integrating these features is constructed under two different scenarios in terms of transport layer protocols characterized by a constant or an adaptive packet arrival rate. The derived performance metric is shown to have several attractive properties in both scenarios, which ensures convergence of the used distributed power control algorithm to a unique point. This point is the Nash equilibrium of a game for which the equilibrium analysis is conducted. Although the equilibrium analysis methodology is not new in itself, conducting it requires several non-trivial proofs, including the proof of quasi-concavity of the payoff functions. A thorough numerical analysis is provided to illustrate the effects of the proposed approach, and provides several valuable insights in terms of designing interference management policies.
Event-triggered control of nonlinear singularly perturbed systems based only on the slow dynamics
Venue: arXiv cs.SY 2014
Year: 2014

Controllers are often designed based on a reduced or simplified model of the plant dynamics. In this context, we investigate whether it is possible to synthesize a stabilizing event-triggered feedback law for networked control systems (NCS) which have two time-scales, based only on an approximate model of the slow dynamics. We follow an emulation-like approach as we assume that we know how to solve the problem in the absence of sampling and then we study how to design the event-triggering rule under communication constraints. The NCS is modeled as a hybrid singularly perturbed system which exhibits the feature to generate jumps for both the fast variable and the error variable induced by the sampling. The first conclusion is that a triggering law which guarantees the stability and the existence of a uniform minimum amount of time between two transmissions for the slow model may not ensure the existence of such a time for the overall system, which makes the controller not implementable in practice. The objective of this contribution is twofold. We first show that existing event-triggering conditions can be adapted to singularly perturbed systems and semiglobal practical stability can be ensured in this case. Second, we propose another technique that combines event-triggered and time-triggered results in the sense that transmissions are only allowed after a predefined amount of time has elapsed since the last transmission. This technique has the advantage, under an additional assumption, to ensure a global asymptotic stability property and to allow the user to directly tune the minimum inter-transmission interval. We believe that this technique is of its own interest independently of the two-time scale nature of the addressed problem. The results are shown to be applicable to a class of globally Lipschitz systems.
First-Class Variability Modeling in Matlab/Simulink
Venue: arXiv cs.SE 2014
Year: 2014

Modern cars exist in an vast number of variants. Thus, variability has to be dealt with in all phases of the development process, in particular during model-based development of software-intensive functionality using Matlab/Simulink. Currently, variability is often encoded within a functional model leading to so called 150%-models which easily become very complex and do not scale for larger product lines. To counter these problems, we propose a modular variability modeling approach for Matlab/Simulink based on the concept of delta modeling [8, 9, 24]. A functional variant is described by a delta encapsulating a set of modifications. A sequence of deltas can be applied to a core product to derive the desired variant. We present a prototypical implementation, which is integrated into Matlab/Simulink and offers graphical editing of delta models.
Planar Octilinear Drawings with One Bend Per Edge
Venue: arXiv cs.DS 2014
Year: 2014

In octilinear drawings of planar graphs, every edge is drawn as an alternating sequence of horizontal, vertical and diagonal ($45^\circ$) line-segments. In this paper, we study octilinear drawings of low edge complexity, i.e., with few bends per edge. A $k$-planar graph is a planar graph in which each vertex has degree less or equal to $k$. In particular, we prove that every 4-planar graph admits a planar octilinear drawing with at most one bend per edge on an integer grid of size $O(n^2) \times O(n)$. For 5-planar graphs, we prove that one bend per edge still suffices in order to construct planar octilinear drawings, but in super-polynomial area. However, for 6-planar graphs we give a class of graphs whose planar octilinear drawings require at least two bends per edge.
The Fixpoint-Iteration Algorithm for Parity Games
Venue: arXiv cs.LO 2014
Year: 2014

It is known that the model checking problem for the modal mu-calculus reduces to the problem of solving a parity game and vice-versa. The latter is realised by the Walukiewicz formulas which are satisfied by a node in a parity game iff player 0 wins the game from this node. Thus, they define her winning region, and any model checking algorithm for the modal mu-calculus, suitably specialised to the Walukiewicz formulas, yields an algorithm for solving parity games. In this paper we study the effect of employing the most straight-forward mu-calculus model checking algorithm: fixpoint iteration. This is also one of the few algorithms, if not the only one, that were not originally devised for parity game solving already. While an empirical study quickly shows that this does not yield an algorithm that works well in practice, it is interesting from a theoretical point for two reasons: first, it is exponential on virtually all families of games that were designed as lower bounds for very particular algorithms suggesting that fixpoint iteration is connected to all those. Second, fixpoint iteration does not compute positional winning strategies. Note that the Walukiewicz formulas only define winning regions; some additional work is needed in order to make this algorithm compute winning strategies. We show that these are particular exponential-space strategies which we call eventually-positional, and we show how positional ones can be extracted from them.
Collaboration on Social Media: Analyzing Successful Projects on Social Coding
Venue: arXiv cs.SI 2014
Year: 2014

Social Coding Sites (SCSs) are social media services for sharing software development projects on the Web, and many open source projects are currently being developed on SCSs. One of the characteristics of SCSs is that they provide a platform on social networks that encourages collaboration between developers with the same interests and purpose. For example, external developers can easily report bugs and improvements to the project members. In this paper, we investigate keys to the success of projects on SCSs based on large data consisting of more than three hundred thousand projects. We focus on the following three perspectives: 1) the team structure, 2) social activity with external developers, and 3) content developed by the project. To evaluate the success quantitatively, we define activity, popularity and sociality as success indexes. A summary of the findings we obtained by using the techniques of correlation analysis, social network analysis and topic extraction is as follows: the number of project members and the connectivity between the members are positively correlated with success indexes. Second, projects that faithfully tackle change requests from external developers are more likely to be successful. Third, the success indexes differ between topics of softwares developed by projects. Our analysis suggests how to be successful in various projects, not limited to social coding.
Exact Algorithms for Dominating Induced Matching Based on Graph Partition
Venue: arXiv cs.DS 2014
Year: 2014

A dominating induced matching, also called an efficient edge domination, of a graph $G=(V,E)$ with $n=|V|$ vertices and $m=|E|$ edges is a subset $F \subseteq E$ of edges in the graph such that no two edges in $F$ share a common endpoint and each edge in $E\setminus F$ is incident with exactly one edge in $F$. It is NP-hard to decide whether a graph admits a dominating induced matching or not. In this paper, we design a $1.1467^nn^{O(1)}$-time exact algorithm for this problem, improving all previous results. This problem can be redefined as a partition problem that is to partition the vertex set of a graph into two parts $I$ and $F$, where $I$ induces an independent set (a 0-regular graph) and $F$ induces a perfect matching (a 1-regular graph). After giving several structural properties of the problem, we show that the problem always contains some "good vertices", branching on which by including them to either $I$ or $F$ we can effectively reduce the graph. This leads to a fast exact algorithm to this problem.
Subset seed automaton
Venue: arXiv cs.FL 2014
Year: 2014

We study the pattern matching automaton introduced in (A unifying framework for seed sensitivity and its application to subset seeds) for the purpose of seed-based similarity search. We show that our definition provides a compact automaton, much smaller than the one obtained by applying the Aho-Corasick construction. We study properties of this automaton and present an efficient implementation of the automaton construction. We also present some experimental results and show that this automaton can be successfully applied to more general situations.
2048 is (PSPACE) Hard, but Sometimes Easy
Venue: arXiv cs.CC 2014
Year: 2014

We prove that a variant of 2048, a popular online puzzle game, is PSPACE-Complete. Our hardness result holds for a version of the problem where the player has oracle access to the computer player's moves. Specifically, we show that for an $n \times n$ game board $\mathcal{G}$, computing a sequence of moves to reach a particular configuration $\mathbb{C}$ from an initial configuration $\mathbb{C}_0$ is PSPACE-Complete. Our reduction is from Nondeterministic Constraint Logic (NCL). We also show that determining whether or not there exists a fixed sequence of moves $\mathcal{S} \in \{\Uparrow, \Downarrow, \Leftarrow, \Rightarrow\}^k$ of length $k$ that results in a winning configuration for an $n \times n$ game board is fixed-parameter tractable (FPT). We describe an algorithm to solve this problem in $O(4^k n^2)$ time.
Optimal Linear Precoding in Multi-User MIMO Systems: A Large System Analysis
Venue: arXiv cs.IT 2014
Year: 2014

We consider the downlink of a single-cell multi-user MIMO system in which the base station makes use of $N$ antennas to communicate with $K$ single-antenna user equipments (UEs) randomly positioned in the coverage area. In particular, we focus on the problem of designing the optimal linear precoding for minimizing the total power consumption while satisfying a set of target signal-to-interference-plus-noise ratios (SINRs). To gain insights into the structure of the optimal solution and reduce the computational complexity for its evaluation, we analyze the asymptotic regime where $N$ and $K$ grow large with a given ratio and make use of recent results from large system analysis to compute the asymptotic solution. Then, we concentrate on the asymptotically design of heuristic linear precoding techniques. Interestingly, it turns out that the regularized zero-forcing (RZF) precoder is equivalent to the optimal one when the ratio between the SINR requirement and the average channel attenuation is the same for all UEs. If this condition does not hold true but only the same SINR constraint is imposed for all UEs, then the RZF can be modified to still achieve optimality if statistical information of the UE positions is available at the BS. Numerical results are used to evaluate the performance gap in the finite system regime and to make comparisons among the precoding techniques.
Developments in Formal Proofs
Venue: arXiv cs.LO 2014
Year: 2014

This report describes three particular technological advances in formal proofs. The HOL Light proof assistant will be used to illustrate the design of a highly reliable system. Today, proof assistants can verify large bodies of advanced mathematics; and as an example, we turn to the formal proof in Coq of the Feit-Thompson Odd Order theorem in group theory. Finally, we discuss advances in the automation of formal proofs, as implemented in proof assistants such as Mizar, Coq, Isabelle, and HOL Light.
A comparison of non-intrusive load monitoring methods for commercial and residential buildings
Venue: arXiv cs.SY 2014
Year: 2014

Non intrusive load monitoring (NILM), or energy disaggregation, is the process of separating the total electricity consumption of a building as measured at single point into the building's constituent loads. Previous research in the field has mostly focused on residential buildings, and although the potential benefits of applying this technology to commercial buildings have been recognised since the field's conception, NILM in the commercial domain has been largely unexplored by the academic community. As a result of the heterogeneity of this section of the building stock (i.e., encompassing buildings as diverse as airports, malls and coffee shops), and hence the loads within them, many of the solutions developed for residential energy disaggregation do not apply directly. In this paper we highlight some insights for NILM in the commercial domain using data collected from a large smart meter deployment within an educational campus in Delhi, India, of which a subset of the data has been released for public use. We present an empirical characterisation of loads in commercial buildings, highlighting the differences in energy consumption and load characteristics between residential and commercial buildings. We assess the validity of the assumptions generally made by NILM solutions for residential buildings when applied to measurements from commercial facilities. Based on our observations, we discuss the required traits for a NILM system for commercial buildings, and run benchmark residential NILM algorithms on our data set to confirm our observations. To advance the research in commercial buildings energy disaggregation, we release a subset of our data set, called COMBED (commercial building energy data set).