OpenRaiser/Intern-Atlas huggingface dataset:
Synthesis of Component and Connector Models from Crosscutting Structural Views
Venue: arXiv cs.SE 2014
Year: 2014

We present component and connector (C&C) views, which specify structural properties of component and connector models in an expressive and intuitive way. C&C views provide means to abstract away direct hierarchy, direct connectivity, port names and types, and thus can crosscut the traditional boundaries of the implementation-oriented hierarchical decomposition of systems and sub-systems, and reflect the partial knowledge available to different stakeholders involved in a system's design. As a primary application for C&C views we investigate the synthesis problem: given a C&C views specification, consisting of mandatory, alternative, and negative views, construct a concrete satisfying C&C model, if one exists. We show that the problem is NP-hard and solve it, in a bounded scope, using a reduction to SAT, via Alloy. We further extend the basic problem with support for library components, specification patterns, and architectural styles. The result of synthesis can be used for further exploration, simulation, and refinement of the C&C model or, as the complete, final model itself, for direct code generation. A prototype tool and an evaluation over four example systems with multiple specifications show promising results and suggest interesting future research directions towards a comprehensive development environment for the structure of component and connector designs.
Accelerating unstructured finite volume computations on field-programmable gate arrays
Venue: arXiv cs.PF 2014
Year: 2014

Accurate simulations of various physical processes on digital computers requires huge computing performance, therefore accelerating these scientific and engineering applications has a great importance. Density of programmable logic devices doubles in every 18 months according to Moore's Law. On the recent devices around one hundred double precision floating-point adders and multipliers can be implemented. In the paper an FPGA based framework is described to efficiently utilize this huge computing power to accelerate simulation of complex physical spatiotemporal phenomena. Simulating complicated geometries requires unstructured spatial discretization which results in irregular memory access patterns severely limiting computing performance. Data locality is improved by mesh node renumbering technique which results in predictable memory access pattern. Additionally storing a small window of node data in the on-chip memory of the FPGA can increase data reuse and decrease memory bandwidth requirements. Generation of the floating-point data path and control structure of the arithmetic unit containing dozens of operators is a very challenging task when the goal is high operating frequency. Long and high fanout control lines and improper placement can severely affect computing performance. In the paper an automatic data path generation and partitioning algorithm is presented to eliminate long delays and aid placement of the circuit. Efficiency and use of the framework is described by a case study solving the Euler equations on an unstructured mesh using finite volume technique. On the currently available largest FPGA the generated architecture contains three processing elements working in parallel providing 90 times speedup compared to a high performance microprocessor core.
Stabilization of nonlinear systems using event-triggered output feedback controllers
Venue: arXiv cs.SY 2014
Year: 2014

The objective is to design output feedback event-triggered controllers to stabilize a class of nonlinear systems. One of the main difficulties of the problem is to ensure the existence of a minimum amount of time between two consecutive transmissions, which is essential in practice. We solve this issue by combining techniques from event-triggered and time-triggered control. The idea is to turn on the event-triggering mechanism only after a fixed amount of time has elapsed since the last transmission. This time is computed based on results on the stabilization of time-driven sampled-data systems. The overall strategy ensures an asymptotic stability property for the closed-loop system. The results are proved to be applicable to linear time-invariant (LTI) systems as a particular case.
A Construction of MDS Quantum Convolutional Codes
Venue: arXiv cs.IT 2014
Year: 2014

In this paper, two new families of MDS quantum convolutional codes are constructed. The first one can be regarded as a generalization of \cite[Theorem 6.5]{GGGlinear}, in the sense that we do not assume that $q\equiv1\pmod{4}$. More specifically, we obtain two classes of MDS quantum convolutional codes with parameters: {\rm (i)}~ $[(q^2+1, q^2-4i+3,1;2,2i+2)]_q$, where $q\geq5$ is an odd prime power and $2\leq i\leq(q-1)/2$; {\rm (ii)}~ $[(\frac{q^2+1}{10},\frac{q^2+1}{10}-4i,1;2,2i+3)]_q$, where $q$ is an odd prime power with the form $q=10m+3$ or $10m+7$ ($m\geq2$), and $2\leq i\leq2m-1$.
Enabling FPGAs for the Masses
Venue: arXiv cs.SE 2014
Year: 2014

