OpenRaiser/Intern-Atlas huggingface dataset:
Proving Non-Deterministic Computations in Agda
Venue: arXiv cs.PL 2017
Year: 2017

We investigate proving properties of Curry programs using Agda. First, we address the functional correctness of Curry functions that, apart from some syntactic and semantic differences, are in the intersection of the two languages. Second, we use Agda to model non-deterministic functions with two distinct and competitive approaches incorporating the non-determinism. The first approach eliminates non-determinism by considering the set of all non-deterministic values produced by an application. The second approach encodes every non-deterministic choice that the application could perform. We consider our initial experiment a success. Although proving properties of programs is a notoriously difficult task, the functional logic paradigm does not seem to add any significant layer of difficulty or complexity to the task.
From Preference-Based to Multiobjective Sequential Decision-Making
Venue: arXiv cs.AI 2017
Year: 2017

In this paper, we present a link between preference-based and multiobjective sequential decision-making. While transforming a multiobjective problem to a preference-based one is quite natural, the other direction is a bit less obvious. We present how this transformation (from preference-based to multiobjective) can be done under the classic condition that preferences over histories can be represented by additively decomposable utilities and that the decision criterion to evaluate policies in a state is based on expectation. This link yields a new source of multiobjective sequential decision-making problems (i.e., when reward values are unknown) and justifies the use of solving methods developed in one setting in the other one.
A pre-semantics for counterfactual conditionals and similar logics
Venue: arXiv cs.AI 2017
Year: 2017

The elegant Stalnaker/Lewis semantics for counterfactual conditonals works with distances between models. But human beings certainly have no tables of models and distances in their head. We begin here an investigation using a more realistic picture, based on findings in neuroscience. We call it a pre-semantics, as its meaning is not a description of the world, but of the brain, whose structure is (partly) determined by the world it reasons about. In the final section, we reconsider the components, and postulate that there are no atomic pictures, we can always look inside.
On (Commercial) Benefits of Automatic Text Summarization Systems in the News Domain: A Case of Media Monitoring and Media Response Analysis
Venue: arXiv cs.CL 2017
Year: 2017

In this work, we present the results of a systematic study to investigate the (commercial) benefits of automatic text summarization systems in a real world scenario. More specifically, we define a use case in the context of media monitoring and media response analysis and claim that even using a simple query-based extractive approach can dramatically save the processing time of the employees without significantly reducing the quality of their work.
Optimized, Direct Sale of Privacy in Personal-Data Marketplaces
Venue: arXiv cs.CR 2017
Year: 2017

Very recently, we are witnessing the emergence of a number of start-ups that enables individuals to sell their private data directly to brokers and businesses. While this new paradigm may shift the balance of power between individuals and companies that harvest data, it raises some practical, fundamental questions for users of these services: how they should decide which data must be vended and which data protected, and what a good deal is. In this work, we investigate a mechanism that aims at helping users address these questions. The investigated mechanism relies on a hard-privacy model and allows users to share partial or complete profile data with broker companies in exchange for an economic reward. The theoretical analysis of the trade-off between privacy and money posed by such mechanism is the object of this work. We adopt a generic measure of privacy although part of our analysis focuses on some important examples of Bregman divergences. We find a parametric solution to the problem of optimal exchange of privacy for money, and obtain a closed-form expression and characterize the trade-off between profile-disclosure risk and economic reward for several interesting cases.
Privacy-Preserving Data Analysis for the Federal Statistical Agencies
Venue: arXiv cs.CY 2017
Year: 2017

Government statistical agencies collect enormously valuable data on the nation's population and business activities. Wide access to these data enables evidence-based policy making, supports new research that improves society, facilitates training for students in data science, and provides resources for the public to better understand and participate in their society. These data also affect the private sector. For example, the Employment Situation in the United States, published by the Bureau of Labor Statistics, moves markets. Nonetheless, government agencies are under increasing pressure to limit access to data because of a growing understanding of the threats to data privacy and confidentiality. "De-identification" - stripping obvious identifiers like names, addresses, and identification numbers - has been found inadequate in the face of modern computational and informational resources. Unfortunately, the problem extends even to the release of aggregate data statistics. This counter-intuitive phenomenon has come to be known as the Fundamental Law of Information Recovery. It says that overly accurate estimates of too many statistics can completely destroy privacy. One may think of this as death by a thousand cuts. Every statistic computed from a data set leaks a small amount of information about each member of the data set - a tiny cut. This is true even if the exact value of the statistic is distorted a bit in order to preserve privacy. But while each statistical release is an almost harmless little cut in terms of privacy risk for any individual, the cumulative effect can be to completely compromise the privacy of some individuals.
A Structural Characterization for Certifying Robinsonian Matrices
Venue: arXiv cs.DM 2017
Year: 2017

