Automata, Languages, and Programming

Two key results of Robertson and Seymour’s graph minor theory are:

1.

a structure theorem stating that all graphs excluding some fixed graph as a minor have a tree decomposition into pieces that are almost embeddable in a fixed surface.

2.

the

k-disjoint paths problem

is tractable when

$$k$$

is a fixed constant: given a graph

$$G$$

and

$$k$$

pairs

$$(s_1,t_1)$$

, ...,

$$(s_k,t_k)$$

of vertices of

$$G$$

, decide whether there are

$$k$$

mutually vertex disjoint paths of

$$G$$

, the

$$i$$

th path linking

$$s_i$$

and

$$t_i$$

for

$$i=1,\dots ,k$$

.

In this talk, we shall try to look at the corresponding problems for digraphs.

Concerning the first point, the grid theorem, originally proved in 1986 by Robertson and Seymour in Graph Minors V, is the basis (even for the whole graph minor project). In the mid-90s, Reed and Johnson, Robertson, Seymour and Thomas (see [

13

,

26

]), independently, conjectured an analogous theorem for directed graphs, i.e. the existence of a function

$$f\mathrel : {\mathbb {N}} \rightarrow {\mathbb {N}}$$

such that every digraph of directed treewidth at least

$$f(k)$$

contains a directed grid of order

$$k$$

. In an unpublished manuscript from 2001, Johnson, Robertson, Seymour and Thomas give a proof of this conjecture for planar digraphs. But for over a decade, this was the most general case proved for the conjecture.

We are finally able to confirm the Reed, Johnson, Robertson, Seymour and Thomas conjecture in full generality. As a consequence of our results we are able to improve results in Reed et al. in 1996 [

27

] to disjoint cycles of length at least

$$l$$

. This would be the first but a significant step toward the structural goals for digraphs (hence towards the first point).

Concerning the second point, in [

19

] we contribute to the disjoint paths problem using the directed grid theorem. We show that the following can be done in polynomial time:

Suppose that we are given a digraph

$$G$$

and

$$k$$

terminal pairs

$$(s_1, t_1), (s_2, t_2), \dots , (s_k, t_k)$$

, where

$$k$$

is a fixed constant. In polynomial time, either

we can find

$$k$$

paths

$$P_1, \dots , P_k$$

such that

$$P_i$$

is from

$$s_i$$

to

$$t_i$$

for

$$i=1, \dots , k$$

and every vertex in

$$G$$

is in at most four of the paths, or

we can conclude that

$$G$$

does not contain disjoint paths

$$P_1, \dots , P_k$$

such that

$$P_i$$

is from

$$s_i$$

to

$$t_i$$

for

$$i=1, \dots , k$$

.

To the best of our knowledge, this is the first positive result for the general directed disjoint paths problem (and hence for the second point). Note that the directed disjoint paths problem is NP-hard even for

$$k=2$$

. Therefore, this kind of results is the best one can hope for.

We also report some progress on the above two points.

Synthesis is a particularly challenging problem for concurrent programs. At the same time it is a very promising approach, since concurrent programs are difficult to get right, or to analyze with traditional verification techniques. This paper gives an introduction to distributed synthesis in the setting of Mazurkiewicz traces, and its applications to decentralized runtime monitoring.

We present a game semantics for dependent type theory (DTT) with

$$\varPi $$

-,

$$\varSigma $$

-, intensional

$$\mathsf {Id}$$

-types and finite inductive type families. The model satisfies Streicher’s criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied.

The model is fully and faithfully complete at the type hierarchy built without

$$\mathsf {Id}$$

-types. Although definability for the hierarchy with

$$\mathsf {Id}$$

-types remains to be investigated, the notions of propositional equality in syntax and semantics do coincide for (open) terms of the

$$\mathsf {Id}$$

-free type hierarchy.

We prove that the propositional translations of the Kneser-Lovász theorem have polynomial size extended Frege proofs and quasi-polynomial size Frege proofs. We present a new counting-based combinatorial proof of the Kneser-Lovász theorem that avoids the topological arguments of prior proofs for all but finitely many cases for each

k

. We introduce a miniaturization of the octahedral Tucker lemma, called the

truncated Tucker lemma

: it is open whether its propositional translations have (quasi-)polynomial size Frege or extended Frege proofs.

Query evaluation in monadic second-order logic (MSO) is tractable on trees and treelike instances, even though it is hard for arbitrary instances. This tractability result has been extended to several tasks related to query evaluation, such as counting query results [

2

] or performing query evaluation on probabilistic trees [

8

]. These are two examples of the more general problem of computing augmented query output, that is referred to as

provenance

. This article presents a provenance framework for trees and treelike instances, by describing a linear-time construction of a circuit provenance representation for MSO queries. We show how this provenance can be connected to the usual definitions of semiring provenance on relational instances [

17

], even though we compute it in an unusual way, using tree automata; we do so via intrinsic definitions of provenance for general semirings, independent of the operational details of query evaluation. We show applications of this provenance to capture existing counting and probabilistic results on trees and treelike instances, and give novel consequences for probability evaluation.

Parametric timed automata extend the standard timed automata with the possibility to use parameters in the clock guards. In general, if the parameters are real-valued, the problem of language emptiness of such automata is undecidable even for various restricted subclasses. We thus focus on the case where parameters are assumed to be integer-valued, while the time still remains continuous. On the one hand, we show that the problem remains undecidable for parametric timed automata with three clocks and one parameter. On the other hand, for the case with arbitrary many clocks where only one of these clocks is compared with (an arbitrary number of) parameters, we show that the parametric language emptiness is decidable. The undecidability result tightens the bounds of a previous result which assumed six parameters, while the decidability result extends the existing approaches that deal with discrete-time semantics only. To the best of our knowledge, this is the first positive result in the case of continuous-time and unbounded integer parameters, except for the rather simple case of single-clock automata.