Implementing an application on a FPGA remains a difficult, non-intuitive task that often requires hardware design expertise in a hardware description language (HDL). High-level synthesis (HLS) raises the design abstraction from HDL to languages such as C/C++/Scala/Java. Despite this, in order to get a good quality of result (QoR), a designer must carefully craft the HLS code. In other words, HLS designers must implement the application using an abstract language in a manner that generates an efficient micro-architecture; we call this process writing restructured code. This reduces the benefits of implementing the application at a higher level of abstraction and limits the impact of HLS by requiring explicit knowledge of the underlying hardware architecture. Developers must know how to write code that reflects low level implementation details of the application at hand as it is interpreted by HLS tools. As a result, FPGA design still largely remains job of either hardware engineers or expert HLS designers. In this work, we aim to take a step towards making HLS tools useful for a broader set of programmers. To do this, we study methodologies of restructuring software code for HLS tools; we provide examples of designing different kernels in state-of-the art HLS tools; and we present a list of challenges for developing a hardware programming model for software programmers.
The Hardness of Finding Linear Ranking Functions for Lasso Programs
Venue: arXiv cs.LO 2014
Year: 2014

Finding whether a linear-constraint loop has a linear ranking function is an important key to understanding the loop behavior, proving its termination and establishing iteration bounds. If no preconditions are provided, the decision problem is known to be in coNP when variables range over the integers and in PTIME for the rational numbers, or real numbers. Here we show that deciding whether a linear-constraint loop with a precondition, specifically with partially-specified input, has a linear ranking function is EXPSPACE-hard over the integers, and PSPACE-hard over the rationals. The precise complexity of these decision problems is yet unknown. The EXPSPACE lower bound is derived from the reachability problem for Petri nets (equivalently, Vector Addition Systems), and possibly indicates an even stronger lower bound (subject to open problems in VAS theory). The lower bound for the rationals follows from a novel simulation of Boolean programs. Lower bounds are also given for the problem of deciding if a linear ranking-function supported by a particular form of inductive invariant exists. For loops over integers, the problem is PSPACE-hard for convex polyhedral invariants and EXPSPACE-hard for downward-closed sets of natural numbers as invariants.
Kleene Algebras, Regular Languages and Substructural Logics
Venue: arXiv cs.LO 2014
Year: 2014

We introduce the two substructural propositional logics KL, KL+, which use disjunction, fusion and a unary, (quasi-)exponential connective. For both we prove strong completeness with respect to the interpretation in Kleene algebras and a variant thereof. We also prove strong completeness for language models, where each logic comes with a different interpretation. We show that for both logics the cut rule is admissible and both have a decidable consequence relation.
Synthesis of Deterministic Top-down Tree Transducers from Automatic Tree Relations
Venue: arXiv cs.FL 2014
Year: 2014

We consider the synthesis of deterministic tree transducers from automaton definable specifications, given as binary relations, over finite trees. We consider the case of specifications that are deterministic top-down tree automatic, meaning the specification is recognizable by a deterministic top-down tree automaton that reads the two given trees synchronously in parallel. In this setting we study tree transducers that are allowed to have either bounded delay or arbitrary delay. Delay is caused whenever the transducer reads a symbol from the input tree but does not produce output. We provide decision procedures for both bounded and arbitrary delay that yield deterministic top-down tree transducers which realize the specification for valid input trees. Similar to the case of relations over words, we use two-player games to obtain our results.
A Formulation of the Potential for Communication Condition using C2KA
Venue: arXiv cs.LO 2014
Year: 2014

An integral part of safeguarding systems of communicating agents from covert channel communication is having the ability to identify when a covert channel may exist in a given system and which agents are more prone to covert channels than others. In this paper, we propose a formulation of one of the necessary conditions for the existence of covert channels: the potential for communication condition. Then, we discuss when the potential for communication is preserved after the modification of system agents in a potential communication path. Our approach is based on the mathematical framework of Communicating Concurrent Kleene Algebra (C2KA). While existing approaches only consider the potential for communication via shared environments, the approach proposed in this paper also considers the potential for communication via external stimuli.
Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power
Venue: arXiv cs.FL 2014
Year: 2014

There has been a growing interest in defining models of automata enriched with time. For instance, timed automata were introduced as automata extended with clocks. In this paper, we study models of timed finite state machines (TFSMs), i.e., FSMs enriched with time, which accept timed input words and generate timed output words. Here we discuss some models of TFSMs with a single clock: TFSMs with timed guards, TFSMs with timeouts, and TFSMs with both timed guards and timeouts. We solve the problem of equivalence checking for all three models, and we compare their expressive power, characterizing subclasses of TFSMs with timed guards and of TFSMs with timeouts that are equivalent to each other.
Recursive Session Types Revisited
Venue: arXiv cs.PL 2014
Year: 2014