A symmetric matrix is Robinsonian if its rows and columns can be simultaneously reordered in such a way that entries are monotone nondecreasing in rows and columns when moving toward the diagonal. The adjacency matrix of a graph is Robinsonian precisely when the graph is a unit interval graph, so that Robinsonian matrices form a matrix analogue of the class of unit interval graphs. Here we provide a structural characterization for Robinsonian matrices in terms of forbidden substructures, extending the notion of asteroidal triples to weighted graphs. This implies the known characterization of unit interval graphs and leads to an efficient algorithm for certifying that a matrix is not Robinsonian.
Collapsing of dimensionality
Venue: arXiv cs.LG 2017
Year: 2017

We analyze a new approach to Machine Learning coming from a modification of classical regularization networks by casting the process in the time dimension, leading to a sort of collapse of dimensionality in the problem of learning the model parameters. This approach allows the definition of a online learning algorithm that progressively accumulates the knowledge provided in the input trajectory. The regularization principle leads to a solution based on a dynamical system that is paired with a procedure to develop a graph structure that stores the input regularities acquired from the temporal evolution. We report an extensive experimental exploration on the behavior of the parameter of the proposed model and an evaluation on artificial dataset.
On the Usability of Probably Approximately Correct Implication Bases
Venue: arXiv cs.AI 2017
Year: 2017

We revisit the notion of probably approximately correct implication bases from the literature and present a first formulation in the language of formal concept analysis, with the goal to investigate whether such bases represent a suitable substitute for exact implication bases in practical use-cases. To this end, we quantitatively examine the behavior of probably approximately correct implication bases on artificial and real-world data sets and compare their precision and recall with respect to their corresponding exact implication bases. Using a small example, we also provide qualitative insight that implications from probably approximately correct bases can still represent meaningful knowledge from a given data set.
PlatEMO: A MATLAB Platform for Evolutionary Multi-Objective Optimization
Venue: arXiv cs.NE 2017
Year: 2017

Over the last three decades, a large number of evolutionary algorithms have been developed for solving multiobjective optimization problems. However, there lacks an up-to-date and comprehensive software platform for researchers to properly benchmark existing algorithms and for practitioners to apply selected algorithms to solve their real-world problems. The demand of such a common tool becomes even more urgent, when the source code of many proposed algorithms has not been made publicly available. To address these issues, we have developed a MATLAB platform for evolutionary multi-objective optimization in this paper, called PlatEMO, which includes more than 50 multi-objective evolutionary algorithms and more than 100 multi-objective test problems, along with several widely used performance indicators. With a user-friendly graphical user interface, PlatEMO enables users to easily compare several evolutionary algorithms at one time and collect statistical results in Excel or LaTeX files. More importantly, PlatEMO is completely open source, such that users are able to develop new algorithms on the basis of it. This paper introduces the main features of PlatEMO and illustrates how to use it for performing comparative experiments, embedding new algorithms, creating new test problems, and developing performance indicators. Source code of PlatEMO is now available at: http://bimk.ahu.edu.cn/index.php?s=/Index/Software/index.html.
Double Link Failure Protection using a Single P-cycle
Venue: arXiv cs.NI 2017
Year: 2017

In this letter, we investigate survivability in optical networks for protection from two simultaneous link failures. Failure probability of two links with overlapping protection can be high if these links are geographically close. In a network with deterministic single link protection, simultaneous failure of two links may lead to partial or full loss of traffic on the failed links. Two link failure protection will make the network more resilient by protecting double failures having overlapping protection. A method for achieving double fault tolerance is double cycle method (DB); it uses two pre-configured cycles (p-cycles) to protect a link. Single p-cycle (SG) method, which uses one p-cycle to protect a link from two simultaneous link failure is introduced in this letter. Integer linear programs (ILP) are formulated for the SG method as well as DB method. It has been observed that the SG method provides a solution to bigger networks with lesser computational resources as compared to the DB method.
A Whole-Body Software Abstraction layer for Control Design of free-floating Mechanical Systems
Venue: arXiv cs.RO 2017
Year: 2017

In this paper, we propose a software abstraction layer to simplify the design and synthesis of whole-body controllers without making any preliminary assumptions on the control law to be implemented. The main advantage of the proposed library is the decoupling of the control software from implementation details, which are related to the robotic platform. Furthermore, the resulting code is more clean and concise than ad-hoc code, as it focuses only on the implementation of the control law. In addition, we present a reference implementation of the abstraction layer together with a Simulink interface to provide support to Model-Driven based development. We also show the implementation of a simple proportional-derivative plus gravity compensation control together with a more complex momentum-based bipedal balance controller.
A Concave Optimization Algorithm for Matching Partially Overlapping Point Sets
Venue: arXiv cs.CV 2017
Year: 2017

