Search

We present DivExplorer, a tool that enables users to explore datasets and find subgroups of data for which a classifier behaves in an anomalous manner. These subgroups, denoted as divergent subgroups, may exhibit, for example, higher-than-normal false positive or negative rates. DivExplorer can be used to analyze and debug classifiers. If the data has ethical or social implications, DivExplorer can be also used to identify bias in classifiers.

A new adaptive transmission protocol is introduced to improve the performance of slotted ALOHA. Nodes use known periodic schedules as base policies with which they collaboratively learn how to transmit periodically in different time slots so that packet collisions are minimized. The Adaptive Policy Tree (APT) algorithm is introduced for this purpose, which results in APT-ALOHA. APT-ALOHA does not require the presence of a central repeater and uses explicit acknowledgements to confirm the reception of packets. It is shown that nodes using APT-ALOHA quickly converge to transmission schedules that are virtually collision-free, and that the throughput of APT-ALOHA resembles that of TDMA, where slots are pre-allocated to nodes. In particular, APT-ALOHA attains a successful utilization of time slots- over 70% on saturation mode.

Identifying the top-K items in a set of items is a problem that finds applications in many areas, such as recommender systems, social review platforms, online contests, web search, and more. Crowdsourcing provides an effective way to collect input for such tasks with low costs and has attracted significant attention.We consider top-K problems in which the focus consists in selecting the set of top-K elements, regardless of their internal ordering. Past algorithms for top-K problems were generally based on a global sorting, which perform unnecessary work sorting elements that are all selected or all rejected. The exceptions are specialized crowdsourcing algorithms that have been proposed especially for top-K selection; these algorithms, however, require a fixed amount of work to be performed, and produce no useful intermediate answer.We propose here a dynamic top-K selection algorithm that uses crowdsourced comparisons to progressively classify items into selected in top-K, and rejected. As the comparisons proceed, more and more elements are accepted; intermediate results can be provided at any time by returning the already-accepted items along with the best among the ones that are still unclassified.We show that the algorithm we develop is efficient and robust with respect to comparison noise. We illustrate the performance of algorithm both analytically and experimentally, and show that our algorithm can achieve comparable precision in the selection of top-K items with less crowdsourcing work than previous algorithms.

Slotted ALOHA is known to have poor channel utilization (a maximum of 37% when average offered load is one packet per time slot). Reinforcement learning has recently been proposed as a technique that allows nodes to learn to coordinate their transmissions in order to attain much higher network utilization. All reinforcement learning schemes proposed to date assume immediate feedback on the outcome of a packet transmission. We introduce ALOHA-dQT, a reinforcement-learning protocol that achieves high utilization by having nodes broadcast short summaries of the channel history as known to them along with their packets. Our simulation results show that ALOHA-dQT leads to network utilization above 75%, with fair bandwidth allocation among nodes. ALOHA-dQT is the first reinforcement-learning approach applied to slotted ALOHA suitable for ad-hoc networks without centralized repeaters.

Graph edges, along with their labels, can represent information of fundamental importance, such as links between web pages, friendship between users, the rating given by users to other users or items, and much more. We introduce LEAP, a trainable, general framework for predicting the presence and properties of edges on the basis of the local structure, topology, and labels of the graph. The LEAP framework is based on the exploration and machine-learning aggregation of the paths connecting nodes in a graph. We provide several methods for performing the aggregation phase by training path aggregators, and we demonstrate the flexibility and generality of the framework by applying it to the prediction of links and user ratings in social networks. We validate the LEAP framework on two problems: link prediction, and user rating prediction. On eight large datasets, among which the arXiv collaboration network, the Yeast protein-protein interaction, and the US airlines routes network, we show that the link prediction performance of LEAP is at least as good as the current state of the art methods, such as SEAL and WLNM. Next, we consider the problem of predicting user ratings on other users: this problem is known as the edge-weight prediction problem in weighted signed networks (WSN). On Bitcoin networks, and Wikipedia RfA, we show that LEAP performs consistently better than the Fairness & Goodness based regression models, varying the amount of training edges between 10 to 90%. These examples demonstrate that LEAP, in spite of its generality, can match or best the performance of approaches that have been especially crafted to solve very specific edge prediction problems., To be published in The Proceedings of the 2019 World Wide Web Conference (WWW'19)

The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chap. 2), and subsequently extended to also handle quantitative features, such as real time (see Chap. 29), continuous flows (see Chap. 30), as well as stochastic phenomena, where system evolution is governed by a given probability distribution. Probabilistic model checking aims to establish the correctness of probabilistic system models against quantitative probabilistic specifications, such as those capable of expressing, for example, the probability of an unsafe event occurring, expected time to termination, or expected power consumption in the start-up phase. In this chapter, we present the foundations of probabilistic model checking, focusing on finite-state Markov decision processes as models and quantitative properties expressed in probabilistic temporal logic. Markov decision processes can be thought of as a probabilistic variant of labelled transition systems in the following sense: transitions are labelled with actions, which can be chosen nondeterministically, and successor states for the chosen action are specified by means of discrete probabilistic distributions, thus specifying the probability of transiting to each successor state. To reason about expectations, we additionally annotate Markov decision processes with quantitative costs, which are incurred upon taking the selected action from a given state. Quantitative properties are expressed as formulas of the probabilistic computation tree logic (PCTL) or using linear temporal logic (LTL). We summarise the main model-checking algorithms for both PCTL and LTL, and illustrate their working through examples. The chapter ends with a brief overview of extensions to more expressive models and temporal logics, existing probabilistic model-checking tool support, and main application domains.