We investigate the use of generating functions in the analysis of discrete Markov chains. Generating functions are introduced as power series whose coefficients are certain hitting probabilities. Being able to compute such functions implies that the calculation of a number of quantities of interest, including absorption probabilities, expected hitting time and number of visits, and variances thereof, becomes straightforward. We show that it is often possible to recover this information, either exactly or within excellent approximation, via the construction of Padé approximations of the involved generating function. The presented algorithms are based on projective methods from linear algebra, which can be made to work with limited computational resources. In particular, only a black-box, on-the-fly access to the transition function is presupposed, and the necessity of storing the whole model is eliminated. A few numerical experiments conducted with this technique give encouraging results.

Efficient implementations of atomic objects such as concurrent stacks and queues are especially susceptible to programming errors, and necessitate automatic verification. Unfortunately their correctness criteria — linearizability with respect to given ADT specifications — are hard to verify. Even on classes of implementations where the usual temporal safety properties like control-state reachability are decidable, linearizability is undecidable.

In this work we demonstrate that verifying linearizability for certain

fixed

ADT specifications is reducible to control-state reachability, despite being harder for

arbitrary

ADTs. We effectuate this reduction for several of the most popular atomic objects. This reduction yields the first decidability results for verification without bounding the number of concurrent threads. Furthermore, it enables the application of existing safety-verification tools to linearizability verification.

The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is “constructed from scratch” rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced

dataflow

and

controlflow

synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of

probabilistic components

was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability 1). Our main contribution for controlflow synthesis from probabilistic components is to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i) is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii) belongs to UP

$$\cap $$

coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound.

The edit distance between two words

$$w_1, w_2$$

is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform

$$w_1$$

to

$$w_2$$

. The edit distance generalizes to languages

$$\mathcal {L}_1, \mathcal {L}_2$$

, where the edit distance is the minimal number

k

such that for every word from

$$\mathcal {L}_1$$

there exists a word in

$$\mathcal {L}_2$$

with edit distance at most

k

. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold

k

, the edit distance from a pushdown automaton to a finite automaton is at most

k

.

We show that, given a word equation over a finitely generated free group, the set of all solutions in reduced words forms an EDT0L language. In particular, it is an indexed language in the sense of Aho. The question of whether a description of solution sets in reduced words as an indexed language is possible has been open for some years [

9

,

10

], apparently without much hope that a positive answer could hold. Nevertheless, our answer goes far beyond: they are EDT0L, which is a proper subclass of indexed languages. We can additionally handle the existential theory of equations with rational constraints in free products

$$\star _{1 \le i \le s}F_i$$

, where each

$$F_i$$

is either a free or finite group, or a free monoid with involution. In all cases the result is the same: the set of all solutions in reduced words is EDT0L. This was known only for quadratic word equations by [

8

], which is a very restricted case. Our general result became possible due to the recent recompression technique of Jeż. In this paper we use a new method to integrate solutions of linear Diophantine equations into the process and obtain more general results than in the related paper [

5

]. For example, we improve the complexity from quadratic nondeterministic space in [

5

] to quasi-linear nondeterministic space here. This implies an improved complexity for deciding the existential theory of non-abelian free groups:

$$\mathsf {NSPACE}(n\log n$$

). The conjectured complexity is

$$\mathsf {NP}$$

, however, we believe that our results are optimal with respect to space complexity, independent of the conjectured

$$\mathsf {NP}$$

.

In this paper, we study several sublogics of monadic second-order logic over countable linear orderings, such as first-order logic, first-order logic on cuts, weak monadic second-order logic, weak monadic second-order logic with cuts, as well as fragments of monadic second-order logic in which sets have to be well ordered or scattered. We give decidable algebraic characterizations of all these logics and compare their respective expressive power.

We consider the

dynamic complexity

of some central graph problems such as Reachability and Matching and linear algebraic problems such as Rank and Inverse. As elementary change operations we allow insertion and deletion of edges of a graph and the modification of a single entry in a matrix, and we are interested in the complexity of maintaining a property or query. Our main results are as follows:

1.

Reachability is in

DynFO

;

2.

Rank of a matrix is in

DynFO

$${(+,\!\times \!)}$$

;

3.

Maximum Matching (decision) is in non-uniform

DynFO

.

Here,

DynFO

allows updates of the auxiliary data structure defined in first-order logic,

DynFO

$${(+,\!\times \!)}$$

additionally has arithmetics at initialization time and non-uniform

DynFO

allows arbitrary auxiliary data at initialization time. Alternatively,

DynFO

$${(+,\!\times \!)}$$

and non-uniform

DynFO

allow updates by uniform and non-uniform families of poly-size, bounded-depth circuits, respectively.

The first result confirms a two decade old conjecture of Patnaik and Immerman [

16

]. The proofs rely mainly on elementary Linear Algebra. The second result can also be concluded from [

7

].

We propose a notion of homology for directed algebraic topology, based on so-called natural systems of abelian groups, and which we call natural homology. As we show, natural homology has many desirable properties: it is invariant under isomorphisms of directed spaces, it is invariant under refinement (subdivision), and it is computable on cubical complexes.

We give polynomial time algorithms for quantitative (and qualitative)

reachability

analysis for

Branching Markov Decision Processes

(BMDPs). Specifically, given a BMDP, and given an initial population, where the objective of the controller is to maximize (or minimize) the probability of eventually reaching a population that contains an object of a desired (or undesired) type, we give algorithms for approximating the supremum (infimum) reachability probability, within desired precision

$$\epsilon > 0$$

, in time polynomial in the encoding size of the BMDP and in