Point matching refers to the process of finding spatial transformation and correspondences between two sets of points. In this paper, we focus on the case that there is only partial overlap between two point sets. Following the approach of the robust point matching method, we model point matching as a mixed linear assignment-least square problem and show that after eliminating the transformation variable, the resulting problem of minimization with respect to point correspondence is a concave optimization problem. Furthermore, this problem has the property that the objective function can be converted into a form with few nonlinear terms via a linear transformation. Based on these properties, we employ the branch-and-bound (BnB) algorithm to optimize the resulting problem where the dimension of the search space is small. To further improve efficiency of the BnB algorithm where computation of the lower bound is the bottleneck, we propose a new lower bounding scheme which has a k-cardinality linear assignment formulation and can be efficiently solved. Experimental results show that the proposed algorithm outperforms state-of-the-art methods in terms of robustness to disturbances and point matching accuracy.
Charging and Discharging of Plug-In Electric Vehicles (PEVs) in Vehicle-to-Grid (V2G) Systems: A Cyber Insurance-Based Model
Venue: arXiv cs.GT 2017
Year: 2017

In addition to being environment-friendly, vehicle-to-grid (V2G) systems can help the plug-in electric vehicle (PEV) users in reducing their energy costs and can also help stabilizing energy demand in the power grid. In V2G systems, since the PEV users need to obtain system information (e.g., locations of charging/discharging stations, current load and supply of the power grid) to achieve the best charging and discharging performance, data communication plays a crucial role. However, since the PEV users are highly mobile, information from V2G systems is not always available for many reasons, e.g., wireless link failures and cyber attacks. Therefore, in this paper, we introduce a novel concept using cyber insurance to "transfer" cyber risks, e.g., unavailable information, of a PEV user to a third party, e.g., a cyber insurance company. Under the insurance coverage, even without information about V2G systems, a PEV user is always guaranteed the best price for charging/discharging. In particular, we formulate the optimal energy cost problem for the PEV user by adopting a Markov decision process framework. We then propose a learning algorithm to help the PEV user make optimal decisions, e.g., to charge or discharge and to buy or not to buy insurance, in an online fashion. Through simulations, we show that cyber insurance is an efficient solution not only in dealing with cyber risks, but also in maximizing revenue of the PEV user.
An Event-B framework for the validation of Event-B refinement plugins
Venue: arXiv cs.SE 2017
Year: 2017

We propose an Event-B framework for modeling the underlying theoretical foundations of Event-B. The aim of this framework is to reuse, for Event-B itself, the refinement development process. This framework introduces first, a functional kernel through an Event-B context, then, it defines Event-B projects, their static and dynamic semantics through Event-B machines. We intend to use this framework for the validation of Event-B plugins related to distribution and for Event-B extensions related to composition and decomposition.
Metric Temporal Logic for Ontology-Based Data Access over Log Data
Venue: arXiv cs.LO 2017
Year: 2017

We present a new metric temporal logic HornMTL over dense time and its datalog extension datalogMTL. The use of datalogMTL is demonstrated in the context of ontology-based data access over meteorological data. We show decidability of answering ontology-mediated queries for a practically relevant non-recursive fragment of datalogMTL. Finally, we discuss directions of the future work, including the potential use-cases in analyzing log data of engines and devices.
Rollback and Forking Detection for Trusted Execution Environments using Lightweight Collective Memory
Venue: arXiv cs.DC 2017
Year: 2017

Novel hardware-aided trusted execution environments, as provided by Intel's Software Guard Extensions (SGX), enable to execute applications in a secure context that enforces confidentiality and integrity of the application state even when the host system is misbehaving. While this paves the way towards secure and trustworthy cloud computing, essential system support to protect persistent application state against rollback and forking attacks is missing. In this paper we present LCM - a lightweight protocol to establish a collective memory amongst all clients of a remote application to detect integrity and consistency violations. LCM enables the detection of rollback attacks against the remote application, enforces the consistency notion of fork-linearizability and notifies clients about operation stability. The protocol exploits the trusted execution environment, complements it with simple client-side operations, and maintains only small, constant storage at the clients. This simplifies the solution compared to previous approaches, where the clients had to verify all operations initiated by other clients. We have implemented LCM and demonstrated its advantages with a key-value store application. The evaluation shows that it introduces low network and computation overhead; in particular, a LCM-protected key-value store achieves 0.72x - 0.98x of a SGX-secured key-value store throughput.
Divergence and Sufficiency for Convex Optimization
Venue: arXiv cs.IT 2017
Year: 2017