Session types model structured communication-based programming. In particular, binary session types for the pi-calculus describe communication between exactly two participants in a distributed scenario. Adding sessions to the pi-calculus means augmenting it with type and term constructs. In a previous paper, we tried to understand to which extent the session constructs are more complex and expressive than the standard pi-calculus constructs. Thus, we presented an encoding of binary session pi-calculus to the standard typed pi-calculus by adopting linear and variant types and the continuation-passing principle. In the present paper, we focus on recursive session types and we present an encoding into recursive linear pi-calculus. This encoding is a conservative extension of the former in that it preserves the results therein obtained. Most importantly, it adopts a new treatment of the duality relation, which in the presence of recursive types has been proven to be quite challenging.
Coding Schemes for a Class of Receiver Message Side Information in AWGN Broadcast Channels
Venue: arXiv cs.IT 2014
Year: 2014

This paper considers the three-receiver AWGN broadcast channel where the receivers (i) have private-message requests and (ii) know some of the messages requested by other receivers as side information. For this setup, all possible side information configurations have been recently classified into eight groups and the capacity of the channel has been established for six groups (Asadi et al., ISIT 2014). We propose inner and outer bounds for the two remaining groups, groups 4 and 7. A distinguishing feature of these two groups is that the weakest receiver knows the requested message of the strongest receiver as side information while the in-between receiver does not. For group 4, the inner and outer bounds coincide at certain regions. For group 7, the inner and outer bounds coincide, thereby establishing the capacity, for four members out of all eight members of the group; for the remaining four members, the proposed bounds reduce the gap between the best known inner and outer bounds.
On symmetries of the Strassen algorithm
Venue: arXiv cs.CC 2014
Year: 2014

We consider the famous Strassen algorithm for fast multiplication of matrices. We show that this algorithm has a nontrivial finite group of automorphisms of order 36 (namely the direct product of two copies of the symmetric group on 3 symbols), or even 72, if we consider "extended" Strassen algorithm. This is an indirect evidence that the (unknown at present) optimal algorithm for multiplication of two size 3 by 3 matrices also may have a large automorphism group, and this may be a fruitful idea for a search of such an algorithm. In the beginning we give a brief introduction to the subject, to make the text accessible for specialists in the representation theory of finite groups.
Tension Bounds for Information Complexity
Venue: arXiv cs.CC 2014
Year: 2014

The main contribution of this work is to relate information complexity to "tension" [Prabhakaran and Prabhakaran, 2014] - an information-theoretic quantity defined with no reference to protocols - and to illustrate that it allows deriving strong lower-bounds on information complexity. In particular, we use a very special case of this connection to give a quantitatively tighter connection between information complexity and discrepancy than the one in the work of Braverman and Weinstein (2012) (albeit, restricted to independent inputs). Further, as tension is in fact a multi-dimensional notion, it enables us to bound the 2-dimensional region that represents the trade-off between the amounts of communication in the two directions in a 2-party protocol. This work is also intended to highlight tension as a fundamental measure of correlation between a pair of random variables, with rich connections to a variety of questions in computer science and information theory.
Function + Action = Interaction
Venue: arXiv cs.HC 2014
Year: 2014

This article presents the mathematical background of general interactive systems. The first principle of designing a large system is to _divide and conquer_, which implies that we could possibly reduce human error if we divided a large system in smaller subsystems. Interactive systems are, however, often composed of many subsystems that are _organically_ connected to one another and thus difficult to divide. In other words, we cannot apply a framework of set theory to the programming of interactive systems. We can overcome this difficulty by applying a framework of category theory (Kleisli category) to the programming, but this requires highly abstract mathematics, which is not very popular. In this article we introduce the fundamental idea of category theory using only lambda calculus, and then demonstrate how it can be used in the practical design of an interactive system. Finally, we mention how this discussion relates to category theory.
Finish Them!: Pricing Algorithms for Human Computation
Venue: arXiv cs.GT 2014
Year: 2014

Given a batch of human computation tasks, a commonly ignored aspect is how the price (i.e., the reward paid to human workers) of these tasks must be set or varied in order to meet latency or cost constraints. Often, the price is set up-front and not modified, leading to either a much higher monetary cost than needed (if the price is set too high), or to a much larger latency than expected (if the price is set too low). Leveraging a pricing model from prior work, we develop algorithms to optimally set and then vary price over time in order to meet a (a) user-specified deadline while minimizing total monetary cost (b) user-specified monetary budget constraint while minimizing total elapsed time. We leverage techniques from decision theory (specifically, Markov Decision Processes) for both these problems, and demonstrate that our techniques lead to upto 30\% reduction in cost over schemes proposed in prior work. Furthermore, we develop techniques to speed-up the computation, enabling users to leverage the price setting algorithms on-the-fly.
A Generic and Extensible Framework for Monitoring Energy Consumption of OpenStack Clouds
Venue: arXiv cs.DC 2014
Year: 2014