$$\log (1/\epsilon )$$

. We furthermore give P-time algorithms for computing

$$\epsilon $$

-optimal strategies for both maximization and minimization of reachability probabilities. We also give P-time algorithms for all associated

qualitative

analysis problems, namely: deciding whether the optimal (supremum or infimum) reachability probabilities are 0 or 1. Prior to this paper, approximation of optimal reachability probabilities for BMDPs was not even known to be decidable.

Our algorithms exploit the following basic fact: we show that for any BMDP, its maximum (minimum)

non

-reachability probabilities are given by the

greatest fixed point

(GFP) solution

$$g^* \in [0,1]^n$$

of a corresponding monotone max (min) Probabilistic Polynomial System of equations (max/min-PPS),

$$x=P(x)$$

, which are the Bellman optimality equations for a BMDP with non-reachability objectives. We show how to compute the GFP of max/min PPSs to desired precision in P-time.

We study two-player games with counters, where the objective of the first player is that the counter values remain bounded. We investigate the existence of a trade-off between the size of the memory and the bound achieved on the counters, which has been conjectured by Colcombet and Löding. We show that unfortunately this conjecture does not hold: there is no trade-off between bounds and memory, even for finite arenas. On the positive side, we prove the existence of a trade-off for the special case of thin tree arenas.

A tree transducer with origin translates an input tree into a pair of output tree and origin info. The origin info maps each node in the output tree to the unique input node that created it. In this way, the implementation of the transducer becomes part of its semantics. We show that the landscape of decidable properties changes drastically when origin info is added. For instance, equivalence of nondeterministic top-down and MSO transducers with origin is decidable. Both problems are undecidable without origin. The equivalence of deterministic top-down tree-to-string transducers is decidable with origin, while without origin it is a long standing open problem. With origin, we can decide if a deterministic macro tree transducer can be realized by a deterministic top-down tree transducer; without origin this is an open problem.

We prove that there exist some 1-counter Büchi automata

$$\mathcal {A}_n$$

for which some elementary properties are independent of theories like

$$T_n$$

=:

ZFC

+ “There exist (at least)

n

inaccessible cardinals", for integers

$$n\ge 1$$

. In particular, if

$$T_n$$

is consistent, then “

$$L(\mathcal {A}_n)$$

is Borel", “

$$L(\mathcal {A}_n)$$

is arithmetical", “

$$L(\mathcal {A}_n)$$

is

$$\omega $$

-regular", “

$$L(\mathcal {A}_n)$$

is deterministic", and “

$$L(\mathcal {A}_n)$$

is unambiguous" are provable from

ZFC

+ “There exist (at least)

$$n+1$$

inaccessible cardinals" but not from

ZFC

+ “There exist (at least)

n

inaccessible cardinals". We prove similar results for infinitary rational relations accepted by 2-tape Büchi automata.

Given Markov chains and Markov decision processes (MDPs) whose transitions are labelled with non-negative integer costs, we study the computational complexity of deciding whether the probability of paths whose accumulated cost satisfies a Boolean combination of inequalities exceeds a given threshold. For acyclic Markov chains, we show that this problem is PP-complete, whereas it is hard for the

PosSLP

problem and in

PSpace

for general Markov chains. Moreover, for acyclic and general MDPs, we prove

PSpace

- and

EXP

-completeness, respectively. Our results have direct implications on the complexity of computing reward quantiles in succinctly represented stochastic systems.

We address a fundamental issue of

interfaces

that arises in the context of cloud computing. We define what it means for a replicated and distributed implementation satisfy the standard sequential specification of the data structure. Several extant implementations of replicated data structures already satisfy the constraints of our definition. We describe how the algorithms discussed in a recent survey of convergent or commutative replicated datatypes [

17

] satisfy our definition. We show that our definition simplifies the programmer task significantly for a class of clients who conform to the CALM principle [

10

].

We generalise the hyperplane separation technique (Chatterjee and Velner, 2013) from multi-dimensional mean-payoff to energy games, and achieve an algorithm for solving the latter whose running time is exponential only in the dimension, but not in the number of vertices of the game graph. This answers an open question whether energy games with arbitrary initial credit can be solved in pseudo-polynomial time for fixed dimensions 3 or larger (Chaloupka, 2013). It also improves the complexity of solving multi-dimensional energy games with given initial credit from non-elementary (Brázdil, Jančar, and Kučera, 2010) to

2EXPTIME

, thus establishing their

2EXPTIME

-completeness.

We study multidimensional configurations (infinite words) and subshifts of low pattern complexity using tools of algebraic geometry. We express the configuration as a multivariate formal power series over integers and investigate the setup when there is a non-trivial annihilating polynomial: a non-zero polynomial whose formal product with the power series is zero. Such annihilator exists, for example, if the number of distinct patterns of some finite shape

D

in the configuration is at most the size |

D

| of the shape. This is our low pattern complexity assumption. We prove that the configuration must be a sum of periodic configurations over integers, possibly with unbounded values. As a specific application of the method we obtain an asymptotic version of the well-known Nivat’s conjecture: we prove that any two-dimensional, non-periodic configuration can satisfy the low pattern complexity assumption with respect to only finitely many distinct rectangular shapes

D

.

We develop the coalgebraic theory of nominal Kleene algebra, including an alternative language-theoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulation-based decision procedure for the equational theory.

In this work we study Good-For-Games (GFG) automata over

$$\omega $$

-words: non-deterministic automata where the non-determinism can be resolved by a strategy depending only on the prefix of the

$$\omega $$

-word read so far. These automata retain some advantages of determinism: they can be composed with games and trees in a sound way, and inclusion

$$\mathrm {L} (\mathcal {A})\supseteq \mathrm {L} (\mathcal {B})$$