Logarithmic score and information divergence appear in information theory, statistics, statistical mechanics, and portfolio theory. We demonstrate that all these topics involve some kind of optimization that leads directly to regret functions and such regret functions are often given by a Bregman divergence. If the regret function also fulfills a sufficiency condition it must be proportional to information divergence. We will demonstrate that sufficiency is equivalent to the apparently weaker notion of locality and it is also equivalent to the apparently stronger notion of monotonicity. These sufficiency conditions have quite different relevance in the different areas of application, and often they are not fulfilled. Therefore sufficiency conditions can be used to explain when results from one area can be transferred directly to another and when one will experience differences.
Non-linear Cyclic Codes that Attain the Gilbert-Varshamov Bound
Venue: arXiv cs.IT 2017
Year: 2017

We prove that there exist non-linear binary cyclic codes that attain the Gilbert-Varshamov bound.
The World's First Real-Time Testbed for Massive MIMO: Design, Implementation, and Validation
Venue: arXiv cs.IT 2017
Year: 2017

This paper sets up a framework for designing a massive multiple-input multiple-output (MIMO) testbed by investigating hardware (HW) and system-level requirements such as processing complexity, duplexing mode and frame structure. Taking these into account, a generic system and processing partitioning is proposed which allows flexible scaling and processing distribution onto a multitude of physically separated devices. Based on the given HW constraints such as maximum number of links and maximum throughput for peer-to-peer interconnections combined with processing capabilities, the framework allows to evaluate modular HW components. To verify our design approach, we present the LuMaMi (Lund University Massive MIMO) testbed which constitutes the first reconfigurable real-time HW platform for prototyping massive MIMO. Utilizing up to 100 base station antennas and more than 50 Field Programmable Gate Arrays, up to 12 user equipments are served on the same time/frequency resource using an LTE-like Orthogonal Frequency Division Multiplexing time-division duplex-based transmission scheme. Proof-of-concept tests with this system show that massive MIMO can simultaneously serve a multitude of users in a static indoor and static outdoor environment utilizing the same time/frequency resource.
GPU Multisplit: an extended study of a parallel algorithm
Venue: arXiv cs.DC 2017
Year: 2017

Multisplit is a broadly useful parallel primitive that permutes its input data into contiguous buckets or bins, where the function that categorizes an element into a bucket is provided by the programmer. Due to the lack of an efficient multisplit on GPUs, programmers often choose to implement multisplit with a sort. One way is to first generate an auxiliary array of bucket IDs and then sort input data based on it. In case smaller indexed buckets possess smaller valued keys, another way for multisplit is to directly sort input data. Both methods are inefficient and require more work than necessary: the former requires more expensive data movements while the latter spends unnecessary effort in sorting elements within each bucket. In this work, we provide a parallel model and multiple implementations for the multisplit problem. Our principal focus is multisplit for a small (up to 256) number of buckets. We use warp-synchronous programming models and emphasize warp-wide communications to avoid branch divergence and reduce memory usage. We also hierarchically reorder input elements to achieve better coalescing of global memory accesses. On a GeForce GTX 1080 GPU, we can reach a peak throughput of 18.93 Gkeys/s (or 11.68 Gpairs/s) for a key-only (or key-value) multisplit. Finally, we demonstrate how multisplit can be used as a building block for radix sort. In our multisplit-based sort implementation, we achieve comparable performance to the fastest GPU sort routines, sorting 32-bit keys (and key-value pairs) with a throughput of 3.0 G keys/s (and 2.1 Gpair/s).
Crowdsourcing with Tullock contests: A new perspective
Venue: arXiv cs.GT 2017
Year: 2017

Incentive mechanisms for crowdsourcing have been extensively studied under the framework of all-pay auctions. Along a distinct line, this paper proposes to use Tullock contests as an alternative tool to design incentive mechanisms for crowdsourcing. We are inspired by the conduciveness of Tullock contests to attracting user entry (yet not necessarily a higher revenue) in other domains. In this paper, we explore a new dimension in optimal Tullock contest design, by superseding the contest prize---which is fixed in conventional Tullock contests---with a prize function that is dependent on the (unknown) winner's contribution, in order to maximize the crowdsourcer's utility. We show that this approach leads to attractive practical advantages: (a) it is well-suited for rapid prototyping in fully distributed web agents and smartphone apps; (b) it overcomes the disincentive to participate caused by players' antagonism to an increasing number of rivals. Furthermore, we optimize conventional, fixed-prize Tullock contests to construct the most superior benchmark to compare against our mechanism. Through extensive evaluations, we show that our mechanism significantly outperforms the optimal benchmark, by over three folds on the crowdsourcer's utility cum profit and up to nine folds on the players' social welfare.