8,025 Works

Non-Blocking Doubly-Linked Lists with Good Amortized Complexity

Niloufar Shafiei
We present a new non-blocking doubly-linked list implementation for an asynchronous shared-memory system. It is the first such implementation for which an upper bound on amortized time complexity has been proved. In our implementation, operations access the list via cursors. Each cursor is located at an item in the list and is local to a process. In our implementation, cursors can be used to traverse and update the list, even as concurrent operations modify the...

Quantum Algorithms for Testing Properties of Distributions

Sergey Bravyi, Aram W. Harrow & Avinatan Hassidim
Suppose one has access to oracles generating samples from two unknown probability distributions $p$ and $q$ on some $N$-element set. How many samples does one need to test whether the two distributions are close or far from each other in the $L_1$-norm? This and related questions have been extensively studied during the last years in the field of property testing. In the present paper we study quantum algorithms for testing properties of distributions. It is...

Reordering Derivatives of Trace Closures of Regular Languages

Hendrik Maarand & Tarmo Uustalu
We provide syntactic derivative-like operations, defined by recursion on regular expressions, in the styles of both Brzozowski and Antimirov, for trace closures of regular languages. Just as the Brzozowski and Antimirov derivative operations for regular languages, these syntactic reordering derivative operations yield deterministic and nondeterministic automata respectively. But trace closures of regular languages are in general not regular, hence these automata cannot generally be finite. Still, as we show, for star-connected expressions, the Antimirov and...

Kleene Algebra with Observations

Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker & Fabio Zanasi
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model...

A Sound Algorithm for Asynchronous Session Subtyping

Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida & Gianluigi Zavattaro
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behavior but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with...

Domain-Aware Session Types

Luís Caires, Jorge A. Pérez, Frank Pfenning & Bernardo Toninho
We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global...

Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum

Ulrich Dorsch, Stefan Milius & Lutz Schröder
State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time - branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the...

Game-Based Local Model Checking for the Coalgebraic mu-Calculus

Daniel Hausmann & Lutz Schröder
The coalgebraic mu-calculus is a generic framework for fixpoint logics with varying branching types that subsumes, besides the standard relational mu-calculus, such diverse logics as the graded mu-calculus, the monotone mu-calculus, the probabilistic mu-calculus, and the alternating-time mu-calculus. In the present work, we give a local model checking algorithm for the coalgebraic mu-calculus using a coalgebraic variant of parity games that runs, under mild assumptions on the complexity of the so-called one-step satisfaction problem, in...

Bialgebraic Semantics for String Diagrams

Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski & Fabio Zanasi
Turi and Plotkin's bialgebraic semantics is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (an endofunctor). This setup is instrumental in showing that a semantic specification (a coalgebra) satisfies desirable properties: in particular, that it is compositional. In this work, we use the bialgebraic approach to derive well-behaved structural operational semantics of string diagrams, a graphical...

Reconfiguration and Message Losses in Parameterized Broadcast Networks

Nathalie Bertrand, Patricia Bouyer & Anirban Majumdar
Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability problem which dually asks whether there exists an execution that visits a configuration exhibiting some given state of the broadcast protocol. Coverability is known to be undecidable for static networks, i.e. when the...

Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries

Nathalie Bertrand, Igor Konnov, Marijana Lazic & Josef Widder
Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it...

A Sound Foundation for the Topological Approach to Task Solvability

Jérémy Ledent & Samuel Mimram
The area of fault-tolerant distributed computability is concerned with the solvability of decision tasks in various computational models where the processes might crash. A very successful approach to prove impossibility results in this context is that of combinatorial topology, started by Herlihy and Shavit's paper in 1999. They proved that, for wait-free protocols where the processes communicate through read/write registers, a task is solvable if and only if there exists some map between simplicial complexes...

Robustness Against Transactional Causal Consistency

Sidi Mohamed Beillahi, Ahmed Bouajjani & Constantin Enea
Distributed storage systems and databases are widely used by various types of applications. Transactional access to these storage systems is an important abstraction allowing application programmers to consider blocks of actions (i.e., transactions) as executing atomically. For performance reasons, the consistency models implemented by modern databases are weaker than the standard serializability model, which corresponds to the atomicity abstraction of transactions executing over a sequentially consistent memory. Causal consistency for instance is one such model...