can be reduced to a parity game over

$$\mathcal {A} \times \mathcal {B} $$

if

$$\mathcal {A} $$

is GFG. Therefore, they could be used to some advantage in verification, for instance as solutions to the synthesis problem.

The main results of this work answer the question whether parity GFG automata actually present an improvement in terms of state-complexity (the number of states) compared to the deterministic ones. We show that a frontier lies between the Büchi condition, where GFG automata can be determinised with only quadratic blow-up in state-complexity; and the co-Büchi condition, where GFG automata can be exponentially smaller than any deterministic automaton for the same language. We also study the complexity of deciding whether a given automaton is GFG.

We show that even in the absence of auxiliary variables, the well-known Owicki-Gries method for verifying concurrent programs is unsound for weak memory models. By strengthening its non-interference check, however, we obtain OGRA, a program logic that is sound for reasoning about programs in the release-acquire fragment of the C11 memory model. We demonstrate the usefulness of this logic by applying it to several challenging examples, ranging from small litmus tests to an implementation of the RCU synchronization primitives.

Does the trace language of a given vector addition system (VAS) intersect with a given context-free language? This question lies at the heart of several verification questions involving recursive programs with integer parameters. In particular, it is equivalent to the coverability problem for VAS that operate on a pushdown stack. We show decidability in dimension one, based on an analysis of a new model called grammar-controlled vector addition systems.

Straight-line (linear) context-free tree (

slt

) grammars have been used to compactly represent ordered trees. Equivalence of

slt

grammars is decidable in polynomial time. Here we extend this result and show that isomorphism of unordered trees given as

slt

grammars is decidable in polynomial time. The result generalizes to isomorphism of unrooted trees and bisimulation equivalence. For non-linear

slt

grammars which can have double-exponential compression ratios, we prove that unordered isomorphism and bisimulation equivalence are

$$\textsc {pspace}$$

-hard and in

$$\textsc {exptime}$$

.

We consider a non-uniform affine lambda-calculus, called parsimonious, and endow its terms with two type disciplines: simply-typed and with linear polymorphism. We show that the terms of string type into Boolean type characterize the class L/poly in the first case, and P/poly in the second. Moreover, we relate this characterization to that given by the second author in terms of Boolean proof nets, highlighting continuous affine approximations as the bridge between the two approaches to non-uniform computation.

We consider Rabin’s

Monadic Second Order

logic (MSO) of the full binary tree extended with Harvey Friedman’s “for almost all” second-order quantifier (

$$\forall ^*$$

) with semantics given in terms of Baire Category. In Theorem 1 we prove that the new quantifier can be eliminated (

$$\text {MSO}\!+\!\forall ^* \!=\! \text {MSO}$$

). We then apply this result to prove in Theorem 2 that the

finite–SAT

problem for the qualitative fragment of the probabilistic temporal logic pCTL* is decidable. This extends a previous result of Brázdil, Forejt, Křetínský and Kučera valid for qualitative pCTL.

We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or S-automata. Such specifications are very expressive (they strictly subsume

$$\omega $$

-regular specifications), and easily express complex liveness and safety properties. Our results are obtained by modeling the passage of time using symmetric broadcast, and by solving the model checking problem of parameterized systems of untimed processes communicating using

k

-wise rendezvous and symmetric broadcast. Our decidability proof makes use of automata theory, rational linear programming, and geometric reasoning for solving certain reachability questions in vector addition systems; we believe these proof techniques will be useful in solving related problems.

Symmetry is inherent in the definition of most of the two-player zero-sum games, including parity, mean-payoff, and discounted-payoff games. It is therefore quite surprising that no symmetric analysis techniques for these games exist. We develop a novel symmetric strategy improvement algorithm where, in each iteration, the strategies of both players are improved simultaneously. We show that symmetric strategy improvement defies Friedmann’s traps, which shook the belief in the potential of classic strategy improvement to be polynomial.

Non-locality and contextuality are among the most counterintuitive aspects of quantum theory. They are difficult to study using classical logic and probability theory. In this paper we start with an effect algebraic approach to the study of non-locality and contextuality. We will see how different slices over the category of set valued functors on the natural numbers induce different settings in which non-locality and contextuality can be studied. This includes the Bell, Hardy and Kochen-Specker-type paradoxes. We link this to earlier sheaf theoretic approaches by defining a fully faithful embedding of the category of effect algebras in this presheaf category over the natural numbers.

We apply a construction of Cook (1971) to show that the intersection non-emptiness problem for one PDA (pushdown automaton) and a finite list of DFA’s (deterministic finite automata) characterizes the complexity class P. In particular, we show that there exist constants

$$c_1$$

and

$$c_2$$

such that for every

k

, intersection non-emptiness for one PDA and

k

DFA’s is solvable in

$$O(n^{c_1 k})$$

time, but is not solvable in

$$O(n^{c_2 k})$$

time. Then, for every

k

, we reduce intersection non-emptiness for one PDA and

$$2^k$$

DFA’s to non-emptiness for multi-stack pushdown automata with

k

-phase switches to obtain a tight time complexity lower bound. Further, we revisit a construction of Veanes (1997) to show that the intersection non-emptiness problem for tree automata also characterizes the complexity class P. We show that there exist constants

$$c_1$$

and

$$c_2$$

such that for every

k

, intersection non-emptiness for

k

tree automata is solvable in

$$O(n^{c_1 k})$$

time, but is not solvable in

$$O(n^{c_2 k})$$

time.