Multithreaded programs coordinate their interaction through synchronization primitives like mutexes and semaphores, which are managed by an OS-provided resource manager. We propose algorithms for the automatic construction of code-aware resource managers for multithreaded embedded applications. Such managers use knowledge about the structure and resource usage (mutex and semaphore usage) of the threads to guarantee deadlock freedom and progress while managing resources in an efficient way. Our algorithms compute managers as winning strategies in certain infinite games, and produce a compact code description of these strategies. We have implemented the algorithms in the tool Cynthesis. Given a multithreaded program in C, the tool produces C code implementing a code-aware resource manager. We show in experiments that Cynthesis produces compact resource managers within a few minutes on a set of embedded benchmarks with up to 6 threads.

We propose techniques that obtain top-k lists of items out of larger itemsets, using human workers to perform comparisons among items. An example application is to short-list a large set of college applications using advanced students as workers. A method that obtains crowdsourced top-k lists has to address several challenges of crowdsourcing: there are constraints in the total number of tasks due to monetary or practical reasons; tasks posted to workers have an inherent limitation on their size; obtaining results from human workers has high latency; workers may disagree on their judgments for the same items or provide wrong results on purpose; and, there can be varying difficulty among tasks of the same size. We describe novel efficient techniques and explore their tolerance to adversarial behavior and the tradeoffs among different measures of performance (latency, expense and quality of results). We empirically evaluate the proposed techniques using simulations as well as real crowds in Amazon Mechanical Turk. A randomized variant of the proposed algorithms achieves significant budget saves, especially for very large itemsets and large top-k lists, with negligible risk of lowering the quality of the output.

Algorithmic-based user incentives ensure the trustworthiness of evaluations of Wikipedia entries and Google Maps business information.

Copyright © 2015 ACM. In online labor marketplaces two parties are involved; employers and workers. An employer posts a job in the marketplace to receive applications from interested workers. After evaluating the match to the job, the employer hires one (or more workers) to accomplish the job via an online contract. At the end of the contract, the employer can provide his worker with some rating that becomes visible in the worker online profile. This form of explicit feedback guides future hiring decisions, since it is indicative of worker true ability. In this paper, first we discuss some of the shortcomings of the existing reputation systems that are based on the end-of-contract ratings. Then we propose a new reputation mechanism that uses Bayesian updates to combine employer implicit feedback signals in a linkanalysis approach. The new system addresses the shortcomings of existing approaches, while yielding better signal for the worker quality towards hiring decision.

We consider two-player games played for an infinite number of rounds, with ω-regular winning conditions. The games may be concurrent, in that the players choose their moves simultaneously and independently, and probabilistic, in that the moves determine a probability distribution for the successor state. We introduce quantitative game μ-calculus, and we show that the maximal probability of winning such games can be expressed as the fixpoint formulas in this calculus. We develop the arguments both for deterministic and for probabilistic concurrent games; as a special case, we solve probabilistic turn-based games with ω-regular winning conditions, which was also open. We also characterize the optimality, and the memory requirements, of the winning strategies. In particular, we show that while memoryless strategies suffice for winning games with safety and reachability conditions, Büchi conditions require the use of strategies with infinite memory. The existence of optimal strategies, as opposed to ϵ-optimal, is only guaranteed in games with safety winning conditions.

Hybrid systems provide a formal model for physical systems controlled by discrete-state controllers. To help with the design of correct controllers, we present a methodology that enables the verification of linear-time temporal logic properties of general, non-linear hybrid systems. The methodology is based on the deductive transformation and algorithmic checking of hybrid diagrams.Hybrid diagrams are graphs whose vertices and edges are labeled with first-order assertions; they represent system abstractions, together with the progress properties that have been proved about them. The verification process begins with the automatic construction of an initial diagram, whose behavior coincides with that of the hybrid system. The proof of a specification is constructed by applying a series of diagram transformations to this initial diagram. The transformations preserve behavior containment, and the aim of the transformations is to obtain a diagram that can be algorithmically shown to satisfy the specification. Whenever the algorithmic check of a diagram fails, the check returns guidance for the further transformation of the diagram, or indications about possible counterexamples to the specification.We present four rules for transforming diagrams: each rule enables the study of a certain class of temporal logic properties. While some rules can be applied unconditionally, others require the proof of first-order verification conditions. We prove that the rules lead to the first verification methodology for general hybrid systems that is complete (relative to first-order reasoning) for proving specifications expressed in first-order linear-time temporal logic, provided no temporal operator appears in the scope of a quantifier.