Expressive Power of Broadcast Consensus Protocols

Michael Blondin, Javier Esparza & Stefan Jaax
Population protocols are a formal model of computation by identical, anonymous mobile agents interacting in pairs. Their computational power is rather limited: Angluin et al. have shown that they can only compute the predicates over N^k expressible in Presburger arithmetic. For this reason, several extensions of the model have been proposed, including the addition of devices called cover-time services, absence detectors, and clocks. All these extensions increase the expressive power to the class of predicates...

Reasoning About Distributed Knowledge of Groups with Infinitely Many Agents

Michell Guzmán, Sophia Knight, Santiago Quintero, Sergio Ramírez, Camilo Rueda & Frank Valencia
Spatial constraint systems (scs) are semantic structures for reasoning about spatial and epistemic information in concurrent systems. We develop the theory of scs to reason about the distributed information of potentially infinite groups. We characterize the notion of distributed information of a group of agents as the infimum of the set of join-preserving functions that represent the spaces of the agents in the group. We provide an alternative characterization of this notion as the greatest...

Long-Run Average Behavior of Vector Addition Systems with States

Krishnendu Chatterjee, Thomas A. Henzinger & Jan Otop
A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state,...

Reachability for Bounded Branching VASS

Filip Mazowiecki & Michal Pilipczuk
In this paper we consider the reachability problem for bounded branching VASS. Bounded VASS are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. This model gained a lot of attention in 2012 when Haase et al. showed its connections with timed automata. Later in 2013 Fearnley and Jurdzinski proved that the reachability problem in this model...

Translating Asynchronous Games for Distributed Synthesis

Raven Beutner, Bernd Finkbeiner & Jesko Hecking-Harbusch
In distributed synthesis, a set of process implementations is generated, which together, accomplish an objective against all possible behaviors of the environment. A lot of recent work has focussed on systems with causal memory, i.e., sets of asynchronous processes that exchange their causal histories upon synchronization. Decidability results for this problem have been stated either in terms of control games, which extend Zielonka's asynchronous automata by partitioning the actions into controllable and uncontrollable, or in...

Synthesis of Data Word Transducers

Léo Exibard, Emmanuel Filiot & Pierre-Alain Reynier
In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals (omega-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite. In this paper, we consider data omega-words instead, i.e., words over an infinite alphabet. In this context,...

Register-Bounded Synthesis

Ayrat Khalimov & Orna Kupferman
Traditional synthesis algorithms return, given a specification over finite sets of input and output Boolean variables, a finite-state transducer all whose computations satisfy the specification. Many real-life systems have an infinite state space. In particular, behaviors of systems with a finite control yet variables that range over infinite domains, are specified by automata with infinite alphabets. A register automaton has a finite set of registers, and its transitions are based on a comparison of the...

Equilibrium Design for Concurrent Games

Julian Gutierrez, Muhammad Najib, Giuseppe Perelli & Michael Wooldridge
In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we study the design of incentives so that a desirable equilibrium is obtained, for instance, an equilibrium satisfying a given temporal logic property - a problem that we call equilibrium design. We base our study on a framework where system specifications are represented as temporal logic formulae, games as...

Partial Order Reduction for Reachability Games

Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz & Jirí Srba
Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability/safety objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on...

Energy Mean-Payoff Games

Véronique Bruyère, Quentin Hautem, Mickael Randour & Jean-François Raskin
In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the...

Good for Games Automata: From Nondeterminism to Alternation

Udi Boker & Karoliina Lehtinen
A word automaton recognizing a language L is good for games (GFG) if its composition with any game with winning condition L preserves the game's winner. While all deterministic automata are GFG, some nondeterministic automata are not. There are various other properties that are used in the literature for defining that a nondeterministic automaton is GFG, including "history-deterministic", "compliant with some letter game", "good for trees", and "good for composition with other automata". The equivalence...

Determinacy in Discrete-Bidding Infinite-Duration Games

Milad Aghajohari, Guy Avni & Thomas A. Henzinger
In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the...

Registration Year

  • 2009
  • 2010
  • 2011
  • 2012
  • 2013
  • 2014
  • 2015
  • 2016
  • 2017
  • 2018
  • 2019

Resource Types

  • Text

Data Centers

  • Dagstuhl