Containment of monadic datalog programs over data trees (labelled trees with an equivalence relation) is undecidable. Recently, decidability was shown for two incomparable fragments: downward programs, which never move up from visited tree nodes, and linear child-only programs, which have at most one intensional predicate per rule and do not use descendant relation. As different as the fragments are, the decidability proofs hinted at an analogy. As it turns out, the common denominator is admitting bounded clique-width counter-examples to containment. This observation immediately leads to stronger decidability results with more elegant proofs, via decidability of monadic second order logic over structures of bounded clique-width. An argument based on two-way alternating tree automata gives a tighter upper bound for linear child-only programs, closing the complexity gap: the problem is

$$2\textsc {-ExpTime}$$

-complete. As a step towards these goals, complexity of containment over arbitrary structures of bounded clique-width is analysed: satisfiability and containment of monadic programs with stratified negation is in

$$3\textsc {-ExpTime}$$

, and containment of a linear monadic program in a monadic program is in

$$2\textsc {-ExpTime}$$

.

The downward closure of a word language is the set of all (not necessarily contiguous) subwords of its members. It is well-known that the downward closure of any language is regular. While the downward closure appears to be a powerful abstraction, algorithms for computing a finite automaton for the downward closure of a given language have been established only for few language classes.

This work presents a simple general method for computing downward closures. For language classes that are closed under rational transductions, it is shown that the computation of downward closures can be reduced to checking a certain unboundedness property.

This result is used to prove that downward closures are computable for (i) every language class with effectively semilinear Parikh images that are closed under rational transductions, (ii) matrix languages, and (iii) indexed languages (equivalently, languages accepted by higher-order pushdown automata of order 2).

Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent’s moves. For

$$\omega $$

-regular winning conditions it is known that such games can be solved in doubly-exponential time and that doubly-exponential lookahead is sufficient.

We improve upon both results by giving an exponential time algorithm and an exponential upper bound on the necessary lookahead. This is complemented by showing

$$\textsc {ExpTime}$$

-hardness of the solution problem and tight exponential lower bounds on the lookahead. Both lower bounds already hold for safety conditions. Furthermore, solving delay games with reachability conditions is shown to be

$$\textsc {PSpace}$$

-complete.

In the study of random structures we often face a trade-off between realism and tractability, the latter typically enabled by independence assumptions. In this work we initiate an effort to bridge this gap by developing tools that allow us to work with independence without assuming it. Let

$$\mathcal {G}_{n}$$

be the set of all graphs on

n

vertices and let

S

be an arbitrary subset of

$$\mathcal {G}_{n}$$

, e.g., the set of all graphs with

m

edges. The study of random networks can be seen as the study of properties that are true for

most

elements of

S

, i.e., that are true with high probability for a uniformly random element of

S

. With this in mind, we pursue the following question:

What are general sufficient conditions for the uniform measure on a set of graphs

$$S \subseteq \mathcal {G}_{n}$$

to be well-approximable by a product measure on the set of all possible edges?

Population protocols are networks of finite-state agents, interacting randomly, and updating their states using simple rules. Despite their extreme simplicity, these systems have been shown to cooperatively perform complex computational tasks, such as simulating register machines to compute standard arithmetic functions. The election of a unique

leader agent

is a key requirement in such computational constructions. Yet, the fastest currently known population protocol for electing a leader only has

linear

convergence time, and it has recently been shown that no population protocol using a

constant

number of states per node may overcome this linear bound.

In this paper, we give the first population protocol for leader election with

polylogarithmic

convergence time, using polylogarithmic memory states per node. The protocol structure is quite simple: each node has an associated value, and is either a

leader

(still in contention) or a

minion

(following some leader). A leader keeps incrementing its value and “defeats” other leaders in one-to-one interactions, and will drop from contention and become a minion if it meets a leader with higher value. Importantly, a leader also drops out if it meets a

minion

with higher absolute value. While these rules are quite simple, the proof that this algorithm achieves polylogarithmic convergence time is non-trivial. In particular, the argument combines careful use of concentration inequalities with anti-concentration bounds, showing that the leaders’ values become spread apart as the execution progresses, which in turn implies that straggling leaders get quickly eliminated. We complement our analysis with empirical results, showing that our protocol converges extremely fast, even for large network sizes.

Consider a preferential attachment model for network evolution that allows both node and edge arrival events: at time

t

, with probability

$$p_t$$

a new node arrives and a new edge is added between the new node and an existing node, and with probability

$$1-p_t$$

a new edge is added between two existing nodes. In both cases existing nodes are chosen at random according to preferential attachment, i.e., with probability proportional to their degree. For

$$\delta \in (0,1)$$

, the

$$\delta $$

-founders

of the network at time

t

is the minimal set of the first nodes to enter the network (i.e., founders) guaranteeing that the sum of degrees of nodes in the set is at least a

$$\delta $$

fraction of the number of edges in the graph at time

t

. We show that for the common model where

$$p_t$$

is constant, i.e., when

$$p_t=p$$

for every

t

and the network is sparse with linear number of edges, the size of the

$$\delta $$

-founders set is concentrated around

$$\delta ^{2/p} n_t$$

, and thus is linear in

$$n_t$$

, the number of nodes at time

t

. In contrast, we show that for

$$p_t=\min \{1,\frac{2a}{\ln t}\}$$

and when the network is dense with super-linear number of edges, the size of the

$$\delta $$

-founders set is sub-linear in

$$n_t$$

and concentrated around

$$\tilde{\Theta }((n_t)^{\eta })$$

, where

$$\eta =\delta ^{1/a}$$

.

We study dynamic matching problems in graphs among agents with preferences. Agents and/or edges of the graph arrive and depart iteratively over time. The goal is to maintain matchings that are favorable to the agent population and stable over time. More formally, we strive to keep a small unpopularity factor by making only a small amortized number of changes to the matching per round. Our main result is an algorithm to maintain matchings with unpopularity factor

$$(\Delta +k)$$

by making an amortized number of

$$O(\Delta + \Delta ^2/k)$$

