Dagstuhl Publishing
http://www.dagstuhl.de
RSS feed announcing the latest publications published by Schloss Dagstuhlen-en2010-06-082018-06-06http://www.dagstuhl.de/dagpub-rss.phpLIPIcs, Volume 121, DISC'18, Complete Volume
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9845
LIPIcs, Volume 121, DISC'18, Complete VolumeFri, 19 Oct 2018 10:31:14 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9845LIPIcs, Volume 120, TIME'18, Complete Volume
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9844
LIPIcs, Volume 120, TIME'18, Complete VolumeFri, 19 Oct 2018 10:30:58 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9844Software Business, Platforms, and Ecosystems: Fundamentals of Software Production Research (Dagstuhl Seminar 18182)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9764
This report documents the program and the outcomes of Dagstuhl Seminar 18182 "Software Business, Platforms, and Ecosystems: Fundamentals of Software Production Research". Mon, 08 Oct 2018 14:36:07 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9764Towards Accountable Systems (Dagstuhl Seminar 18181)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9763
This report documents the program and the outcomes of Dagstuhl Seminar 18181 "Towards Accountable Systems", which took place from April 29th to May 4th, 2018, at Schloss Dagstuhl - Leibniz Center for Informatics. Researchers and practitioners from academia and industry were brought together covering broad fields from computer and information science, public policy and law.Many risks and opportunities were discussed that relate to the alignment of systems technologies with developing legal and regulatory requirements and evolving user expectations. This report summarises outcomes of the seminar by highlighting key future research directions and challenges that lie on the path to developing systems that better align with accountability concerns.Mon, 08 Oct 2018 13:56:27 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9763Algebraic Effect Handlers go Mainstream (Dagstuhl Seminar 18172)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9762
Languages like C\#, C++, or JavaScript support complex control flow statements like exception handling, iterators (yield), and even asynchrony (async/await) through special extensions. For exceptions, the runtime needs to be extended with exception handling stack frames. For iterators and asynchrony, the situation is more involved, as the compiler needs to turn regular code into stack restoring state machines. Furthermore, these features need to interact as expected, e.g. finally blocks must not be forgotten in the state machines for iterators. And all of this work needs to be done again for the next control flow abstraction that comes along.Or we can use algebraic effect handlers! This single mechanism generalizes all the control flow abstractions listed above and more, composes freely, has simple operational semantics, and can be efficiently compiled, since there is just one mechanism that needs to be supported well. Handlers allow programmers to keep the code in direct-style, which is easy to reason about, and empower library writers to implement various high-level abstractions without special extensions.The idea of algebraic effects handlers has already been experimented with in the form of small research languages and libraries in several mainstream languages, including OCaml, Haskell, Clojure, and Scala. The next step, and the aim of this seminar, is to seriously consider adoption by mainstream languages including both functional languages such as OCaml or Haskell, as well as languages like JavaScript and the JVM and .NET ecosystems.Mon, 08 Oct 2018 13:54:55 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9762Normative Multi-Agent Systems (Dagstuhl Seminar 18171)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9761
This report documents the program and the outcomes of Dagstuhl Seminar 18171 "Normative Multi-Agent Systems".Normative multi-agent systems combine models for multi-agent systems with normative concepts, like obligations, permissions, and prohibitions. As such, they promise to be a suitable model, for example for (regulated) multiagent societies, organizations, electronic institutions, autonomous agent cooperation (with humans-in-the-loop) and much more.The aim of this seminar was to bring together researchers from various scientific disciplines, such as computer science, artificial intelligence, philosophy, law, cognitive science and social sciences to discuss the emerging topic concerning the responsibility of autonomous systems.Autonomous software systems and multi-agent systems in open environments require methodologies, models and tools to analyse and develop flexible control and coordination mechanisms. Without them, it is not possible to steer the behaviour and interaction of such systems and to ensure important overall properties. Normative multi-agent systems is an established area focussing on how norms can be used to control and coordinate autonomous systems and multi-agents systems without restricting the autonomy of the involved systems. Such control and coordination systems allow autonomous systems to violate norms, but respond to norm violations by means of various sanctioning mechanisms. Therefore it is crucial to determine which agents or agent groups are accountable for norm violations. The focus of this seminar laid on howthe responsibility of autonomous systems can be defined, modelled, analysed and computed.Mon, 08 Oct 2018 13:54:25 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9761Visualization of Biological Data - Crossroads (Dagstuhl Seminar 18161)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9760
Our ability to generate and collect biological data has accelerated significantly in the past two decades. In response, many novel computational and statistical analysis techniques have been developed to process and integrate biological data sets. However, in addition to computational and statistical approaches, visualization techniques are needed to enable the interpretation of data as well as the communication of results. The design and implementation of such techniques lies at the intersection of the biology, bioinformatics, and data visualization fields. The purpose of Dagstuhl Seminar 18161 "Visualization of Biological Data - Crossroads" was to bring together researchers from all three fields, to identify opportunities and challenges, and to develop a path forward for biological data visualization research.Tue, 02 Oct 2018 08:00:04 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9760Blockchains, Smart Contracts and Future Applications (Dagstuhl Seminar 18152)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9759
This report documents the Dagstuhl seminar 18152 "Blockchains, Smart Contracts & Future Applications". While Bitcoin currently works well in practice, there are many open questions regarding the long-term perspective of blockchain technologies, for both public and private/permissioned blockchains. It is yet unclear how processes can be designed to work in predictive ways and how to embed security in the lifecycle of smart contract development and deployment. Furthermore, the distributed nature of the system needs to be considered when thinking about which groups or individuals can influence future developments. Similar to 'real-world' societies, blockchains are based on mutual recognition of conventions. Diverse academic disciplines as well as industry can and need to collaborate to advance research in blockchain and to fully understand how the technology might impact our future lives.Tue, 02 Oct 2018 07:59:50 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9759Program Equivalence (Dagstuhl Seminar 18151)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9758
Program equivalence is the problem of proving that two programs are equal under some definition of equivalence, e.g., input-output equivalence. The field draws researchers from formal verification, semantics and logics.This report documents the program and the outcomes of Dagstuhl Seminar 18151 "Program Equivalence". The seminar was organized by the four official organizers mentioned above, and Dr. Nikos Tzevelekos from Queen-Mary University in London. Tue, 02 Oct 2018 07:59:38 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9758Front Matter, Table of Contents, Preface, Conference Organization, Awards
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9789
Front Matter, Table of Contents, Preface, Conference Organization, AwardsFri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9789Autonomous Vehicles: From Individual Navigation to Challenges of Distributed Swarms (Invited Talk)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9790
Recent years have seen impressive advancements in the development of robots on four wheels: autonomous cars. While much of this progress is owed to a combination of breakthroughs in artificial intelligence and improved sensors, dealing with complex, non-ideal scenarios, where errors or failures can turn out to be catastrophic is still largely unsolved; this will require combining "fast", heuristic approaches of machine learning with "slow", more deliberate methods of discrete algorithms and mathematical optimization. However, many of the real challenges go beyond performance guarantees for individual vehicles and aim at the behavior of swarms: How can we control the complex interaction of a distributed swarm of vehicles, such that the overall behavior can measure up to and go beyond the capabilities of humans? Even though many of our engineering colleagues do not fully realize this yet, there is no doubt that this will have to be based to no small part on expertise in distributed algorithms.I will present a multi-level overview of results and challenges, ranging from information exchanges of small groups all the way to game-theoretic mechanisms for large-scale control. Application scenarios do not just arise from road traffic (where short response times, large numbers of vehicles and individual interests give rise to many difficulties), but also from swarms of autonomous space vehicles (where huge distances, times and energies make distributed methods indispensable).Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9790Challenges for Machine Learning on Distributed Platforms (Invited Talk)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9791
Deep neural networks are trained by solving huge optimization problems with large datasets and millions of variables. On the surface, it seems that the size of these problems makes them a natural target for distributed computing. Despite this, most deep learning research still takes place on a single compute node with a small number of GPUs, and only recently have researchers succeeded in unlocking the power of HPC. In this talk, we'll give a brief overview of how deep networks are trained, and use HPC tools to explore and explain deep network behaviors. Then, we'll explain the problems and challenges that arise when scaling deep nets over large system, and highlight reasons why naive distributed training methods fail. Finally, we'll discuss recent algorithmic innovations that have overcome these limitations, including "big batch" training for tightly coupled clusters and supercomputers, and "variance reduction" strategies to reduce communication in high latency settings.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9791Logical Analysis of Distributed Systems: The Importance of Being Constructive (Invited Talk)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9792
The design and analysis of complex distributed systems proceeds along numerous levels of abstractions. One key abstraction step for reducing complexity is the passage from analog transistor electronics to synchronously clocked digital circuits. This significantly simplifies the modelling from continuous differential equations over the real numbers to discrete Mealy automata over two-valued Boolean algebra. Although typically taken for granted, this step is magic. How do we obtain clock synchronization from asynchronous communication of continuous values? How do we decide on the discrete meaning of continuous signals without a synchronization clock? From a logical perspective, the possibility of synchronization is paradoxical and appears "out of thin air." The chicken-or-egg paradox persists at higher levels abstraction for distributed software. We cannot achieve globally consistent state from local communications without synchronization. At the same time we cannot synchronize without access to globally consistent state. From this perspective, distributed algorithms such as for leader election, consensus or mutual exclusion do not strictly solve their task but merely reduce one synchronization problem to another.This talk revisits the logical justification of the synchronous abstraction claiming that correctness arguments, in so far as they are not merely reductions, must intrinsically depend on reasoning in classical logic. This is studied at the circuit level, where all software reductions must end. The well-known result that some synchronization elements cannot be implemented in delay-insensitive circuits is related to Berry's Thesis according to which digital circuits are delay-insensitive if and only if they are provably correct in constructive logic. More technically, the talk will show how non-inertial delays give rise to a constructive modal logic while inertial delays are inherently non-constructive. This gives a logical explanation for why inertial delays can be used to build arbiters, memory-cells and other synchronization elements, while non-inertial delays are not powerful enough. Though these results are tentative, they indicate the importance of logical constructiveness for metastable-free discrete abstractions of physical behavior. This also indicates that metastability is an unavoidable artifact of the digital abstraction in classical logic.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9792Selecting a Leader in a Network of Finite State Machines
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9793
This paper studies a variant of the leader election problem under the stone age model (Emek and Wattenhofer, PODC 2013) that considers a network of n randomized finite automata with very weak communication capabilities (a multi-frequency asynchronous generalization of the beeping model's communication scheme). Since solving the classic leader election problem is impossible even in more powerful models, we consider a relaxed variant, referred to as k-leader selection, in which a leader should be selected out of at most k initial candidates. Our main contribution is an algorithm that solves k-leader selection for bounded k in the aforementioned stone age model. On (general topology) graphs of diameter D, this algorithm runs in O~(D) time and succeeds with high probability. The assumption that k is bounded turns out to be unavoidable: we prove that if k = omega (1), then no algorithm in this model can solve k-leader selection with a (positive) constant probability.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9793The Role of A-priori Information in Networks of Rational Agents
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9794
Until now, distributed algorithms for rational agents have assumed a-priori knowledge of n, the size of the network. This assumption is challenged here by proving how much a-priori knowledge is necessary for equilibrium in different distributed computing problems. Duplication - pretending to be more than one agent - is the main tool used by agents to deviate and increase their utility when not enough knowledge about n is given.We begin by proving that when no information on n is given, equilibrium is impossible for both Coloring and Knowledge Sharing. We then provide new algorithms for both problems when n is a-priori known to all agents. However, what if agents have partial knowledge about n? We provide tight upper and lower bounds that must be a-priori known on n for equilibrium to be possible in Leader Election, Knowledge Sharing, Coloring, Partition and Orientation.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9794Distributed Approximate Maximum Matching in the CONGEST Model
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9795
We study distributed algorithms for the maximum matching problem in the CONGEST model, where each message must be bounded in size. We give new deterministic upper bounds, and a new lower bound on the problem.We begin by giving a distributed algorithm that computes an exact maximum (unweighted) matching in bipartite graphs, in O(n log n) rounds. Next, we give a distributed algorithm that approximates the fractional weighted maximum matching problem in general graphs. In a graph with maximum degree at most Delta, the algorithm computes a (1-epsilon)-approximation for the problem in time O(log(Delta W)/epsilon^2), where W is a bound on the ratio between the largest and the smallest edge weight. Next, we show a slightly improved and generalized version of the deterministic rounding algorithm of Fischer [DISC '17]. Given a fractional weighted maximum matching solution of value f for a given graph G, we show that in time O((log^2(Delta)+log^*n)/epsilon), the fractional solution can be turned into an integer solution of value at least (1-epsilon)f for bipartite graphs and (1-epsilon) * (g-1)/g * f for general graphs, where g is the length of the shortest odd cycle of G. Together with the above fractional maximum matching algorithm, this implies a deterministic algorithm that computes a (1-epsilon)* (g-1)/g-approximation for the weighted maximum matching problem in time O(log(Delta W)/epsilon^2 + (log^2(Delta)+log^* n)/epsilon).On the lower-bound front, we show that even for unweighted fractional maximum matching in bipartite graphs, computing an (1 - O(1/sqrt{n}))-approximate solution requires at least Omega~(D+sqrt{n}) rounds in CONGEST. This lower bound requires the introduction of a new 2-party communication problem, for which we prove a tight lower bound.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9795State Machine Replication Is More Expensive Than Consensus
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9796
Consensus and State Machine Replication (SMR) are generally considered to be equivalent problems. In certain system models, indeed, the two problems are computationally equivalent: any solution to the former problem leads to a solution to the latter, and vice versa. In this paper, we study the relation between consensus and SMR from a complexity perspective. We find that, surprisingly, completing an SMR command can be more expensive than solving a consensus instance. Specifically, given a synchronous system model where every instance of consensus always terminates in constant time, completing an SMR command does not necessarily terminate in constant time. This result naturally extends to partially synchronous models. Besides theoretical interest, our result also corresponds to practical phenomena we identify empirically. We experiment with two well-known SMR implementations (Multi-Paxos and Raft) and show that, indeed, SMR is more expensive than consensus in practice. One important implication of our result is that - even under synchrony conditions - no SMR algorithm can ensure bounded response times.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9796Allocate-On-Use Space Complexity of Shared-Memory Algorithms
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9797
Many fundamental problems in shared-memory distributed computing, including mutual exclusion [James E. Burns and Nancy A. Lynch, 1993], consensus [Leqi Zhu, 2016], and implementations of many sequential objects [Prasad Jayanti et al., 2000], are known to require linear space in the worst case. However, these lower bounds all work by constructing particular executions for any given algorithm that may be both very long and very improbable. The significance of these bounds is justified by an assumption that any space that is used in some execution must be allocated for all executions. This assumption is not consistent with the storage allocation mechanisms of actual practical systems.We consider the consequences of adopting a per-execution approach to space complexity, where an object only counts toward the space complexity of an execution if it is used in that execution. This allows us to show that many known randomized algorithms for fundamental problems in shared-memory distributed computing have expected space complexity much lower than the worst-case lower bounds, and that many algorithms that are adaptive in time complexity can also be made adaptive in space complexity. For the specific problem of mutual exclusion, we develop a new algorithm that illustrates an apparent trade-off between low expected space complexity and low expected RMR complexity. Whether this trade-off is necessary is an open problem.For some applications, it may be helpful to pay only for objects that are updated, as opposed to those that are merely read. We give a data structure that requires no space to represent objects that are not updated at the cost of a small overhead on those that are.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9797Almost Global Problems in the LOCAL Model
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9798
The landscape of the distributed time complexity is nowadays well-understood for subpolynomial complexities. When we look at deterministic algorithms in the LOCAL model and locally checkable problems (LCLs) in bounded-degree graphs, the following picture emerges:- There are lots of problems with time complexities Theta(log^* n) or Theta(log n). - It is not possible to have a problem with complexity between omega(log^* n) and o(log n). - In general graphs, we can construct LCL problems with infinitely many complexities between omega(log n) and n^{o(1)}.- In trees, problems with such complexities do not exist. However, the high end of the complexity spectrum was left open by prior work. In general graphs there are problems with complexities of the form Theta(n^alpha) for any rational 0 < alpha <=1/2, while for trees only complexities of the form Theta(n^{1/k}) are known. No LCL problem with complexity between omega(sqrt{n}) and o(n) is known, and neither are there results that would show that such problems do not exist. We show that:- In general graphs, we can construct LCL problems with infinitely many complexities between omega(sqrt{n}) and o(n).- In trees, problems with such complexities do not exist. Put otherwise, we show that any LCL with a complexity o(n) can be solved in time O(sqrt{n}) in trees, while the same is not true in general graphs.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9798A Population Protocol for Exact Majority with O(log5/3 n) Stabilization Time and Theta(log n) States
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9799
A population protocol is a sequence of pairwise interactions of n agents. During one interaction, two randomly selected agents update their states by applying a deterministic transition function. The goal is to stabilize the system at a desired output property. The main performance objectives in designing such protocols are small number of states per agent and fast stabilization time.We present a fast population protocol for the exact-majority problem, which uses Theta(log n) states (per agent) and stabilizes in O(log^{5/3} n) parallel time (i.e., in O(n log^{5/3} n) interactions) in expectation and with high probability. Alistarh et al. [SODA 2018] showed that exact-majority protocols which stabilize in expected O(n^{1-Omega(1)}) parallel time and have the properties of monotonicity and output dominance require Omega(log n) states. Note that the properties mentioned above are satisfied by all known population protocols for exact majority, including ours. They also showed an O(log^2 n)-time exact-majority protocol with O(log n) states, which, prior to our work, was the fastest exact-majority protocol with polylogarithmic number of states. The standard design framework for majority protocols is based on O(log n) phases and requires that all agents are well synchronized within each phase, leading naturally to upper bounds of the order of log^2 n because of Theta(log n) synchronization time per phase. We show how this framework can be tightened with weak synchronization to break the O(log^2 n) upper bound of previous protocols.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9799Integrated Bounds for Disintegrated Storage
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9800
We point out a somewhat surprising similarity between non-authenticated Byzantine storage, coded storage, and certain emulations of shared registers from smaller ones. A common characteristic in all of these is the inability of reads to safely return a value obtained in a single atomic access to shared storage. We collectively refer to such systems as disintegrated storage, and show integrated space lower bounds for asynchronous regular wait-free emulations in all of them. In a nutshell, if readers are invisible, then the storage cost of such systems is inherently exponential in the size of written values; otherwise, it is at least linear in the number of readers. Our bounds are asymptotically tight to known algorithms, and thus justify their high costs.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9800Distributed Recoloring
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9801
Given two colorings of a graph, we consider the following problem: can we recolor the graph from one coloring to the other through a series of elementary changes, such that the graph is properly colored after each step?We introduce the notion of distributed recoloring: The input graph represents a network of computers that needs to be recolored. Initially, each node is aware of its own input color and target color. The nodes can exchange messages with each other, and eventually each node has to stop and output its own recoloring schedule, indicating when and how the node changes its color. The recoloring schedules have to be globally consistent so that the graph remains properly colored at each point, and we require that adjacent nodes do not change their colors simultaneously.We are interested in the following questions: How many communication rounds are needed (in the deterministic LOCAL model of distributed computing) to find a recoloring schedule? What is the length of the recoloring schedule? And how does the picture change if we can use extra colors to make recoloring easier?The main contributions of this work are related to distributed recoloring with one extra color in the following graph classes: trees, 3-regular graphs, and toroidal grids.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9801A Tight Lower Bound for Semi-Synchronous Collaborative Grid Exploration
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9802
Recently, there has been a growing interest in grid exploration by agents with limited capabilities. We show that the grid cannot be explored by three semi-synchronous finite automata, answering an open question by Emek et al. [TCS'15] in the negative.In the setting we consider, time is divided into discrete steps, where in each step, an adversarially selected subset of the agents executes one look-compute-move cycle. The agents operate according to a shared finite automaton, where every agent is allowed to have a distinct initial state. The only means of communication is to sense the states of the agents sharing the same grid cell. The agents are equipped with a global compass and whenever an agent moves, the destination cell of the movement is chosen by the agent's automaton from the set of neighboring grid cells. In contrast to the four agent protocol by Emek et al., we show that three agents do not suffice for grid exploration.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9802Multi-Shot Distributed Transaction Commit
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9803
Atomic Commit Problem (ACP) is a single-shot agreement problem similar to consensus, meant to model the properties of transaction commit protocols in fault-prone distributed systems. We argue that ACP is too restrictive to capture the complexities of modern transactional data stores, where commit protocols are integrated with concurrency control, and their executions for different transactions are interdependent. As an alternative, we introduce Transaction Certification Service (TCS), a new formal problem that captures safety guarantees of multi-shot transaction commit protocols with integrated concurrency control. TCS is parameterized by a certification function that can be instantiated to support common isolation levels, such as serializability and snapshot isolation. We then derive a provably correct crash-resilient protocol for implementing TCS through successive refinement. Our protocol achieves a better time complexity than mainstream approaches that layer two-phase commit on top of Paxos-style replication.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9803Deterministic Blind Radio Networks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9804
Ad-hoc radio networks and multiple access channels are classical and well-studied models of distributed systems, with a large body of literature on deterministic algorithms for fundamental communications primitives such as broadcasting and wake-up. However, almost all of these algorithms assume knowledge of the number of participating nodes and the range of possible IDs, and often make the further assumption that the latter is linear in the former. These are very strong assumptions for models which were designed to capture networks of weak devices organized in an ad-hoc manner. It was believed that without this knowledge, deterministic algorithms must necessarily be much less efficient.In this paper we address this fundamental question and show that this is not the case. We present deterministic algorithms for blind networks (in which nodes know only their own IDs), which match or nearly match the running times of the fastest algorithms which assume network knowledge (and even surpass the previous fastest algorithms which assume parameter knowledge but not small labels).Specifically, in multiple access channels with k participating nodes and IDs up to L, we give a wake-up algorithm requiring O((k log L log k)/(log log k)) time, improving dramatically over the O(L^3 log^3 L) time algorithm of De Marco et al. (2007), and a broadcasting algorithm requiring O(k log L log log k) time, improving over the O(L) time algorithm of Gasieniec et al. (2001) in most circumstances. Furthermore, we show how these same algorithms apply directly to multi-hop radio networks, achieving even larger running time improvements.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9804Detecting Cliques in CONGEST Networks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9805
The problem of detecting network structures plays a central role in distributed computing. One of the fundamental problems studied in this area is to determine whether for a given graph H, the input network contains a subgraph isomorphic to H or not. We investigate this problem for H being a clique K_l in the classical distributed CONGEST model, where the communication topology is the same as the topology of the underlying network, and with limited communication bandwidth on the links.Our first and main result is a lower bound, showing that detecting K_l requires Omega(sqrt{n} / b) communication rounds, for every 4 <=l <=sqrt{n}, and Omega(n / (l b)) rounds for every l >= sqrt{n}, where b is the bandwidth of the communication links. This result is obtained by using a reduction to the set disjointness problem in the framework of two-party communication complexity. We complement our lower bound with a two-party communication protocol for listing all cliques in the input graph, which up to constant factors communicates the same number of bits as our lower bound for K_4 detection. This demonstrates that our lower bound cannot be improved using the two-party communication framework.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9805A Wealth of Sub-Consensus Deterministic Objects
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9806
The consensus hierarchy classifies shared an object according to its consensus number, which is the maximum number of processes that can solve consensus wait-free using the object. The question of whether this hierarchy is precise enough to fully characterize the synchronization power of deterministic shared objects was open until 2016, when Afek et al. showed that there is an infinite hierarchy of deterministic objects, each weaker than the next, which is strictly between i and i+1-processors consensus, for i >= 2. For i=1, the question whether there exist a deterministic object whose power is strictly between read-write and 2-processors consensus, remained open.We resolve the question positively by exhibiting an infinite hierarchy of simple deterministic objects which are equivalent to set-consensus tasks, and thus are stronger than read-write registers, but they cannot implement consensus for two processes. Still our paper leaves a gap with open questions.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9806NUMASK: High Performance Scalable Skip List for NUMA
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9807
This paper presents NUMASK, a skip list data structure specifically designed to exploit the characteristics of Non-Uniform Memory Access (NUMA) architectures to improve performance. NUMASK deploys an architecture around a concurrent skip list so that all metadata accesses (e.g., traversals of the skip list index levels) read and write memory blocks allocated in the NUMA zone where the thread is executing. To the best of our knowledge, NUMASK is the first NUMA-aware skip list design that goes beyond merely limiting the performance penalties introduced by NUMA, and leverages the NUMA architecture to outperform state-of-the-art concurrent high-performance implementations. We tested NUMASK on a four-socket server. Its performance scales for both read-intensive and write-intensive workloads (tested up to 160 threads). In write-intensive workload, NUMASK shows speedups over competitors in the range of 2x to 16x.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9807TuringMobile: A Turing Machine of Oblivious Mobile Robots with Limited Visibility and Its Applications
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9808
In this paper we investigate the computational power of a set of mobile robots with limited visibility. At each iteration, a robot takes a snapshot of its surroundings, uses the snapshot to compute a destination point, and it moves toward its destination. Each robot is punctiform and memoryless, it operates in R^m, it has a local reference system independent of the other robots' ones, and is activated asynchronously by an adversarial scheduler. Moreover, the robots are non-rigid, in that they may be stopped by the scheduler at each move before reaching their destination (but are guaranteed to travel at least a fixed unknown distance before being stopped).We show that despite these strong limitations, it is possible to arrange 3m+3k of these weak entities in R^m to simulate the behavior of a stronger robot that is rigid (i.e., it always reaches its destination) and is endowed with k registers of persistent memory, each of which can store a real number. We call this arrangement a TuringMobile. In its simplest form, a TuringMobile consisting of only three robots can travel in the plane and store and update a single real number. We also prove that this task is impossible with fewer than three robots.Among the applications of the TuringMobile, we focused on Near-Gathering (all robots have to gather in a small-enough disk) and Pattern Formation (of which Gathering is a special case) with limited visibility. Interestingly, our investigation implies that both problems are solvable in Euclidean spaces of any dimension, even if the visibility graph of the robots is initially disconnected, provided that a small amount of these robots are arranged to form a TuringMobile. In the special case of the plane, a basic TuringMobile of only three robots is sufficient.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9808Beeping a Deterministic Time-Optimal Leader Election
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9809
The beeping model is an extremely restrictive broadcast communication model that relies only on carrier sensing. In this model, we solve the leader election problem with an asymptotically optimal round complexity of O(D + log n), for a network of unknown size n and unknown diameter D (but with unique identifiers). Contrary to the best previously known algorithms in the same setting, the proposed one is deterministic. The techniques we introduce give a new insight as to how local constraints on the exchangeable messages can result in efficient algorithms, when dealing with the beeping model.Using this deterministic leader election algorithm, we obtain a randomized leader election algorithm for anonymous networks with an asymptotically optimal round complexity of O(D + log n) w.h.p. In previous works this complexity was obtained in expectation only.Moreover, using deterministic leader election, we obtain efficient algorithms for symmetry-breaking and communication procedures: O(log n) time MIS and 5-coloring for tree networks (which is time-optimal), as well as k-source multi-broadcast for general graphs in O(min(k,log n) * D + k log{(n M)/k}) rounds (for messages in {1,..., M}). This latter result improves on previous solutions when the number of sources k is sublogarithmic (k = o(log n)).Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9809An Almost Tight RMR Lower Bound for Abortable Test-And-Set
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9810
We prove a lower bound of Omega(log n/log log n) for the remote memory reference (RMR) complexity of abortable test-and-set (leader election) in the cache-coherent (CC) and the distributed shared memory (DSM) model. This separates the complexities of abortable and non-abortable test-and-set, as the latter has constant RMR complexity [Wojciech Golab et al., 2010].Golab, Hendler, Hadzilacos and Woelfel [Wojciech M. Golab et al., 2012] showed that compare-and-swap can be implemented from registers and test-and-set objects with constant RMR complexity. We observe that a small modification to that implementation is abortable, provided that the used test-and-set objects are atomic (or abortable). As a consequence, using existing efficient randomized wait-free implementations of test-and-set [George Giakkoupis and Philipp Woelfel, 2012], we obtain randomized abortable compare-and-swap objects with almost constant (O(log^* n)) RMR complexity.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9810Distributed Set Cover Approximation: Primal-Dual with Optimal Locality
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9811
This paper presents a deterministic distributed algorithm for computing an f(1+epsilon) approximation of the well-studied minimum set cover problem, for any constant epsilon>0, in O(log (f Delta)/log log (f Delta)) rounds. Here, f denotes the maximum element frequency and Delta denotes the cardinality of the largest set. This f(1+epsilon) approximation almost matches the f-approximation guarantee of standard centralized primal-dual algorithms, which is known to be essentially the best possible approximation for polynomial-time computations. The round complexity almost matches the Omega(log (Delta)/log log (Delta)) lower bound of Kuhn, Moscibroda, Wattenhofer [JACM'16], which holds for even f=2 and for any poly(log Delta) approximation. Our algorithm also gives an alternative way to reproduce the time-optimal 2(1+epsilon)-approximation of vertex cover, with round complexity O(log Delta/log log Delta), as presented by Bar-Yehuda, Censor-Hillel, and Schwartzman [PODC'17] for weighted vertex cover. Our method is quite different and it can be viewed as a locality-optimal way of performing primal-dual for the more general case of set cover. We note that the vertex cover algorithm of Bar-Yehuda et al. does not extend to set cover (when f >= 3).Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9811Order out of Chaos: Proving Linearizability Using Local Views
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9812
Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning about the view of the memory obtained by the threads, because as they execute, threads observe different fragments of memory from different points in time. Until today, every linearizability proof has tackled this challenge from scratch.We present a unifying proof argument for the correctness of unsynchronized traversals, and apply it to prove the linearizability of several highly concurrent search data structures, including an optimistic self-balancing binary search tree, the Lazy List and a lock-free skip list. Our framework harnesses sequential reasoning about the view of a thread, considering the thread as if it traverses the data structure without interference from other operations. Our key contribution is showing that properties of reachability along search paths can be deduced for concurrent traversals from such interference-free traversals, when certain intuitive conditions are met. Basing the correctness of traversals on such local view arguments greatly simplifies linearizability proofs. At the heart of our result lies a notion of order on the memory, corresponding to the order in which locations in memory are read by the threads, which guarantees a certain notion of consistency between the view of the thread and the actual memory.To apply our framework, the user proves that the data structure satisfies two conditions: (1) acyclicity of the order on memory, even when it is considered across intermediate memory states, and (2) preservation of search paths to locations modified by interfering writes. Establishing the conditions, as well as the full linearizability proof utilizing our proof argument, reduces to simple concurrent reasoning. The result is a clear and comprehensible correctness proof, and elucidates common patterns underlying several existing data structures.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9812Redundancy in Distributed Proofs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9813
Distributed proofs are mechanisms enabling the nodes of a network to collectively and efficiently check the correctness of Boolean predicates on the structure of the network (e.g. having a specific diameter), or on data structures distributed over the nodes (e.g. a spanning tree). We consider well known mechanisms consisting of two components: a prover that assigns a certificate to each node, and a distributed algorithm called verifier that is in charge of verifying the distributed proof formed by the collection of all certificates. We show that many network predicates have distributed proofs offering a high level of redundancy, explicitly or implicitly. We use this remarkable property of distributed proofs to establish perfect tradeoffs between the size of the certificate stored at every node, and the number of rounds of the verification protocol.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9813Local Verification of Global Proofs
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9814
In this work we study the cost of local and global proofs on distributed verification. In this setting the nodes of a distributed system are provided with a nondeterministic proof for the correctness of the state of the system, and the nodes need to verify this proof by looking at only their local neighborhood in the system.Previous works have studied the model where each node is given its own, possibly unique, part of the proof as input. The cost of a proof is the maximum size of an individual label. We compare this model to a model where each node has access to the same global proof, and the cost is the size of this global proof.It is easy to see that a global proof can always include all of the local proofs, and every local proof can be a copy of the global proof. We show that there exists properties that exhibit these relative proof sizes, and also properties that are somewhere in between. In addition, we introduce a new lower bound technique and use it to prove a tight lower bound on the complexity of reversing distributed decision and establish a link between communication complexity and distributed proof complexity.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9814A Simple Parallel and Distributed Sampling Technique: Local Glauber Dynamics
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9815
Sampling constitutes an important tool in a variety of areas: from machine learning and combinatorial optimization to computational physics and biology. A central class of sampling algorithms is the Markov Chain Monte Carlo method, based on the construction of a Markov chain with the desired sampling distribution as its stationary distribution. Many of the traditional Markov chains, such as the Glauber dynamics, do not scale well with increasing dimension. To address this shortcoming, we propose a simple local update rule based on the Glauber dynamics that leads to efficient parallel and distributed algorithms for sampling from Gibbs distributions. Concretely, we present a Markov chain that mixes in O(log n) rounds when Dobrushin's condition for the Gibbs distribution is satisfied. This improves over the LubyGlauber algorithm by Feng, Sun, and Yin [PODC'17], which needs O(Delta log n) rounds, and their LocalMetropolis algorithm, which converges in O(log n) rounds but requires a considerably stronger mixing condition. Here, n denotes the number of nodes in the graphical model inducing the Gibbs distribution, and Delta its maximum degree. In particular, our method can sample a uniform proper coloring with alpha Delta colors in O(log n) rounds for any alpha >2, which almost matches the threshold of the sequential Glauber dynamics and improves on the alpha>2 + sqrt{2} threshold of Feng et al.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9815Fast Multidimensional Asymptotic and Approximate Consensus
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9816
We study the problems of asymptotic and approximate consensus in which agents have to get their values arbitrarily close to each others' inside the convex hull of initial values, either without or with an explicit decision by the agents. In particular, we are concerned with the case of multidimensional data, i.e., the agents' values are d-dimensional vectors. We introduce two new algorithms for dynamic networks, subsuming classical failure models like asynchronous message passing systems with Byzantine agents. The algorithms are the first to have a contraction rate and time complexity independent of the dimension d. In particular, we improve the time complexity from the previously fastest approximate consensus algorithm in asynchronous message passing systems with Byzantine faults by Mendes et al. [Distrib. Comput. 28] from Omega(d log (d Delta)/epsilon) to O(log Delta/epsilon), where Delta is the initial and epsilon is the terminal diameter of the set of vectors of correct agents.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9816Local Queuing Under Contention
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9817
We study stability of local packet scheduling policies in a distributed system of n nodes. The local policies at nodes may only access their local queues, and have no other feedback from the underlying distributed system. The packets arrive at queues according to arrival patterns controlled by an adversary restricted only by injection rate rho and burstiness b. In this work, we assume that the underlying distributed system is a shared channel, in which in order to get rid of a packet from the queue, a node needs to schedule it for transmission on the channel and no other packet is scheduled for transmission at the same time. We show that there is a local adaptive scheduling policy with relatively small memory, which is universally stable on a shared channel, that is, it has bounded queues for any rho<1 and b >= 0. On the other hand, without memory the maximal stable injection rate is O(1/log n). We show a local memoryless (non-adaptive) scheduling policy based on novel idea of ultra strong selectors which is stable for slightly smaller injection c/log^2 n, for some constant c>0.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9817Derandomizing Distributed Algorithms with Small Messages: Spanners and Dominating Set
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9818
This paper presents improved deterministic distributed algorithms, with O(log n)-bit messages, for some basic graph problems. The common ingredient in our results is a deterministic distributed algorithm for computing a certain hitting set, which can replace the random part of a number of standard randomized distributed algorithms. This deterministic hitting set algorithm itself is derived using a simple method of conditional expectations. As one main end-result of this derandomized hitting set, we get a deterministic distributed algorithm with round complexity 2^O(sqrt{log n * log log n}) for computing a (2k-1)-spanner of size O~(n^{1+1/k}). This improves considerably on a recent algorithm of Grossman and Parter [DISC'17] which needs O(n^{1/2-1/k} * 2^k) rounds. We also get a 2^O(sqrt{log n * log log n})-round deterministic distributed algorithm for computing an O(log^2 n)-approximation of minimum dominating set; all prior algorithms for this problem were either randomized or required large messages.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9818Distributed MST and Broadcast with Fewer Messages, and Faster Gossiping
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9819
We present a distributed minimum spanning tree algorithm with near-optimal round complexity of O~(D+sqrt{n}) and message complexity O~(min{n^{3/2}, m}). This is the first algorithm with sublinear message complexity and near-optimal round complexity and it improves over the recent algorithms of Elkin [PODC'17] and Pandurangan et al. [STOC'17], which have the same round complexity but message complexity O~(m). Our method also gives the first broadcast algorithm with o(n) time complexity - when that is possible at all, i.e., when D=o(n) - and o(m) messages. Moreover, our method leads to an O~(sqrt{nD})-round GOSSIP algorithm with bounded-size messages. This is the first such algorithm with a sublinear round complexity.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9819New Distributed Algorithms in Almost Mixing Time via Transformations from Parallel Algorithms
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9820
We show that many classical optimization problems - such as (1 +/- epsilon)-approximate maximum flow, shortest path, and transshipment - can be computed in tau_{mix}(G)* n^o(1) rounds of distributed message passing, where tau_{mix}(G) is the mixing time of the network graph G. This extends the result of Ghaffari et al. [PODC'17], whose main result is a distributed MST algorithm in tau_{mix}(G)* 2^O(sqrt{log n log log n}) rounds in the CONGEST model, to a much wider class of optimization problems. For many practical networks of interest, e.g., peer-to-peer or overlay network structures, the mixing time tau_{mix}(G) is small, e.g., polylogarithmic. On these networks, our algorithms bypass the Omega(sqrt n+D) lower bound of Das Sarma et al. [STOC'11], which applies for worst-case graphs and applies to all of the above optimization problems. For all of the problems except MST, this is the first distributed algorithm which takes o(sqrt n) rounds on a (nontrivial) restricted class of network graphs.Towards deriving these improved distributed algorithms, our main contribution is a general transformation that simulates any work-efficient PRAM algorithm running in T parallel rounds via a distributed algorithm running in T * tau_{mix}(G)* 2^O(sqrt{log n}) rounds. Work- and time-efficient parallel algorithms for all of the aforementioned problems follow by combining the work of Sherman [FOCS'13, SODA'17] and Peng and Spielman [STOC'14]. Thus, simulating these parallel algorithms using our transformation framework produces the desired distributed algorithms.The core technical component of our transformation is the algorithmic problem of solving multi-commodity routing - that is, roughly, routing n packets each from a given source to a given destination - in random graphs. For this problem, we obtain a new algorithm running in 2^O(sqrt{log n}) rounds, improving on the 2^O(sqrt{log n log log n}) round algorithm of Ghaffari, Kuhn, and Su [PODC'17]. As a consequence, for the MST problem in particular, we obtain an improved distributed algorithm running in tau_{mix}(G)* 2^O(sqrt{log n}) rounds.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9820Time-Message Trade-Offs in Distributed Algorithms
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9821
This paper focuses on showing time-message trade-offs in distributed algorithms for fundamental problems such as leader election, broadcast, spanning tree (ST), minimum spanning tree (MST), minimum cut, and many graph verification problems. We consider the synchronous CONGEST distributed computing model and assume that each node has initial knowledge of itself and the identifiers of its neighbors - the so-called KT_1 model - a well-studied model that also naturally arises in many applications. Recently, it has been established that one can obtain (almost) singularly optimal algorithms, i.e., algorithms that have simultaneously optimal time and message complexity (up to polylogarithmic factors), for many fundamental problems in the standard KT_0 model (where nodes have only local knowledge of themselves and not their neighbors). The situation is less clear in the KT_1 model. In this paper, we present several new distributed algorithms in the KT_1 model that trade off between time and message complexity.Our distributed algorithms are based on a uniform and general approach which involves constructing a sparsified spanning subgraph of the original graph - called a danner - that trades off the number of edges with the diameter of the sparsifier. In particular, a key ingredient of our approach is a distributed randomized algorithm that, given a graph G and any delta in [0,1], with high probability constructs a danner that has diameter O~(D + n^{1-delta}) and O~(min{m,n^{1+delta}}) edges in O~(n^{1-delta}) rounds while using O~(min{m,n^{1+delta}}) messages, where n, m, and D are the number of nodes, edges, and the diameter of G, respectively. Using our danner construction, we present a family of distributed randomized algorithms for various fundamental problems that exhibit a trade-off between message and time complexity and that improve over previous results. Specifically, we show the following results (all hold with high probability) in the KT_1 model, which subsume and improve over prior bounds in the KT_1 model (King et al., PODC 2014 and Awerbuch et al., JACM 1990) and the KT_0 model (Kutten et al., JACM 2015, Pandurangan et al., STOC 2017 and Elkin, PODC 2017):1) Leader Election, Broadcast, and ST. These problems can be solved in O~(D+n^{1-delta}) rounds using O~(min{m,n^{1+delta}}) messages for any delta in [0,1]. 2) MST and Connectivity. These problems can be solved in O~(D+n^{1-delta}) rounds using O~(min{m,n^{1+delta}}) messages for any delta in [0,0.5]. In particular, for delta = 0.5 we obtain a distributed MST algorithm that runs in optimal O~(D+sqrt{n}) rounds and uses O~(min{m,n^{3/2}}) messages. We note that this improves over the singularly optimal algorithm in the KT_0 model that uses O~(D+sqrt{n}) rounds and O~(m) messages.3) Minimum Cut. O(log n)-approximate minimum cut can be solved in O~(D+n^{1-delta}) rounds using O~(min{m,n^{1+delta}}) messages for any delta in [0,0.5]. 4) Graph Verification Problems such as Bipartiteness, Spanning Subgraph etc. These can be solved in O~(D+n^{1-delta}) rounds using O~(min{m,n^{1+delta}}) messages for any delta in [0,0.5].Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9821Faster Distributed Shortest Path Approximations via Shortcuts
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9822
A long series of recent results and breakthroughs have led to faster and better distributed approximation algorithms for single source shortest paths (SSSP) and related problems in the CONGEST model. The runtime of all these algorithms, however, is Omega~(sqrt{n}), regardless of the network topology, even on nice networks with a (poly)logarithmic network diameter D. While this is known to be necessary for some pathological networks, most topologies of interest are arguably not of this type.We give the first distributed approximation algorithms for shortest paths problems that adjust to the topology they are run on, thus achieving significantly faster running times on many topologies of interest. The running time of our algorithms depends on and is close to Q, where Q is the quality of the best shortcut that exists for the given topology. While Q = Theta~(sqrt{n} + D) for pathological worst-case topologies, many topologies of interest have Q = Theta~(D), which results in near instance optimal running times for our algorithm, given the trivial Omega(D) lower bound.The problems we consider are as follows: - an approximate shortest path tree and SSSP distances, - a polylogarithmic size distance label for every node such that from the labels of any two nodes alone one can determine their distance (approximately), and - an (approximately) optimal flow for the transshipment problem. Our algorithms have a tunable tradeoff between running time and approximation ratio. Our fastest algorithms have an arbitrarily good polynomial approximation guarantee and an essentially optimal O~(Q) running time. On the other end of the spectrum, we achieve polylogarithmic approximations in O~(Q * n^epsilon) rounds for any epsilon > 0. It seems likely that eventually, our non-trivial approximation algorithms for the SSSP tree and transshipment problem can be bootstrapped to give fast Q * 2^O(sqrt{log n log log n}) round (1+epsilon)-approximation algorithms using a recent result by Becker et al.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9822A Lower Bound for Adaptively-Secure Collective Coin-Flipping Protocols
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9823
In 1985, Ben-Or and Linial (Advances in Computing Research '89) introduced the collective coin-flipping problem, where n parties communicate via a single broadcast channel and wish to generate a common random bit in the presence of adaptive Byzantine corruptions. In this model, the adversary can decide to corrupt a party in the course of the protocol as a function of the messages seen so far. They showed that the majority protocol, in which each player sends a random bit and the output is the majority value, tolerates O(sqrt n) adaptive corruptions. They conjectured that this is optimal for such adversaries.We prove that the majority protocol is optimal (up to a poly-logarithmic factor) among all protocols in which each party sends a single, possibly long, message.Previously, such a lower bound was known for protocols in which parties are allowed to send only a single bit (Lichtenstein, Linial, and Saks, Combinatorica '89), or for symmetric protocols (Goldwasser, Kalai, and Park, ICALP '15).Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9823Adapting Local Sequential Algorithms to the Distributed Setting
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9824
It is a well known fact that sequential algorithms which exhibit a strong "local" nature can be adapted to the distributed setting given a legal graph coloring. The running time of the distributed algorithm will then be at least the number of colors. Surprisingly, this well known idea was never formally stated as a unified framework. In this paper we aim to define a robust family of local sequential algorithms which can be easily adapted to the distributed setting. We then develop new tools to further enhance these algorithms, achieving state of the art results for fundamental problems.We define a simple class of greedy-like algorithms which we call orderless-local algorithms. We show that given a legal c-coloring of the graph, every algorithm in this family can be converted into a distributed algorithm running in O(c) communication rounds in the CONGEST model. We show that this family is indeed robust as both the method of conditional expectations and the unconstrained submodular maximization algorithm of Buchbinder et al. [Niv Buchbinder et al., 2015] can be expressed as orderless-local algorithms for local utility functions - Utility functions which have a strong local nature to them.We use the above algorithms as a base for new distributed approximation algorithms for the weighted variants of some fundamental problems: Max k-Cut, Max-DiCut, Max 2-SAT and correlation clustering. We develop algorithms which have the same approximation guarantees as their sequential counterparts, up to a constant additive epsilon factor, while achieving an O(log^* n) running time for deterministic algorithms and O(epsilon^{-1}) running time for randomized ones. This improves exponentially upon the currently best known algorithms.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9824Strong Separations Between Broadcast and Authenticated Channels
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9825
In the theory of distributed systems and cryptography one considers a setting with n parties, (often) connected via authenticated bilateral channels, who want to achieve a certain goal even if some fraction of the parties is dishonest. A classical goal of this type is to construct a broadcast channel. A broadcast channel guarantees that all honest recipients get the same value v (consistency) and, if the sender is honest, that v is the sender's input (validity). Lamport et al. showed that it is possible to construct broadcast if and only if the fraction of cheaters is less than a third.A natural question, first raised by Lamport, is whether there are weaker, still useful primitives achievable from authenticated channels. He proposed weak broadcast, where the validity condition must hold only if all parties are honest, and showed that it can be achieved with an unbounded number of protocol rounds, while broadcast cannot, suggesting that weak broadcast is in a certain sense weaker than broadcast.The purpose of this paper is to deepen the investigation of the separation between broadcast and authenticated channels. This is achieved by proving the following results. First, we prove a stronger impossibility result for 3-party broadcast. Even if two of the parties can broadcast, one can not achieve broadcast for the third party. Second, we prove a strong separation between authenticated channels and broadcast by exhibiting a new primitive, called XOR-cast, which satisfies two conditions: (1) XOR-cast is strongly unachievable (even with small error probability) from authenticated channels (which is not true for weak broadcast), and (2) broadcast is strongly unachievable from XOR-cast (and authenticated channels). This demonstrates that the hierarchy of primitives has a more complex structure than previously known. Third, we prove a strong separation between weak broadcast and broadcast which is not implied by Lamport's results. The proofs of these results requires the generalization of known techniques for impossibility proofs.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9825Broadcast and Minimum Spanning Tree with o(m) Messages in the Asynchronous CONGEST Model
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9826
We provide the first asynchronous distributed algorithms to compute broadcast and minimum spanning tree with o(m) bits of communication, in a sufficiently dense graph with n nodes and m edges. For decades, it was believed that Omega(m) bits of communication are required for any algorithm that constructs a broadcast tree. In 2015, King, Kutten and Thorup showed that in the KT1 model where nodes have initial knowledge of their neighbors' identities it is possible to construct MST in O~(n) messages in the synchronous CONGEST model. In the CONGEST model messages are of size O(log n). However, no algorithm with o(m) messages were known for the asynchronous case. Here, we provide an algorithm that uses O(n^{3/2} log^{3/2} n) messages to find MST in the asynchronous CONGEST model. Our algorithm is randomized Monte Carlo and outputs MST with high probability. We will provide an algorithm for computing a spanning tree with O(n^{3/2} log^{3/2} n) messages. Given a spanning tree, we can compute MST with O~(n) messages.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9826Fault-Tolerant Consensus with an Abstract MAC Layer
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9827
In this paper, we study fault-tolerant distributed consensus in wireless systems. In more detail, we produce two new randomized algorithms that solve this problem in the abstract MAC layer model, which captures the basic interface and communication guarantees provided by most wireless MAC layers. Our algorithms work for any number of failures, require no advance knowledge of the network participants or network size, and guarantee termination with high probability after a number of broadcasts that are polynomial in the network size. Our first algorithm satisfies the standard agreement property, while our second trades a faster termination guarantee in exchange for a looser agreement property in which most nodes agree on the same value. These are the first known fault-tolerant consensus algorithms for this model. In addition to our main upper bound results, we explore the gap between the abstract MAC layer and the standard asynchronous message passing model by proving fault-tolerant consensus is impossible in the latter in the absence of information regarding the network participants, even if we assume no faults, allow randomized solutions, and provide the algorithm a constant-factor approximation of the network size.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9827Randomized (Delta+1)-Coloring in O(log* Delta) Congested Clique Rounds
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9828
(Delta+1)-vertex coloring is one of the most fundamental symmetry breaking graph problems, receiving tremendous amount of attention over the last decades. We consider the congested clique model where in each round, every pair of vertices can exchange O(log n) bits of information. In a recent breakthrough, Yi-Jun Chang, Wenzheng Li, and Seth Pettie [CLP-STOC'18] presented a randomized (Delta+1)-list coloring algorithm in the LOCAL model that works in O(log^*n+Det_{deg}(log log n)) rounds, where Det_{deg}(n') is the deterministic LOCAL complexity of (deg+1)-list coloring algorithm on n'-vertex graphs. Unfortunately, the CLP algorithm uses large messages and hence cannot be efficiently implemented in the congested clique model when the maximum degree Delta is large (in particular, when Delta=omega(sqrt{n})).Merav Parter [P-ICALP'18] recently provided a randomized (Delta+1)-coloring algorithm in O(log log Delta * log^* Delta) congested clique rounds based on a careful partitioning of the input graph into almost-independent subgraphs with maximum degree sqrt{n}. In this work, we significantly improve upon this result and present a randomized (Delta+1)-coloring algorithm with O(log^* Delta) rounds, with high probability. At the heart of our algorithm is an adaptation of the CLP algorithm for coloring a subgraph with o(n) vertices and maximum degree Omega(n^{5/8}) in O(log^* Delta) rounds. The approach is built upon a combination of techniques, this includes: the graph sparsification of [Parter-ICALP'18], and a palette sampling technique adopted to the CLP framework.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9828Congested Clique Algorithms for Graph Spanners
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9829
Graph spanners are sparse subgraphs that faithfully preserve the distances in the original graph up to small stretch. Spanner have been studied extensively as they have a wide range of applications ranging from distance oracles, labeling schemes and routing to solving linear systems and spectral sparsification. A k-spanner maintains pairwise distances up to multiplicative factor of k. It is a folklore that for every n-vertex graph G, one can construct a (2k-1) spanner with O(n^{1+1/k}) edges. In a distributed setting, such spanners can be constructed in the standard CONGEST model using O(k^2) rounds, when randomization is allowed.In this work, we consider spanner constructions in the congested clique model, and show: - a randomized construction of a (2k-1)-spanner with O~(n^{1+1/k}) edges in O(log k) rounds. The previous best algorithm runs in O(k) rounds;- a deterministic construction of a (2k-1)-spanner with O~(n^{1+1/k}) edges in O(log k +(log log n)^3) rounds. The previous best algorithm runs in O(k log n) rounds. This improvement is achieved by a new derandomization theorem for hitting sets which might be of independent interest;- a deterministic construction of a O(k)-spanner with O(k * n^{1+1/k}) edges in O(log k) rounds.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9829Lattice Agreement in Message Passing Systems
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9830
This paper studies the lattice agreement problem and the generalized lattice agreement problem in distributed message passing systems. In the lattice agreement problem, given input values from a lattice, processes have to non-trivially decide output values that lie on a chain. We consider the lattice agreement problem in both synchronous and asynchronous systems. For synchronous lattice agreement, we present two algorithms which run in log(f) and min{O(log^2 h(L)), O(log^2 f)} rounds, respectively, where h(L) denotes the height of the input sublattice L, f < n is the number of crash failures the system can tolerate, and n is the number of processes in the system. These algorithms have significant better round complexity than previously known algorithms. The algorithm by Attiya et al. [Attiya et al. DISC, 1995] takes log(n) synchronous rounds, and the algorithm by Mavronicolasa [Mavronicolasa, 2018] takes min{O(h(L)), O(sqrt(f))} rounds. For asynchronous lattice agreement, we propose an algorithm which has time complexity of 2*min{h(L), f + 1} message delays which improves on the previously known time complexity of O(n) message delays.The generalized lattice agreement problem defined by Faleiro et al in [Faleiro et al. PODC, 2012] is a generalization of the lattice agreement problem where it is applied for the replicated state machine. We propose an algorithm which guarantees liveness when a majority of the processes are correct in asynchronous systems. Our algorithm requires min{O(h(L)), O(f)} units of time in the worst case which is better than O(n) units of time required by the algorithm in [Faleiro et al. PODC, 2012].Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9830Brief Announcement: Local Distributed Algorithms in Highly Dynamic Networks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9831
We define a generalization of local distributed graph problems to (synchronous round-based) dynamic networks and present a framework for developing algorithms for these problems. We require two properties from our algorithms: (1) They should satisfy non-trivial guarantees in every round. The guarantees should be stronger the more stable the graph has been during the last few rounds and they coincide with the definition of the static graph problem if no topological change appeared recently. (2) If a constant neighborhood around some part of the graph is stable during an interval, the algorithms quickly converge to a solution for this part of the graph that remains unchanged throughout the interval.We demonstrate our generic framework with two classic distributed graph, namely (degree+1)-vertex coloring and maximal independent set (MIS).Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9831Brief Announcement: Randomized Blind Radio Networks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9832
Radio networks are a long-studied model for distributed system of devices which communicate wirelessly. When these devices are mobile or have limited capabilities, the system is best modeled by the ad-hoc variant, in which the devices do not know the structure of the network. Much work has been devoted to designing algorithms for the ad-hoc model, particularly for fundamental communications tasks such as broadcasting. Most of these algorithms, however, assume that devices have some network knowledge (usually bounds on the number of nodes in the network n, and the diameter D), which may not be realistic in systems with weak devices or gradual deployment. Little is known about what can be done without this information.This is the issue we address in this work, by presenting the first randomized broadcasting algorithms for blind networks in which nodes have no prior knowledge whatsoever. We demonstrate that lack of parameter knowledge can be overcome at only a small increase in running time. Specifically, we show that in networks without collision detection, broadcast can be achieved in O(D log n/D log^2 log n/D + log^2 n) time, almost reaching the Omega(D log n/D + log^2 n) lower bound. We also give an even faster algorithm for directed networks with collision detection.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9832Brief Announcement: Deterministic Contention Resolution on a Shared Channel
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9833
A shared channel, also called multiple-access channel, is one of the fundamental communication models. Autonomous entities communicate over a shared medium, and one of the main challenges is how to efficiently resolve collisions occurring when more than one entity attempts to access the channel at the same time. In this work we explore the impact of asynchrony, knowledge (or linear estimate) of the number of contenders, and acknowledgments, on both latency and channel utilization for the Contention resolution problem with non-adaptive deterministic algorithms.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9833Brief Announcement: Generalising Concurrent Correctness to Weak Memory
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9834
Correctness conditions like linearizability and opacity describe some form of atomicity imposed on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity) for concurrent objects executing in a weak memory model, where the histories of the objects in question are partially ordered. We establish compositionality and abstraction results for causal atomicity and develop an associated refinement-based proof technique.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9834Brief Announcement: Exact Size Counting in Uniform Population Protocols in Nearly Logarithmic Time
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9835
We study population protocols: networks of anonymous agents whose pairwise interactions are chosen uniformly at random. The size counting problem is that of calculating the exact number n of agents in the population, assuming no leader (each agent starts in the same state). We give the first protocol that solves this problem in sublinear time.The protocol converges in O(log n log log n) time and uses O(n^60) states (O(1) + 60 log n bits of memory per agent) with probability 1-O((log log n)/n). The time to converge is also O(log n log log n) in expectation. Crucially, unlike most published protocols with omega(1) states, our protocol is uniform: it uses the same transition algorithm for any population size, so does not need an estimate of the population size to be embedded into the algorithm.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9835Brief Announcement: A Tight Lower Bound for Clock Synchronization in Odd-Ary M-Toroids
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9836
In this paper we show a tight closed-form expression for the optimal clock synchronization in k-ary m-cubes with wraparound, where k is odd. This is done by proving a lower bound of 1/4um (k-1/k), where k is the (odd) number of processes in each of the m dimensions, and u is the uncertainty in delay on every link. Our lower bound matches the previously known upper bound.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9836Brief Announcement: On Simple Back-Off in Unreliable Radio Networks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9837
In this paper, we study local broadcast in the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Existing work proved that efficient solutions to these problems are impossible in the dual graph model under standard assumptions. In real networks, however, simple back-off strategies tend to perform well for solving these basic communication tasks. We address this apparent paradox by introducing a new set of constraints to the dual graph model that better generalize the slow/fast fading behavior common in real networks. We prove that in the context of these new constraints, simple back-off strategies now provide efficient solutions to local broadcast in the dual graph model. These results provide theoretical foundations for the practical observation that simple back-off algorithms tend to work well even amid the complicated link dynamics of real radio networks.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9837Brief Announcement: Fast and Scalable Group Mutual Exclusion
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9838
The group mutual exclusion (GME) problem is a generalization of the classical mutual exclusion problem in which every critical section is associated with a type or session. Critical sections belonging to the same session can execute concurrently, whereas critical sections belonging to different sessions must be executed serially. The well-known read-write mutual exclusion problem is a special case of the group mutual exclusion problem.In a shared memory system, locks based on traditional mutual exclusion or its variants are commonly used to manage contention among processes. In concurrent algorithms based on fine-grained synchronization, a single lock is used to protect access to a small number of shared objects (e.g., a lock for every tree node) so as to minimize contention window. Evidently, a large number of shared objects in the system would translate into a large number of locks. Also, when fine-grained synchronization is used, most lock accesses are expected to be uncontended in practice.Most existing algorithms for the solving the GME problem have high space-complexity per lock. Further, all algorithms except for one have high step-complexity in the uncontented case. This makes them unsuitable for use in concurrent algorithms based on fine-grained synchronization. In this work, we present a novel GME algorithm for an asynchronous shared-memory system that has O(1) space-complexity per GME lock when the system contains a large number of GME locks as well as O(1) step-complexity when the system contains no conflicting requests.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9838Brief Announcement: On the Impossibility of Detecting Concurrency
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9839
We identify a general principle of distributed computing: one cannot force two processes running in parallel to see each other. This principle is formally stated in the context of asynchronous processes communicating through shared objects, using trace-based semantics. We prove that it holds in a reasonable computational model, and then study the class of concurrent specifications which satisfy this property. This allows us to derive a Galois connection theorem for different variants of linearizability.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9839Brief Announcement: Effects of Topology Knowledge and Relay Depth on Asynchronous Consensus
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9840
Consider an asynchronous incomplete directed network. We study the feasibility and efficiency of approximate crash-tolerant consensus under different restrictions on topology knowledge and relay depth, i.e., the maximum number of hops any message can be relayed.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9840Brief Announcement: Loosely-stabilizing Leader Election with Polylogarithmic Convergence Time
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9841
We present a fast loosely-stabilizing leader election protocol in the population protocol model. It elects a unique leader in a poly-logarithmic time and holds the leader for a polynomial time with arbitrarily large degree in terms of parallel time, i.e, the number of steps per the population size.Fri, 28 Sep 2018 12:12:49 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9841Front Matter, Table of Contents, Preface, Conference Organization
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9765
Front Matter, Table of Contents, Preface, Conference OrganizationWed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9765On Temporal and Separation Logics (Invited Paper)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9766
There exist many success stories about the introduction of logics designed for the formal verification of computer systems. Obviously, the introduction of temporal logics to computer science has been a major step in the development of model-checking techniques. More recently, separation logics extend Hoare logic for reasoning about programs with dynamic data structures, leading to many contributions on theory, tools and applications. In this talk, we illustrate how several features of separation logics, for instance the key concept of separation, are related to similar notions in temporal logics. We provide formal correspondences (when possible) and present an overview of related works from the literature. This is also the opportunity to present bridges between well-known temporal logics and more recent separation logics.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9766Database Technology for Processing Temporal Data (Invited Paper)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9767
Despite the ubiquity of temporal data and considerable research on processing such data, database systems largely remain designed for processing the current state of some modeled reality. More recently, we have seen an increasing interest in processing historical or temporal data. The SQL:2011 standard introduced some temporal features, and commercial database management systems have started to offer temporal functionalities in a step-by-step manner. There has also been a proposal for a more fundamental and comprehensive solution for sequenced temporal queries, which allows a tight integration into relational database systems, thereby taking advantage of existing query optimization and evaluation technologies. New challenges for processing temporal data arise with multiple dimensions of time and the increasing amounts of data, including time series data that represent a special kind of temporal data.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9767Model Checking Strategic Ability - Why, What, and Especially: How? (Invited Paper)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9768
Automated verification of discrete-state systems has been a hot topic in computer science for over 35 years. Model checking of temporal and strategic properties is one of the most prominent and most successful approaches here. In this talk, I present a brief introduction to the topic, and mention some relevant properties that one might like to verify this way. Then, I describe some recent results on approximate model checking and model reductions, which can be applied to facilitate verification of notoriously hard cases.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9768Predicting the Evolution of Communities with Online Inductive Logic Programming
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9769
In the recent years research on dynamic social network has increased, which is also due to the availability of data sets from streaming media. Modeling a network's dynamic behaviour can be performed at the level of communities, which represent their mesoscale structure. Communities arise as a result of user to user interaction. In the current work we aim to predict the evolution of communities, i.e. to predict their future form. While this problem has been studied in the past as a supervised learning problem with a variety of classifiers, the problem is that the "knowledge" of a classifier is opaque and consequently incomprehensible to a human. Thus we have employed first order logic, and in particular the event calculus to represent the communities and their evolution. We addressed the problem of predicting the evolution as an online Inductive Logic Programming problem (ILP), where the issue is to learn first order logical clauses that associate evolutionary events, and particular Growth, Shrinkage, Continuation and Dissolution to lower level events. The lower level events are features that represent the structural and temporal characteristics of communities. Experiments have been performed on a real life data set form the Mathematics StackExchange forum, with the OLED framework for ILP. In doing so we have produced clauses that model both short term and long term correlations.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9769Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9770
Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For the specification purposes rich temporal languages are required that, in particular, can express fairness constraints. For linear-time logics which deal with fairness in the linear-time setting, one-pass and two-pass tableau methods have been developed. In the repository of the CTL-type branching-time setting, the well-known logics ECTL and ECTL^+ were developed to explicitly deal with fairness. However, due to the syntactical restrictions, these logics can only express restricted versions of fairness. The logic CTL^*, often considered as "the full branching-time logic" overcomes these restrictions on expressing fairness. However, this logic itself, is extremely challenging for the application of verification techniques, and the tableau technique, in particular. For example, there is no one-pass tableau construction for this logic, while it is known that one-pass tableau has an additional benefit enabling the formulation of dual sequent calculi that are often treated as more "natural" being more friendly for human understanding. Based on these two considerations, the following problem arises - are there logics that have richer expressiveness than ECTL^+ yet "simpler" than CTL^* for which a one-pass tableau can be developed? In this paper we give a solution to this problem. We present a tree-style one-pass tableau for a sub-logic of CTL^* that we call ECTL^#, which is more expressive than ECTL^+ allowing the formulation of a new range of fairness constraints with "until" operator. The presentation of the tableau construction is accompanied by an algorithm for constructing a systematic tableau, for any given input of admissible branching-time formulae. We prove the termination, soundness and completeness of the method. As tree-shaped one-pass tableaux are well suited for the automation and are amenable for the implementation and for the formulation of sequent calculi, our results also open a prospect of relevant developments of the automation and implementation of the tableau method for ECTL^#, and of a dual sequent calculi.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9770Results on Alternating-Time Temporal Logics with Linear Past
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9771
We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard CTL^* (resp., ATL^*). We establish by formal non-trivial arguments that the "memoryful" linear-past extension (the history leading to the current state is taken into account) can be exponentially more succinct than the standard "local" linear-past extension (the history leading to the current state is forgotten). As a second contribution, we consider the ATL-like fragment, denoted ATL_{lp}, of the known "memoryful" linear-past extension of ATL^{*}. We show that ATL_{lp} is strictly more expressive than ATL, and interestingly, it can be exponentially more succinct than the more expressive logic ATL^{*}. Moreover, we prove that both satisfiability and model-checking for the logic ATL_{lp} are Exptime-complete.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9771Extracting Interval Temporal Logic Rules: A First Approach
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9772
Discovering association rules is a classical data mining task with a wide range of applications that include the medical, the financial, and the planning domains, among others. Modern rule extraction algorithms focus on static rules, typically expressed in the language of Horn propositional logic, as opposed to temporal ones, which have received less attention in the literature. Since in many application domains temporal information is stored in form of intervals, extracting interval-based temporal rules seems the natural choice. In this paper we extend the well-known algorithm APRIORI for rule extraction to discover interval temporal rules written in the Horn fragment of Halpern and Shoham's interval temporal logic.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9772Faster Dynamic Controllability Checking for Simple Temporal Networks with Uncertainty
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9773
Simple Temporal Networks (STNs) are a well-studied model for representing and reasoning about time. An STN comprises a set of real-valued variables called time-points, together with a set of binary constraints, each of the form Y <= X+w. The problem of finding a feasible schedule (i.e., an assignment of real numbers to time-points such that all of the constraints are satisfied) is equivalent to the Single Source Shortest Path problem (SSSP) in the STN graph.Simple Temporal Networks with Uncertainty (STNUs) augment STNs to include contingent links that can be used, for example, to represent actions with uncertain durations. The duration of a contingent link is not controlled by the planner, but is instead controlled by a (possibly adversarial) environment. Each contingent link has the form, <A,l,u,C>, where 0 < l <= u < infty. Once the planner executes the activation time-point A, the environment must execute the contingent time-point C at some time A+Delta, where Delta in [l,u]. Crucially, the planner does not know the value of Delta in advance, but only discovers it when C executes. An STNU is dynamically controllable (DC) if there is a strategy that the planner can use to execute all of the non-contingent time-points, such that all of the constraints are guaranteed to be satisfied no matter which durations the environment chooses for the contingent links. The strategy can be dynamic in that it can react in real time to the contingent durations it observes. Recently, an upper bound of O(N^3) was given for the DC-checking problem for STNUs, where N is the number of time-points.This paper introduces a new algorithm, called the RUL^- algorithm, for solving the DC-checking problem for STNUs that improves on the O(N^3) bound. The worst-case complexity of the RUL^- algorithm is O(MN+K^2N+KN log N), where N is the number of time-points, M is the number of constraints, and K is the number of contingent time-points. If M is O(N^2), then the complexity reduces to O(N^3); however, in sparse graphs the complexity can be much less. For example, if M is O(N log N), and K is O(sqrt{N}), then the complexity of the RUL^- algorithm reduces to O(N^2 log N).The RUL^- algorithm begins by using the Bellman-Ford algorithm to compute a potential function. It then performs at most 2K rounds of computations, interleaving novel applications of Dijkstra's algorithm to (1) generate new edges and (2) update the potential function in response to those new edges. The constraint-propagation/edge-generation rules used by the RUL^- algorithm are distinguished from related work in two ways. First, they only generate unlabeled edges. Second, their applicability conditions are more restrictive. As a result, the RUL^- algorithm requires only O(K) rounds of Dijkstra's algorithm, instead of the O(N) rounds required by other approaches. The paper proves that the RUL^- algorithm is sound and complete for the DC-checking problem for STNUs.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9773Extending Conditional Simple Temporal Networks with Partially Shrinkable Uncertainty
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9774
The proper handling of temporal constraints is crucial in many domains. As a particular challenge, temporal constraints must be also handled when different specific situations happen (conditional constraints) and when some event occurrences can be only observed at run time (contingent constraints). In this paper we introduce Conditional Simple Temporal Networks with Partially Shrinkable Uncertainty (CSTNPSUs), in which contingent constraints are made more flexible (guarded constraints) and they are also specified as conditional constraints. It turns out that guarded constraints require the ability to reason on both kinds of constraints in a seamless way. In particular, we discuss CSTNPSU features through a motivating example and, then, we introduce the concept of controllability for such networks and the related sound checking algorithm.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9774On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9775
In 2005 T.K.S. Kumar studied the Restricted Disjunctive Temporal Problem (RDTP), a restricted but very expressive class of Disjunctive Temporal Problems (DTPs). An RDTP comes with a finite set of temporal variables, and a finite set of temporal constraints each of which can be either one of the following three types: (t_1) two-variable linear-difference simple constraint; (t_2) single-variable disjunction of many interval constraints; (t_3) two-variable disjunction of two interval constraints only. Kumar showed that RDTPs are solvable in deterministic strongly polynomial time by reducing them to the Connected Row-Convex (CRC) constraints satisfaction problem, also devising a faster randomized algorithm. Instead, the most general form of DTPs allows for multi-variable disjunctions of many interval constraints and it is NP-complete.This work offers a deeper comprehension on the tractability of RDTPs, leading to an elementary deterministic strongly polynomial time algorithm for them, significantly improving the asymptotic running times of all the previous deterministic and randomized solutions. The result is obtained by reducing RDTPs to the Single-Source Shortest Paths (SSSP) and the 2-SAT problem (jointly), instead of reducing to CRCs. In passing, we obtain a faster (quadratic time) algorithm for RDTPs having only {t_1, t_2}-constraints and no t_3-constraint. As a second main contribution, we study the tractability frontier of solving RDTPs blended with Hyper Temporal Networks (HyTNs), a disjunctive strict generalization of Simple Temporal Networks (STNs) based on hypergraphs: we prove that solving temporal problems having only t_2-constraints and either only multi-tail or only multi-head hyperarc-constraints lies in NP cap co-NP and admits deterministic pseudo-polynomial time algorithms; on the other hand, problems having only t_3-constraints and either only multi-tail or only multi-head hyperarc-constraints turns out strongly NP-complete.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9775Algebraic Operators for Processing Sets of Temporal Intervals in Relational Databases
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9776
The efficient management of temporal data has become increasingly important for many database applications. Most commercial systems already allow the management of temporal data but the operational support for processing this data is still rather limited. One particular reason is that many extension proposals typically require considerable modifications of the underlying database engine. In this paper, we propose a lightweight solution where temporal operators are realized using a library of user-defined functions. This way the complexity of temporal queries can be drastically reduced leading to more readable and less error-prone code without touching the database system. Our experiments show that the proposed operators significantly outperform temporal queries formulated in pure SQL. In addition, we investigate the possibility to incorporate algebraic optimization strategies directly into our operator definitions which allow for further performance improvements.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9776Deciding the Consistency of Branching Time Interval Networks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9777
Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9777A Game-Theoretic Approach to Timeline-Based Planning with Uncertainty
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9778
In timeline-based planning, domains are described as sets of independent, but interacting, components, whose behaviour over time (the set of timelines) is governed by a set of temporal constraints. A distinguishing feature of timeline-based planning systems is the ability to integrate planning with execution by synthesising control strategies for flexible plans. However, flexible plans can only represent temporal uncertainty, while more complex forms of nondeterminism are needed to deal with a wider range of realistic problems. In this paper, we propose a novel game-theoretic approach to timeline-based planning problems, generalising the state of the art while uniformly handling temporal uncertainty and nondeterminism. We define a general concept of timeline-based game and we show that the notion of winning strategy for these games is strictly more general than that of control strategy for dynamically controllable flexible plans. Moreover, we show that the problem of establishing the existence of such winning strategies is decidable using a doubly exponential amount of space.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9778Sound-and-Complete Algorithms for Checking the Dynamic Controllability of Conditional Simple Temporal Networks with Uncertainty
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9779
A Conditional Simple Temporal Network with Uncertainty (CSTNU) is a data structure for representing and reasoning about time. CSTNUs incorporate observation time-points from Conditional Simple Temporal Networks (CSTNs) and contingent links from Simple Temporal Networks with Uncertainty (STNUs). A CSTNU is dynamically controllable (DC) if there exists a strategy for executing its time-points that guarantees the satisfaction of all relevant constraints no matter how the uncertainty associated with its observation time-points and contingent links is resolved in real time. This paper presents the first sound-and-complete DC-checking algorithms for CSTNUs that are based on the propagation of labeled constraints and demonstrates their practicality.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9779Reducing epsilon-DC Checking for Conditional Simple Temporal Networks to DC Checking
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9780
Recent work on Conditional Simple Temporal Networks (CSTNs) has introduced the problem of checking the dynamic consistency (DC) property for the case where the reaction time of an execution strategy to observations is bounded below by some fixed epsilon > 0, the so-called epsilon-DC-checking problem. This paper proves that the epsilon-DC-checking problem for CSTNs can be reduced to the standard DC-checking problem for CSTNs - without incurring any computational cost. Given any CSTN S with k observation time-points, the paper defines a new CSTN S_0 that is the same as S, except that for each observation time-point P? in S: (i) P? is demoted to a non-observation time-point in S_0; and (ii) a new observation time-point P_0?, constrained to occur exactly epsilon units after P?, is inserted into S_0. The paper proves that S is epsilon-DC if and only if S_0 is (standard) DC, and that the application of the epsilon-DC-checking constraint-propagation rules to S is equivalent to the application of the corresponding (standard) DC-checking constraint-propagation rules to S_0. Two versions of these results are presented that differ only in whether a dynamic strategy for S_0 can react instantaneously to observations, or only after some arbitrarily small, positive delay. Finally, the paper demonstrates empirically that building S_0 and DC-checking it incurs no computational cost as the sizes of the instances increase.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9780On the Expressive Power of Hybrid Branching-Time Logics
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9781
Hybrid branching-time logics are a powerful extension of branching-time logics like CTL, CTL^* or even the modal mu-calculus through the addition of binders, jumps and variable tests. Their expressiveness is not restricted by bisimulation-invariance anymore. Hence, they do not retain the tree model property, and the finite model property is equally lost. Their satisfiability problems are typically undecidable, their model checking problems (on finite models) are decidable with complexities ranging from polynomial to non-elementary time. In this paper we study the expressive power of such hybrid branching-time logics beyond some earlier results about their invariance under hybrid bisimulations. In particular, we aim to extend the hierarchy of non-hybrid branching-time logics CTL, CTL^+, CTL^* and the modal mu-calculus to their hybrid extensions. We show that most separation results can be transferred to the hybrid world, even though the required techniques become a bit more involved. We also present some collapse results for restricted classes of models that are especially worth investigating, namely linear, tree-shaped and finite models.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9781A Temporal Logic for Modelling Activities of Daily Living
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9782
Behaviour support technology is aimed at assisting people in organizing their Activities of Daily Living (ADLs). Numerous frameworks have been developed for activity recognition and for generating specific types of support actions, such as reminders. The main goal of our research is to develop a generic formal framework for representing and reasoning about ADLs and their temporal relations. This framework should facilitate modelling and reasoning about 1) durative activities, 2) relations between higher-level activities and subactivities, 3) activity instances, and 4) activity duration. In this paper we present a temporal logic as an extension of the logic TPTL for specification of real-time systems. Our logic TPTL_{bih} is defined over Behaviour Identification Hierarchies (BIHs) for representing ADL structure and typical activity duration. To model execution of ADLs, states of the temporal traces in TPTL_{bih} comprise information about the start, stop and current execution of activities. We provide a number of constraints on these traces that we stipulate are desired for the accurate representation of ADL execution, and investigate corresponding validities in the logic. To evaluate the expressivity of the logic, we give a formal definition for the notion of Coherence for (complex) activities, by which we mean that an activity is done without interruption and in a timely fashion. We show that the definition is satisfiable in our framework. In this way the logic forms the basis for a generic monitoring and reasoning framework for ADLs.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9782GSM+T: A Timed Artifact-Centric Process Model
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9783
We introduce an extension to the declarative and artifact-centric Guard Stage Milestone (GSM) process modeling language to represent temporal aspects (duration, deadlines, lower- and upper-bound constraints), define the correctness of executions of GSM processes with respect to temporal constraints, check controllability of processes, compute execution plans respecting temporal constraints, and provide a translation method allowing to execute controllable GSM+T processes on standard GSM Engines.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9783Learning Qualitative Constraint Networks
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9784
Temporal and spatial reasoning is a fundamental task in artificial intelligence and its related areas including scheduling, planning and Geographic Information Systems (GIS). In these applications, we often deal with incomplete and qualitative information. In this regard, the symbolic representation of time and space using Qualitative Constraint Networks (QCNs) is therefore substantial.We propose a new algorithm for learning a QCN from a non expert. The learning process includes different cases where querying the user is an essential task. Here, membership queries are asked in order to elicit temporal or spatial relationships between pairs of temporal or spatial entities. During this acquisition process, constraint propagation through Path Consistency (PC) is performed in order to reduce the number of membership queries needed to reach the target QCN. We use the learning theory machinery to prove some limits on learning path consistent QCNs from queries. The time performances of our algorithm have been experimentally evaluated using different scenarios.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9784A Stream Reasoning System for Maritime Monitoring
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9785
We present a stream reasoning system for monitoring vessel activity in large geographical areas. The system ingests a compressed vessel position stream, and performs online spatio-temporal link discovery to calculate proximity relations between vessels, and topological relations between vessel and static areas. Capitalizing on the discovered relations, a complex activity recognition engine, based on the Event Calculus, performs continuous pattern matching to detect various types of dangerous, suspicious and potentially illegal vessel activity. We evaluate the performance of the system by means of real datasets including kinematic messages from vessels, and demonstrate the effects of the highly efficient spatio-temporal link discovery on performance.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9785An Empirical Study on Bidirectional Recurrent Neural Networks for Human Motion Recognition
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9786
The deep recurrent neural networks (RNNs) and their associated gated neurons, such as Long Short-Term Memory (LSTM) have demonstrated a continued and growing success rates with researches in various sequential data processing applications, especially when applied to speech recognition and language modeling. Despite this, amongst current researches, there are limited studies on the deep RNNs architectures and their effects being applied to other application domains. In this paper, we evaluated the different strategies available to construct bidirectional recurrent neural networks (BRNNs) applying Gated Recurrent Units (GRUs), as well as investigating a reservoir computing RNNs, i.e., Echo state networks (ESN) and a few other conventional machine learning techniques for skeleton-based human motion recognition. The evaluation of tasks focuses on the generalization of different approaches by employing arbitrary untrained viewpoints, combined together with previously unseen subjects. Moreover, we extended the test by lowering the subsampling frame rates to examine the robustness of the algorithms being employed against the varying of movement speed.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9786Population Based Methods for Optimising Infinite Behaviours of Timed Automata
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9787
Timed automata are powerful models for the analysis of real time systems. The optimal infinite scheduling problem for double-priced timed automata is concerned with finding infinite runs of a system whose long term cost to reward ratio is minimal. Due to the state-space explosion occurring when discretising a timed automaton, exact computation of the optimal infinite ratio is infeasible. This paper describes the implementation and evaluation of ant colony optimisation for approximating the optimal schedule for a given double-priced timed automaton. The application of ant colony optimisation to the corner-point abstraction of the automaton proved generally less effective than a random method. The best found optimisation method was obtained by formulating the choice of time delays in a cycle of the automaton as a linear program and utilizing ant colony optimisation in order to determine a sequence of profitable discrete transitions comprising an infinite behaviour.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9787Computational Complexity of a Core Fragment of Halpern-Shoham Logic
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9788
Halpern-Shoham logic (HS) is a highly expressive interval temporal logic but the satisfiability problem of its formulas is undecidable. The main goal in the research area is to introduce fragments of the logic which are of low computational complexity and of expressive power high enough for practical applications. Recently introduced syntactical restrictions imposed on formulas and semantical constraints put on models gave rise to tractable HS fragments for which prototypical real-world applications have already been proposed. One of such fragments is obtained by forbidding diamond modal operators and limiting formulas to the core form, i.e., the Horn form with at most one literal in the antecedent. The fragment was known to be NL-hard and in P but no tight results were known. In the paper we prove its P-completeness in the case where punctual intervals are allowed and the timeline is dense.Importantly, the fragment is not referential, i.e., it does not allow us to express nominals (which label intervals) and satisfaction operators (which enables us to refer to intervals by their labels). We show that by adding nominals and satisfaction operators to the fragment we reach NP-completeness whenever the timeline is dense or the interpretation of modal operators is weakened (excluding the case when punctual intervals are disallowed and the timeline is discrete). Moreover, we prove that in the case of language containing nominals but not satisfaction operators, the fragment is still NP-complete over dense timelines.Wed, 26 Sep 2018 11:58:52 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9788OASIcs, Volume 63, WCET'18, Complete Volume
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9757
OASIcs, Volume 63, WCET'18, Complete VolumeWed, 26 Sep 2018 08:32:17 +0200http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9757