Although cloud computing has been transformational to the IT industry, it is built on large data centres that often consume massive amounts of electrical power. Efforts have been made to reduce the energy clouds consume, with certain data centres now approaching a Power Usage Effectiveness (PUE) factor of 1.08. While this is an incredible mark, it also means that the IT infrastructure accounts for a large part of the power consumed by a data centre. Hence, means to monitor and analyse how energy is spent have never been so crucial. Such monitoring is required not only for understanding how power is consumed, but also for assessing the impact of energy management policies. In this article, we draw lessons from experience on monitoring large-scale systems and introduce an energy monitoring software framework called KiloWatt API (KWAPI), able to handle OpenStack clouds. The framework --- whose architecture is scalable, extensible, and completely integrated into OpenStack --- supports several wattmeter devices, multiple measurement formats, and minimises communication overhead.
Definition and properties to assess multi-agent environments as social intelligence tests
Venue: arXiv cs.MA 2014
Year: 2014

Social intelligence in natural and artificial systems is usually measured by the evaluation of associated traits or tasks that are deemed to represent some facets of social behaviour. The amalgamation of these traits is then used to configure the intuitive notion of social intelligence. Instead, in this paper we start from a parametrised definition of social intelligence as the expected performance in a set of environments with several agents, and we assess and derive tests from it. This definition makes several dependencies explicit: (1) the definition depends on the choice (and weight) of environments and agents, (2) the definition may include both competitive and cooperative behaviours depending on how agents and rewards are arranged into teams, (3) the definition mostly depends on the abilities of other agents, and (4) the actual difference between social intelligence and general intelligence (or other abilities) depends on these choices. As a result, we address the problem of converting this definition into a more precise one where some fundamental properties ensuring social behaviour (such as action and reward dependency and anticipation on competitive/cooperative behaviours) are met as well as some other more instrumental properties (such as secernment, boundedness, symmetry, validity, reliability, efficiency), which are convenient to convert the definition into a practical test. From the definition and the formalised properties, we take a look at several representative multi-agent environments, tests and games to see whether they meet these properties.
The Binary Energy Harvesting Channel with a Unit-Sized Battery
Venue: arXiv cs.IT 2014
Year: 2014

We consider a binary energy harvesting communication channel with a finite-sized battery at the transmitter. In this model, the channel input is constrained by the available energy at each channel use, which is driven by an external energy harvesting process, the size of the battery, and the previous channel inputs. We consider an abstraction where energy is harvested in binary units and stored in a battery with the capacity of a single unit, and the channel inputs are binary. Viewing the available energy in the battery as a state, this is a state-dependent channel with input-dependent states, memory in the states, and causal state information available at the transmitter only. We find an equivalent representation for this channel based on the timings of the symbols, and determine the capacity of the resulting equivalent timing channel via an auxiliary random variable. We give achievable rates based on certain selections of this auxiliary random variable which resemble lattice coding for the timing channel. We develop upper bounds for the capacity by using a genie-aided method, and also by quantifying the leakage of the state information to the receiver. We show that the proposed achievable rates are asymptotically capacity achieving for small energy harvesting rates. We extend the results to the case of ternary channel inputs. Our achievable rates give the capacity of the binary channel within 0.03 bits/channel use, the ternary channel within 0.05 bits/channel use, and outperform basic Shannon strategies that only consider instantaneous battery states, for all parameter values.
Maximizing Mobile Coverage via Optimal Deployment of Base Station and Relays
Venue: arXiv cs.IT 2014
Year: 2014

Deploying relays and/or mobile base stations is a major means of extending the coverage of a wireless network. This paper presents models, analytical results, and algorithms to answer two related questions: The first is where to deploy relays in order to extend the reach from a base station to the maximum; the second is where to deploy a mobile base station and how many relays are needed to reach any point in a given area. Simple time-division and frequency-division scheduling schemes as well as an end-to-end data rate requirement are assumed. An important use case of the results is in the Public Safety Broadband Network, in which deploying relays and mobile base stations is often crucial to provide coverage to an incident scene.
An MPC approach to output-feedback control of stochastic linear discrete-time systems
Venue: arXiv cs.SY 2014
Year: 2014

In this paper we propose an output-feedback Model Predictive Control (MPC) algorithm for linear discrete-time systems affected by a possibly unbounded additive noise and subject to probabilistic constraints. In case the noise distribution is unknown, the chance constraints on the input and state variables are reformulated by means of the Chebyshev - Cantelli inequality. The recursive feasibility of the proposed algorithm is guaranteed and the convergence of the state to a suitable neighbor of the origin is proved under mild assumptions. The implementation issues are thoroughly addressed showing that, with a proper choice of the design parameters, its computational load can be made similar to the one of a standard stabilizing MPC algorithm. Two examples are discussed in details, with the aim of providing an insight on the performance achievable by the proposed control scheme.