changes per round, for any

$$k > 0$$

. Here

$$\Delta $$

denotes the maximum degree of any agent in any round. We complement this result by a variety of lower bounds indicating that matchings with smaller factor do not exist or cannot be maintained using our algorithm.

As a byproduct, we obtain several additional results that might be of independent interest. First, our algorithm implies existence of matchings with small unpopularity factors in graphs with bounded degree. Second, given any matching

M

and any value

$$\alpha \ge 1$$

, we provide an efficient algorithm to compute a matching

$$M'$$

with unpopularity factor

$$\alpha $$

over

M

if it exists. Finally, our results show the absence of voting paths in two-sided instances, even if we restrict to sequences of matchings with larger unpopularity factors (below

$$\Delta )$$

.

The performance of large distributed systems crucially depends on efficiently balancing their load. This has motivated a large amount of theoretical research how an imbalanced load vector can be smoothed with local algorithms. For technical reasons, the vast majority of previous work focuses on regular (or almost regular) graphs including symmetric topologies such as grids and hypercubes, and ignores the fact that large networks are often highly heterogenous.

We model large scale-free networks by Chung-Lu random graphs and analyze a simple local algorithm for iterative load balancing. On

n

-node graphs our distributed algorithm balances the load within

$$\mathcal {O}((\log \log n)^2)$$

steps. It does not need to know the exponent

$$\beta \in (2,3)$$

of the power-law degree distribution or the weights

$$w_i$$

of the graph model. To the best of our knowledge, this is the first result which shows that load-balancing can be done in double-logarithmic time on realistic graph classes.

We investigate the approximate consensus problem in highly dynamic networks in which topology may change continually and unpredictably. We prove that in both synchronous and partially synchronous networks, approximate consensus is solvable if and only if the communication graph in each round has a rooted spanning tree. Interestingly, the class of averaging algorithms, which have the benefit of being memoryless and requiring no process identifiers, entirely captures the solvability issue of approximate consensus in that the problem is solvable if and only if it can be solved using any averaging algorithm.

We develop a proof strategy which for each positive result consists in a reduction to the

nonsplit

networks. It dramatically improves the best known upper bound on the decision times of averaging algorithms and yields a quadratic time non-averaging algorithm for approximate consensus in non-anonymous networks. We also prove that a general upper bound on the decision times of averaging algorithms have to be exponential, shedding light on the price of anonymity.

Finally we apply our results to networked systems with a fixed topology and benign fault models to show that with

n

processes, up to

$$2n-3$$

of link faults per round can be tolerated for approximate consensus, increasing by a factor 2 the bound of Santoro and Widmayer for exact consensus.

We continue the study of communication cost of computing functions when inputs are distributed among

k

processors, each of which is located at one vertex of a network/graph called a terminal. Every other node of the network also has a processor, with no input. The communication is point-to-point and the cost is the total number of bits exchanged by the protocol, in the worst case, on all edges.

Chattopadhyay, Radhakrishnan and Rudra (FOCS’14) recently initiated the study of the effect of topology of the network on the total communication cost using tools from

$$L_1$$

embeddings. Their techniques provided tight bounds for simple functions like Element-Distinctness (ED), which depend on the 1-median of the graph. This work addresses two other kinds of natural functions. We show that for a large class of natural functions like Set-Disjointness the communication cost is essentially

n

times the cost of the optimal Steiner tree connecting the terminals. Further, we show for natural composed functions like

$$\text {ED} \circ \text {XOR}$$

and

$$\text {XOR} \circ \text {ED}$$

, the naive protocols suggested by their definition is optimal for general networks. Interestingly, the bounds for these functions depend on more involved topological parameters that are a combination of Steiner tree and 1-median costs.

To obtain our results, we use some new tools in addition to ones used in Chattopadhyay et al. These include (i) viewing the communication constraints via a linear program; (ii) using tools from the theory of tree embeddings to prove topology sensitive direct sum results that handle the case of composed functions and (iii) representing the communication constraints of certain problems as a family of collection of multiway cuts, where each multiway cut simulates the hardness of computing the function on the star topology.

The secretary model is a popular framework for the analysis of online admission problems beyond the worst case. In many markets, however, decisions about admission have to be made in a decentralized fashion and under competition. We cope with this problem and design algorithms for secretary markets with limited information. In our basic model, there are

m

firms and each has a job to offer.

n

applicants arrive iteratively in random order. Upon arrival of an applicant, a value for each job is revealed. Each firm decides whether or not to offer its job to the current applicant without knowing the strategies, actions, or values of other firms. Applicants decide to accept their most preferred offer.

We consider the social welfare of the matching and design a decentralized randomized thresholding-based algorithm with ratio

$$O(\log n)$$

that works in a very general sampling model. It can even be used by firms hiring several applicants based on a local matroid. In contrast, even in the basic model we show a lower bound of

$$\Omega (\log n/(\log \log n))$$

for all thresholding-based algorithms. Moreover, we provide secretary algorithms with constant competitive ratios, e.g., when values of applicants for different firms are stochastically independent. In this case, we can show a constant ratio even when each firm offers several different jobs, and even with respect to its individually optimal assignment. We also analyze several variants with stochastic correlation among applicant values.

We present a

$$\lg n + 2 \lg \lg n+3$$

ancestry labeling scheme for trees. The problem was first presented by Kannan et al. [STOC 88’] along with a simple

$$2 \lg n$$

solution. Motivated by applications to XML files, the label size was improved incrementally over the course of more than 20 years by a series of papers. The last, due to Fraigniaud and Korman [STOC 10’], presented an asymptotically optimal

$$\lg n + 4 \lg \lg n+O(1)$$

labeling scheme using non-trivial tree-decomposition techniques. By providing a framework generalizing interval based labeling schemes, we obtain a simple, yet asymptotically optimal solution to the problem. Furthermore, our labeling scheme is attained by a small modification of the original

$$2 \lg n$$

solution.

Alice and Bob want to run a protocol over an noisy channel, where a certain number of bits are flipped adversarially. Several results take a protocol requiring

L

bits of noise-free communication and make it robust over such a channel. In a recent breakthrough result, Haeupler described an algorithm that sends a number of bits that is conjectured to be near optimal in such a model. However, his algorithm critically requires

a priori

knowledge of the number of bits that will be flipped by the adversary.

We describe an algorithm requiring no such knowledge. If an adversary flips

T

bits, our algorithm sends

$$L + O\left( (T+\sqrt{LT+L})\log (LT+L)\right) $$

bits in expectation and succeeds with high probability in

L

. It does so without any

a priori

knowledge of

T

. Assuming a conjectured lower bound by Haeupler, ourresult is optimal up to logarithmic factors.

Our algorithm critically relies on the assumption of a private channel. We show that privacy is necessary when the amount of noise is unknown.

We consider the

k

-Center

problem and some generalizations. For

k

-Center a set of

k

center vertices

needs to be found in a graph

G

with edge lengths, such that the distance from any vertex of

G

to its nearest center is minimized. This problem naturally occurs in transportation networks, and therefore we model the inputs as graphs with bounded

highway dimension

, as proposed by Abraham et al. [ICALP 2011].

We show both approximation and fixed-parameter hardness results, and how to overcome them using

fixed-parameter approximations

. In particular, we prove that for any

$${\varepsilon }>0$$

computing a

$$(2-{\varepsilon })$$

-approximation is W[2]-hard for parameter

k

, and NP-hard for graphs with highway dimension

$$O(\log ^2 n)$$

. The latter does not rule out fixed-parameter

$$(2-{\varepsilon })$$

-approximations for the highway dimension parameter

h

, but implies that such an algorithm must have at least doubly exponential running time in

h

if it exists, unless the ETH fails. On the positive side, we show how to get below the approximation factor of 2 by combining the parameters

k

and

h

: we develop a fixed-parameter 3/2-approximation with running time

$$2^{O(kh\log h)}\cdot n^{O(1)}$$

.

We also provide similar fixed-parameter approximations for the

weighted

k

-Center

and

$$(k,{\mathcal {F}})$$

-Partition

problems, which generalize

k

-Center.

We devise a unified framework for quantifying the inefficiency of equilibria in clustering games on networks. This class of games has two properties exhibited by many real-life social and economic settings: (a) an agent’s utility is affected only by the behavior of her direct neighbors rather than that of the entire society, and (b) an agent’s utility does not depend on the actual strategies chosen by agents, but rather by whether or not other agents selected the same strategy. Our framework is sufficiently general to account for unilateral versus coordinated deviations by coalitions of different sizes, different types of relationships between agents, and different structures of strategy spaces. Many settings that have been recently studied are special cases of clustering games on networks. Using our framework: (1) We recover previous results for special cases and provide extended and improved results in a unified way. (2) We identify new settings that fall into the class of clustering games on networks and establish price of anarchy and strong price of anarchy bounds for them.

For understanding the structure of the resulting graphs and for analyzing the behavior of network algorithms, the next question is bounding the size of the diameter. The only known bound is

$$\mathcal {O}((\log n)^{32/((3-\beta )(5-\beta ))})$$

(Kiwi and Mitsche. ANALCO, pp. 26–39, 2015). We present two much simpler proofs for an improved upper bound of

$$\mathcal {O}((\log n)^{2/(3-\beta )})$$

and a lower bound of

$$\Omega (\log n)$$

. If the average degree is bounded from above by some constant, we show that the latter bound is tight by proving an upper bound of

$$\mathcal {O}(\log n)$$

for the diameter.

This work studies the price of anarchy and the price of stability of cost-sharing methods in weighted congestion games. We require that our cost-sharing method and our set of cost functions satisfy certain natural conditions and we present general tight price of anarchy bounds, which are robust and apply to general equilibrium concepts. We then turn to the price of stability and prove an upper bound for the Shapley value cost-sharing method, which holds for general sets of cost functions and which is tight in special cases of interest, such as bounded degree polynomials. Also for bounded degree polynomials, we close the paper with a somehow surprising result, showing that a slight deviation from the Shapley value has a huge impact on the price of stability. In fact, for this case, the price of stability becomes as bad as the price of anarchy.

This paper revisits the classical problem of multi-message broadcast: given an undirected network

G

, the objective is to deliver

k

messages, initially placed arbitrarily in

G

, to all nodes. Per round, one message can be sent along each edge. The standard textbook result is an

$$O(D+k)$$

round algorithm, where

D

is the diameter of

G

. This bound is

existentially

optimal, which means there exists a graph

$$G'$$

with diameter

D

over which any algorithm needs

$$\varOmega (D+k)$$

rounds.

In this paper, we seek the stronger notion of optimality—called

universal optimality

by Garay, Kutten, and Peleg [FOCS’93]—which is with respect to the best possible for graph

G

itself. We present a distributed construction that produces a

k

-message broadcast schedule with length roughly within an

$$\tilde{O}(\log n)$$

factor of the best possible for

G

, after

$$\tilde{O}(D+k)$$

pre-computation rounds.

Our approach is conceptually inspired by that of Censor-Hillel, Ghaffari, and Kuhn [SODA’14, PODC’14] of finding many essentially-disjoint trees and using them to parallelize the flow of information. One key aspect that our result improves is that our trees have sufficiently low diameter to admit a nearly-optimal broadcast schedule, whereas the trees obtained by the algorithms of Censor-Hillel et al. could have arbitrarily large diameter, even up to

$$\Theta (n)$$

.

We provide sufficient conditions for revenue maximization in a two-good monopoly where the buyer’s valuations for the items come from independent (but not necessarily identical) distributions over bounded intervals. Under certain distributional assumptions, we give exact, closed-form formulas for the prices and allocation rules of the optimal selling mechanism. As a side result we give the first example of an optimal mechanism in an i.i.d. setting over a support of the form [0,

b

] which is

not

deterministic. Since our framework is based on duality techniques, we were also able to demonstrate how slightly relaxed versions of it can still be used to design mechanisms that have very good approximation ratios with respect to the optimal revenue, through a “convexification” process.

The question of how much bias a coalition of faulty players can introduce into distributed sampling protocols in the full information model was first studied by Ben-Or and Linial in 1985. They focused on the problem of

collective coin-flipping

, in which a set of

n

players wish to use their private randomness to generate a common random bit

b

in the presence of

t

(

n

) faulty players, such that the probability that

$$b=0$$

(and 1) are at least

$$\varepsilon $$

for some constant

$$\varepsilon >0$$

. They showed that the majority function can tolerate

$$t=\Theta (\sqrt{n})$$

corruptions even in the presence of adaptive adversaries and conjectured that this is optimal in the adaptive setting. Shortly thereafter, Lichtenstein, Linial, and Saks proved that the conjecture holds for protocols where each player sends a single bit. Their result has been the main progress on the conjecture for the last 30 years.

In this work we revisit this question, and ask: what about protocols where players can send longer messages? Can increased communication enable tolerance of a larger fraction of corrupt players?

We introduce a model of

strong adaptive

corruptions, in which an adversary sees all messages sent by honest parties in any given round, and based on the message content, decides whether to corrupt a party (and alter its message) or not. This is in contrast to the (classical) adaptive adversary, who corrupts parties based on prior communication history, and cannot alter messages already sent. Such strongly adaptive corruptions seem to be a realistic concern in settings where malicious parties can alter (or sabotage the delivery) of honest messages depending on their content, yet existing adversarial models do not take this into account.

We then shed light on the connection between adaptive and strongly adaptive adversaries, by proving that for any symmetric one-round coin-flipping protocol secure against

t

adaptive corruptions, there is a symmetric one-round coin-flipping protocol secure against

t

strongly adaptive corruptions. Going back to the standard adaptive model, we can now prove that any symmetric one-round protocol with arbitrarily long messages can tolerate at most

$$\widetilde{O}(\sqrt{n})$$

adaptive corruptions.

At the heart of our results there is a new technique for converting any one-round secure protocol with arbitrarily long messages into a secure one where each player sends only

$$\mathsf {polylog}(n)$$

bits. This technique may be of independent interest.

We present optimal online algorithms for two related known problems involving Steiner Arborescence, improving both the lower and the upper bounds. One of them is the well studied continuous problem of the

Rectilinear Steiner Arborescence

(

$$\text{RSA}$$

). We improve the lower bound and the upper bound on the competitive ratio for

$$\text{RSA}$$

from

$$O(\log N)$$

and

$$\varOmega (\sqrt{\log N})$$

to

$$\varTheta (\frac{\log N}{\log \log N})$$

, where

N

is the number of Steiner points. This separates the competitive ratios of

$$\text{RSA}$$

and the Symetric-

$$\text{RSA}$$

$$(\text{SRSA})$$

, two problems for which the bounds of Berman and Coulston is STOC 1997 were identical. The second problem is one of the Multimedia Content Distribution problems presented by Papadimitriou et al. in several papers and Charikar et al. SODA 1998. It can be viewed as the discrete counterparts (or a network counterpart) of

$$\text{RSA}$$

. For this second problem we present tight bounds also in terms of the network size, in addition to presenting tight bounds in terms of the number of Steiner points (the latter are similar to those we derived for

$$\text{RSA}$$

).

In this work we study a diffusion process in a network that consists of two types of vertices:

inhibitory

vertices (those obstructing the diffusion) and

excitatory

vertices (those facilitating the diffusion). We consider a continuous time model in which every edge of the network draws its transmission time randomly. For such an asynchronous diffusion process it has been recently proven that in Erdős-Rényi random graphs a

normalization phenomenon

arises: whenever the diffusion starts from a large enough (but still tiny) set of active vertices, it only percolates to a certain level that depends only on the activation threshold and the ratio of inhibitory to excitatory vertices. In this paper we extend this result to all networks in which the percolation process exhibits an explosive behaviour. This includes in particular inhomogeneous random networks, as given by Chung-Lu graphs with degree parameter

$$\beta \in (2,3)$$

.

Byzantine broadcast is a distributed primitive that allows a specific party to consistently distribute a message among

n

parties in the presence of potential misbehavior of up to

t

of the parties. The celebrated result of [

PSL80

] shows that broadcast is achievable from point-to-point channels if and only if

$$t < n/3$$

.

The following two generalizations have been proposed to the original broadcast problem. In [

FM98

] the authors considered a

general adversary

characterized by the sets of parties that can be corrupted. It was shown that broadcast is achievable from point-to-point channels if and only if no three possible corrupted sets can cover the whole party set. In [

CFF+05

] the notion of point-to-point channels has been extended to the

b

-minicast channels allowing to locally broadcast among any subset of

b

parties. It has been shown that broadcast secure against adversaries corrupting up to

t

parties is achievable from

b

-minicast if and only if

$$t < \frac{b-1}{b+1}n$$

.

In this paper we combine both generalizations by considering the problem of achieving broadcast from

b

-minicast channels secure against general adversaries. Our main result is a condition on the possible corrupted sets such that broadcast is achievable from

b

-minicast if and only if this condition holds.