Skip to main content

2011 | Buch

Automata, Languages and Programming

38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II

herausgegeben von: Luca Aceto, Monika Henzinger, Jiří Sgall

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

insite
SUCHEN

Über dieses Buch

The two-volume set LNCS 6755 and LNCS 6756 constitutes the refereed proceedings of the 38th International Colloquium on Automata, Languages and Programming, ICALP 2011, held in Zürich, Switzerland, in July 2011. The 114 revised full papers (68 papers for track A, 29 for track B, and 17 for track C) presented together with 4 invited talks, 3 best student papers, and 3 best papers were carefully reviewed and selected from a total of 398 submissions. The papers are grouped in three major tracks on algorithms, complexity and games; on logic, semantics, automata, and theory of programming; as well as on foundations of networked computation: models, algorithms and information management.

Inhaltsverzeichnis

Frontmatter

Invited Lectures

Nondeterministic Streaming String Transducers

We introduce

nondeterministic streaming string transducers

(

nssts

) – a new computational model that can implement MSO-definable relations between strings. An

nsst

makes a single left-to-right pass on the input string and uses a finite set of

string variables

to compute the output. In each step, it reads one input symbol, and updates its string variables in parallel with a

copyless assignment

. We show that

nsst

are closed under sequential composition and that their expressive power coincides with that of nondeterministic MSO-definable transductions. Further, we identify the class of

functional

nssts

; such an

nsst

allows nondeterministic transitions, but for every successful run on a given input generates the same output string. We show that deciding functionality of an arbitrary

nsst

is decidable with

pspace

complexity, while the equivalence problem for functional

nssts

is

pspace-complete

. We also show that checking if the set of outputs of an

nsst

is contained within the set of outputs of a finite number of

dssts

is decidable in

pspace

.

Rajeev Alur, Jyotirmoy V. Deshmukh
An Introduction to Randomness Extractors

We give an introduction to the area of “randomness extraction” and survey the main concepts of this area: deterministic extractors, seeded extractors and multiple sources extractors. For each one we briefly discuss background, definitions, explicit constructions and applications.

Ronen Shaltiel
Invitation to Algorithmic Uses of Inclusion–Exclusion

I give an introduction to algorithmic uses of the principle of inclusion–exclusion. The presentation is intended to be be concrete and accessible, at the expense of generality and comprehensiveness.

Thore Husfeldt
On the Relation between Differential Privacy and Quantitative Information Flow

Differential privacy is a notion that has emerged in the community of statistical databases, as a response to the problem of protecting the privacy of the database’s participants when performing statistical queries. The idea is that a randomized query satisfies differential privacy if the likelihood of obtaining a certain answer for a database

x

is not too different from the likelihood of obtaining the same answer on adjacent databases, i.e. databases which differ from

x

for only one individual.

Information flow is an area of Security concerned with the problem of controlling the leakage of confidential information in programs and protocols. Nowadays, one of the most established approaches to quantify and to reason about leakage is based on the Rényi min entropy version of information theory.

In this paper, we analyze critically the notion of differential privacy in light of the conceptual framework provided by the Rényi min information theory. We show that there is a close relation between differential privacy and leakage, due to the graph symmetries induced by the adjacency relation. Furthermore, we consider the utility of the randomized answer, which measures its expected degree of accuracy. We focus on certain kinds of utility functions called “binary”, which have a close correspondence with the Rényi min mutual information. Again, it turns out that there can be a tight correspondence between differential privacy and utility, depending on the symmetries induced by the adjacency relation and by the query. Depending on these symmetries we can also build an optimal-utility randomization mechanism while preserving the required level of differential privacy. Our main contribution is a study of the kind of structures that can be induced by the adjacency relation and the query, and how to use them to derive bounds on the leakage and achieve the optimal utility.

Mário S. Alvim, Miguel E. Andrés, Konstantinos Chatzikokolakis, Catuscia Palamidessi

Best Student Papers

A 1.488 Approximation Algorithm for the Uncapacitated Facility Location Problem

We present a 1.488 approximation algorithm for the metric uncapacitated facility location (UFL) problem. Previously the best algorithm was due to Byrka [1]. By linearly combining two algorithms

A

1(

γ

f

) for

γ

f

 ≈ 1.6774 and the (1.11,1.78)-approximation algorithm

A

2 proposed by Jain, Mahdian and Saberi [8], Byrka gave a 1.5 approximation algorithm for the UFL problem. We show that if

γ

f

is randomly selected from some distribution, the approximation ratio can be improved to 1.488. Our algorithm cuts the gap with the 1.463 approximability lower bound by almost 1/3.

Shi Li
Rice’s Theorem for μ-Limit Sets of Cellular Automata

Cellular automata are a parallel and synchronous computing model, made of infinitely many finite automata updating according to the same local rule. Rice’s theorem states that any nontrivial property over computable functions is undecidable. It has been adapted by Kari to limit sets of cellular automata [7], that is the set of configurations that can be reached arbitrarily late. This paper proves a new Rice theorem for

μ

-limit sets, which are sets of configurations often reached arbitrarily late.

Martin Delacourt
Fault-Tolerant Compact Routing Schemes for General Graphs

This paper considers compact fault-tolerant routing schemes for weighted general graphs, namely, routing schemes that avoid a set of failed (or

forbidden

) edges. We present a compact routing scheme capable of handling multiple edge failures. Assume a source node

s

contains a message

M

designated to a destination target

t

and assume a set

F

of edges crashes (unknown to

s

). Our scheme routes the message to

t

(provided that

s

and

t

are still connected in

G

 ∖ 

F

) over a path whose length is proportional to the distance between

s

and

t

in

G

 ∖ 

F

, to |

F

|

3

and to some poly-log factor. The routing table required at a node

v

is of size proportional to the degree of

v

in

G

and some poly-log factor. This improves on the previously known fault-tolerant compact routing scheme for general graphs, which was capable of overcoming at most 2 edge failures.

Shiri Chechik

Best Papers

Local Matching Dynamics in Social Networks

We study stable marriage and roommates problems in graphs with locality constraints. Each player is a node in a social network and has an incentive to match with other players. The value of a match is specified by an edge weight. Players explore possible matches only based on their current neighborhood. We study convergence of natural better-response dynamics that converge to

locally stable matchings

– matchings that allow no incentive to deviate with respect to their imposed information structure in the social network. For every starting state we construct in polynomial time a sequence of polynomially many better-response moves to a locally stable matching. However, for a large class of oblivious dynamics including random and concurrent better-response the convergence time turns out to be exponential. In contrast, convergence time becomes polynomial if we allow the players to have a small amount of random memory, even for many-to-many matchings and more general notions of neighborhood.

Martin Hoefer
Regular Languages of Words over Countable Linear Orderings

We develop an algebraic model for recognizing languages of words indexed by countable linear orderings. This notion of recognizability is effectively equivalent to definability in monadic second-order (MSO) logic. The proofs also imply the first known collapse result for MSO logic over countable linear orderings.

Olivier Carton, Thomas Colcombet, Gabriele Puppis
Algebraic Independence and Blackbox Identity Testing

Algebraic independence is an advanced notion in commutative algebra that generalizes independence of linear polynomials to higher degree. The transcendence degree (

trdeg

) of a set

$\{f_1, \dotsc, f_m\} \subset \mathbb{F}[x_1, \dotsc, x_n]$

of polynomials is the maximal size

r

of an algebraically independent subset. In this paper we design blackbox and efficient linear maps

ϕ

that reduce the number of variables from

n

to

r

but maintain

trdeg

{

ϕ

(

f

i

)}

i

 = 

r

, assuming

f

i

’s sparse and small

r

. We apply these fundamental maps to solve several cases of blackbox identity testing:

1

Given a circuit

C

and sparse subcircuits

f

1

,…,

f

m

of

trdeg

r

such that

D

: = 

C

(

f

1

,…,

f

m

) has polynomial degree, we can test blackbox

D

for zeroness in

poly

(

size

(

D

))

r

time.

2

Define a ΣΠΣΠ

δ

(

k

,

s

,

n

) circuit

C

to be of the form ∑ 

i

 = 1

k

 ∏ 

j

 = 1

s

f

i

,

j

, where

f

i

,

j

are sparse

n

-variate polynomials of degree at most

δ

. For

k

 = 2, we give a

$poly(\delta sn)^{\delta^2}$

time blackbox identity test.

3

For a general depth-4 circuit we define a notion of rank. Assuming there is a rank bound

R

for minimal simple ΣΠΣΠ

δ

(

k

,

s

,

n

) identities, we give a

$poly(\delta snR)^{Rk\delta^2}$

time blackbox identity test for ΣΠΣΠ

δ

(

k

,

s

,

n

) circuits. This partially generalizes the state of the art of depth-3 to depth-4 circuits.

The notion of

trdeg

works best with large or zero characteristic, but we also give versions of our results for arbitrary fields.

Malte Beecken, Johannes Mittmann, Nitin Saxena

Session B1: Foundations of Program Semantics

A Fragment of ML Decidable by Visibly Pushdown Automata

The simply-typed, call-by-value language,

RML

, may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a “bad variable” construct in the sense of Reynolds. By a

short

type, we mean a type of order at most 2 and arity at most 1. We consider the

O-strict

fragment of (finitary)

RML

,

RML

O

 − 

Str

, consisting of terms-in-context

x

1

:

θ

1

, ... ,

x

n

:

θ

n

 ⊢ 

M

:

θ

such that

θ

is short, and every argument type of every

θ

i

is short.

RML

O

 − 

Str

is surprisingly expressive; it includes several instances of (in)equivalence in the literature that are challenging to prove using methods based on (state-based) logical relations. We show that it is decidable whether a given pair of

RML

O

 − 

Str

terms-in-context is observationally equivalent. Using the fully abstract game semantics of

RML

, our algorithm reduces the problem to the language equivalence of visibly pushdown automata. When restricted to terms in canonical form, the problem is EXPTIME-complete.

David Hopkins, Andrzej S. Murawski, C. -H. Luke Ong
Krivine Machines and Higher-Order Schemes

We propose a new approach to analysing higher-order recursive schemes. Many results in the literature use automata models generalising pushdown automata, most notably higher-order pushdown automata with collapse (CPDA). Instead, we propose to use the Krivine machine model. Compared to CPDA, this model is closer to lambdacalculus, and incorporates nicely many invariants of computations, as for example the typing information. The usefulness of the proposed approach is demonstrated with new proofs of two central results in the field: the decidability of the local and global model checking problems for higher-order schemes with respect to the mu-calculus.

S. Salvati, I. Walukiewicz
Relating Computational Effects by ⊤ ⊤-Lifting

We consider the problem of establishing a relationship between two interpretations of base type terms of a

λ

c

-calculus with algebraic operations. We show that the given relationship holds if it satisfies a set of natural conditions. We apply this result to comparing interpretations of new name creation by two monads: Stark’s new name creation monad [25] and a global counter monad.

Shin-ya Katsumata
Constructing Differential Categories and Deconstructing Categories of Games

We present an abstract construction for building differential categories useful to model resource sensitive calculi, and we apply it to categories of games. In one instance, we recover a category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model. A second instance corresponds to a new Cartesian differential category of games. We give a model of a Resource PCF in this category and show that it enjoys the finite definability property. Comparison with a relational semantics reveals that the latter also possesses this property and is fully abstract.

Jim Laird, Giulio Manzonetto, Guy McCusker

Session B2: Automata and Formal Languages

Nondeterminism Is Essential in Small 2FAs with Few Reversals

On every

n

-long input, every two-way finite automaton (2fa) can reverse its head

O

(

n

) times before halting. A 2FA

with

few reversals is an automaton where this number is only

o

(

n

). For every

h

, we exhibit a language that requires Ω(2

h

) states on every deterministic 2FA with few reversals, but only

h

states on a nondeterministic 2FA with few reversals.

Christos A. Kapoutsis
Isomorphism of Regular Trees and Words

The complexity of the isomorphism problem for regular trees, regular linear orders, and regular words is analyzed. A tree is regular if it is isomorphic to the prefix order on a regular language. In case regular languages are represented by NFAs (DFAs), the isomorphism problem for regular trees turns out to be

EXPTIME

-complete (resp.

P

-complete). In case the input automata are acyclic NFAs (acyclic DFAs), the corresponding trees are (succinctly represented) finite trees, and the isomorphism problem turns out to be

PSPACE

-complete (resp.

P

-complete). A linear order is regular if it is isomorphic to the lexicographic order on a regular language. A polynomial time algorithm for the isomorphism problem for regular linear orders (and even regular words, which generalize the latter) given by DFAs is presented. This solves an open problem by Ésik and Bloom. A long version of this paper can be found in [18].

Markus Lohrey, Christian Mathissen
On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids

During recent decades, classical models in language theory have been extended by control mechanisms defined by monoids. We study which monoids cause the extensions of context-free grammars, finite automata, or finite state transducers to exceed the capacity of the original model. Furthermore, we investigate when, in the extended automata model, the nondeterministic variant differs from the deterministic one in capacity. We show that all these conditions are in fact equivalent and present an algebraic characterization. In particular, the open question of whether every language generated by a valence grammar over a finite monoid is context-free is provided with a positive answer.

Georg Zetzsche
The Cost of Traveling between Languages

We show how to calculate the maximum number of edits per character needed to convert any string in one regular language to a string in another language. Our algorithm makes use of a local determinization procedure applicable to a subclass of distance automata. We then show how to calculate the same property when the editing needs to be done in streaming fashion, by a finite state transducer, using a reduction to mean-payoff games. We show that the optimal streaming editor can be produced in PTIME.

Michael Benedikt, Gabriele Puppis, Cristian Riveros

Session B3: Model Checking

Emptiness and Universality Problems in Timed Automata with Positive Frequency

The languages of infinite timed words accepted by timed automata are traditionally defined using Büchi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting locations. We study various properties of timed languages accepted with positive frequency, and in particular the emptiness and universality problems.

Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Amélie Stainer
Büchi Automata Can Have Smaller Quotients

We study novel simulation-like preorders for quotienting nondeterministic Büchi automata. We define

fixed-word delayed simulation

, a new preorder coarser than delayed simulation. We argue that fixed-word simulation is the coarsest forward simulation-like preorder which can be used for quotienting Büchi automata, thus improving our understanding of the limits of quotienting. Also, we show that computing fixed-word simulation is PSPACE-complete.

On the practical side, we introduce

proxy simulations

, which are novel polynomial-time computable preorders sound for quotienting. In particular,

delayed proxy simulation

induce quotients that can be smaller by an arbitrarily large factor than direct backward simulation. We derive proxy simulations as the product of a theory of refinement transformers: A

refinement transformer

maps preorders nondecreasingly, preserving certain properties. We study under which general conditions refinement transformers are sound for quotienting.

Lorenzo Clemente
Automata-Based CSL Model Checking

For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. The presented decision procedure, however, has exponential complexity. In this paper, we propose an effective approximation algorithm for full CSL.

The key to our method is the notion of

stratified CTMCs

with respect to the CSL property to be checked. We present a measure-preservation theorem allowing us to reduce the problem to a transient analysis on stratified CTMCs. The corresponding probability can then be approximated in polynomial time (using uniformization). This makes the present work the centerpiece of a broadly applicable full CSL model checker.

Recently, the decision algorithm by Aziz

et al.

was shown to be incorrect in general. In fact, it works only for stratified CTMCs. As an additional contribution, our measure-preservation theorem can be used to ensure the decidability for general CTMCs.

Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns
A Progress Measure for Explicit-State Probabilistic Model-Checkers

Verification of the source code of a probabilistic system by means of an explicit-state model-checker is challenging. In most cases, the probabilistic model-checker will run out of memory due to the infamous state space explosion problem. As far as we know, we are the first to introduce the notion of a progress measure for such a model-checker. The progress measure returns a number in the interval [0, 1]. This number captures the amount of progress the model-checker has made towards verifying a particular linear-time property. The larger the number, the more progress the model-checker has made. We prove that the progress measure provides a lower bound of the measure of the set of execution paths that satisfy the property. We also show how to compute the progress measure for checking a particular class of linear-time properties, namely invariants.

Xin Zhang, Franck van Breugel

Session B4: Probabilistic Systems

Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation

We show how bisimulation equivalence and simulation preorder on probabilistic LTSs (PLTSs), namely the main behavioural relations on probabilistic nondeterministic processes, can be characterized by abstract interpretation. Both bisimulation and simulation can be obtained as completions of partitions and preorders, viewed as abstract domains, w.r.t. a pair of concrete functions that encode a PLTS. As a consequence, this approach provides a general framework for designing algorithms for computing bisimulation and simulation on PLTSs. Notably, (i) we show that the standard bisimulation algorithm by Baier et al. can be viewed as an instance of such a framework and (ii) we design a new efficient simulation algorithm that improves the state of the art.

Silvia Crafa, Francesco Ranzato
On the Semantics of Markov Automata

Markov automata describe systems in terms of events which may be nondeterministic, may occur probabilistically, or may be subject to time delays. We define a novel notion of weak bisimulation for such systems and prove that this provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between such systems, a generalisation of

reduction barbed congruence

, the well-known touchstone equivalence for a large variety of process description languages.

Yuxin Deng, Matthew Hennessy
Runtime Analysis of Probabilistic Programs with Unbounded Recursion

We study the runtime in probabilistic programs with unbounded recursion. As underlying formal model for such programs we use

probabilistic pushdown automata (pPDA)

which exactly correspond to recursive Markov chains. We show that every pPDA can be transformed into a stateless pPDA (called “pBPA”) whose runtime and further properties are closely related to those of the original pPDA. This result substantially simplifies the analysis of runtime and other pPDA properties. We prove that for every pPDA the probability of performing a long run decreases

exponentially

in the length of the run, if and only if the expected runtime in the pPDA is

finite

. If the expectation is infinite, then the probability decreases “polynomially”. We show that these bounds are asymptotically tight. Our tail bounds on the runtime are

generic

, i.e., applicable to any probabilistic program with unbounded recursion. An intuitive interpretation is that in pPDA the runtime is exponentially unlikely to deviate from its expected value.

Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, Ivana Hutařová Vařeková
Approximating the Termination Value of One-Counter MDPs and Stochastic Games

One-counter MDPs (OC-MDPs) and one-counter simple stochastic games (OC-SSGs) are 1-player, and 2-player turn-based zero-sum, stochastic games played on the transition graph of classic one-counter automata (equivalently, pushdown automata with a 1-letter stack alphabet). A key objective for the analysis and verification of these games is the

termination

objective, where the players aim to maximize (minimize, respectively) the probability of hitting counter value 0, starting at a given control state and given counter value.

Recently [4,2], we studied qualitative decision problems (“is the optimal termination value = 1?”) for OC-MDPs (and OC-SSGs) and showed them to be decidable in P-time (in NP∩coNP, respectively). However,

quantitative

decision and approximation problems (“is the optimal termination value ≥ p”, or “approximate the termination value within

ε

”) are far more challenging. This is so in part because optimal strategies may not exist, and because even when they do exist they can have a highly non-trivial structure. It thus remained open even whether any of these quantitative termination problems are computable.

In this paper we show that all quantitative

approximation

problems for the termination value for OC-MDPs and OC-SSGs are computable. Specifically, given a OC-SSG, and given

ε

 > 0, we can compute a value

v

that approximates the value of the OC-SSG termination game within additive error

ε

, and furthermore we can compute

ε

-optimal strategies for both players in the game.

A key ingredient in our proofs is a subtle martingale, derived from solving certain LPs that we can associate with a maximizing OC-MDP. An application of Azuma’s inequality on these martingales yields a computable bound for the “wealth” at which a “rich person’s strategy” becomes

ε

-optimal for OC-MDPs.

Tomáš Brázdil, Václav Brožek, Kousha Etessami, Antonín Kučera

Session B5: Logic in Computer Science

Generic Expression Hardness Results for Primitive Positive Formula Comparison

We study the expression complexity of two basic problems involving the comparison of primitive positive formulas: equivalence and containment. We give two generic hardness results for the studied problems, and discuss evidence that they are optimal and yield, for each of the problems, a complexity trichotomy.

Simone Bova, Hubie Chen, Matthew Valeriote
Guarded Negation

We consider restrictions of first-order logic and of fixpoint logic in which all occurrences of negation are required to be guarded by an atomic predicate. In terms of expressive power, the logics in question, called GNFO and GNFP, extend the guarded fragment of first-order logic and guarded least fixpoint logic, respectively. They also extend the recently introduced unary negation fragments of first-order logic and of least fixpoint logic.

We show that the satisfiability problem for GNFO and for GNFP is 2ExpTime-complete, both on arbitrary structures and on finite structures. We also study the complexity of the associated model checking problems. Finally, we show that GNFO and GNFP are not only computationally well behaved, but also model theoretically: we show that GNFO and GNFP have the tree-like model property and that GNFO has the finite model property, and we characterize the expressive power of GNFO in terms of invariance for an appropriate notion of bisimulation.

Vince Bárány, Balder ten Cate, Luc Segoufin
Locality of Queries Definable in Invariant First-Order Logic with Arbitrary Built-in Predicates

We consider first-order formulas over relational structures which may use arbitrary numerical predicates. We require that the validity of the formula is independent of the particular interpretation of the numerical predicates and refer to such formulas as Arb-invariant first-order.

Our main result shows a Gaifman locality theorem: two tuples of a structure with

n

elements, having the same neighborhood up to distance (log n)

ω

(1)

, cannot be distinguished by Arb-invariant first-order formulas. When restricting attention to word structures, we can achieve the same quantitative strength for Hanf locality. In both cases we show that our bounds are tight.

Our proof exploits the close connection between Arb-invariant first-order formulas and the complexity class AC

0

, and hinges on the tight lower bounds for parity on constant-depth circuits.

Matthew Anderson, Dieter van Melkebeek, Nicole Schweikardt, Luc Segoufin
Modular Markovian Logic

We introduce Modular Markovian Logic (MML) for compositional continuous-time and continuous-space Markov processes. MML combines operators specific to stochastic logics with operators reflecting the modular structure of the models, similar to those used by spatial and separation logics. We present a complete Hilbert-style axiomatization for MML, prove the small model property and analyze the relation between stochastic bisimulation and logical equivalence.

Luca Cardelli, Kim G. Larsen, Radu Mardare

Session B6: Hybrid Systems

Programming with Infinitesimals: A While-Language for Hybrid System Modeling

We add, to the common combination of a

$\textsc{While}$

-language and a Hoare-style program logic, a constant

$\ensuremath \mathtt{d{\kern-.5pt}t}$

that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of

hybrid systems

: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge. We rigorously define the semantics of programs in the language of

nonstandard analysis

, on the basis of which the program logic is shown to be sound and relatively complete.

Kohei Suenaga, Ichiro Hasuo
Model Checking the Quantitative μ-Calculus on Linear Hybrid Systems

In this work, we consider the model-checking problem for a quantitative extension of the modal

μ

-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions, which arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and additionally allow to measure interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative

μ

-calculus, can be model-checked with arbitrary precision on initialised linear hybrid systems. To this end, we develop new techniques for the discretisation of continuous state spaces based on a special class of strategies in model-checking games and show decidability of a class of counter-reset games that may be of independent interest.

Diana Fischer, Łukasz Kaiser
On Reachability for Hybrid Automata over Bounded Time

This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within

T

time units, where

T

is a constant rational value. We show that, in contrast to the classical (unbounded) reachability problem, the timed-bounded version is

decidable

for rectangular hybrid automata provided only non-negative rates are allowed. This class of systems is of practical interest and subsumes, among others, the class of stopwatch automata. We also show that the problem becomes undecidable if either diagonal constraints or both negative and positive rates are allowed.

Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin, James Worrell

Session B7: Specification and Verification

Deciding Robustness against Total Store Ordering

We address the problem of deciding robustness of a program against the total store ordering (TSO) relaxed memory model, i.e., of checking whether the behaviour under TSO coincides with the expected sequential consistency (SC) semantics. We prove that this problem is

PSpace

-complete. The key insight is that violations to robustness can be detected on pairs of SC computations.

Ahmed Bouajjani, Roland Meyer, Eike Möhlmann
Multiply-Recursive Upper Bounds with Higman’s Lemma

We develop a new analysis for the length of controlled bad sequences in well-quasi-orderings based on Higman’s Lemma. This leads to tight multiply-recursive upper bounds that readily apply to several verification algorithms for well-structured systems.

S. Schmitz, Ph. Schnoebelen
Liveness-Preserving Atomicity Abstraction

Modern concurrent algorithms are usually encapsulated in libraries, and complex algorithms are often constructed using libraries of simpler ones. We present the first theorem that allows harnessing this structure to give compositional liveness proofs to concurrent algorithms and their clients. We show that, while proving a liveness property of a client using a concurrent library, we can soundly replace the library by another one related to the original library by a generalisation of a well-known notion of linearizability. We apply this result to show formally that lock-freedom, an often-used liveness property of non-blocking algorithms, is compositional for linearizable libraries, and provide an example illustrating our proof technique.

Alexey Gotsman, Hongseok Yang
On Stabilization in Herman’s Algorithm

Herman’s algorithm is a synchronous randomized protocol for achieving self-stabilization in a token ring consisting of

N

processes. The interaction of tokens makes the dynamics of the protocol very difficult to analyze. In this paper we study the expected time to stabilization in terms of the initial configuration.

It is straightforward that the algorithm achieves stabilization almost surely from any initial configuration, and it is known that the worst-case expected time to stabilization (with respect to the initial configuration) is Θ(

N

2

). Our first contribution is to give an upper bound of 0.64

N

2

on the expected stabilization time, improving on previous upper bounds and reducing the gap with the best existing lower bound. We also introduce an asynchronous version of the protocol, showing a similar

O

(

N

2

) convergence bound in this case.

Assuming that errors arise from the corruption of some number

k

of bits, where

k

is fixed independently of the size of the ring, we show that the expected time to stabilization is

O

(

N

). This reveals a hitherto unknown and highly desirable property of Herman’s algorithm: it recovers quickly from bounded errors. We also show that if the initial configuration arises by resetting each bit independently and uniformly at random, then stabilization is significantly faster than in the worst case.

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, James Worrell, Lijun Zhang

Session C1: Graphs

Online Graph Exploration: New Results on Old and New Algorithms

We study the problem of exploring an unknown undirected connected graph. Beginning in some start vertex, a searcher must visit each node of the graph by traversing edges. Upon visiting a vertex for the first time, the searcher learns all incident edges and their respective traversal costs. The goal is to find a tour of minimum total cost. Kalyanasundaram and Pruhs [23] proposed a sophisticated generalization of a Depth First Search that is 16-competitive on planar graphs. While the algorithm is feasible on arbitrary graphs, the question whether it has constant competitive ratio in general has remained open. Our main result is an involved lower bound construction that answers this question negatively. On the positive side, we prove that the algorithm has constant competitive ratio on any class of graphs with bounded genus. Furthermore, we provide a constant competitive algorithm for general graphs with a bounded number of distinct weights.

Nicole Megow, Kurt Mehlhorn, Pascal Schweitzer
Distance Oracles for Vertex-Labeled Graphs

Given a graph

G

 = (

V

,

E

) with non-negative edge lengths whose vertices are assigned a

label

from

L

 = {

λ

1

,…,

λ

}, we construct a compact

distance oracle

that answers queries of the form: “What is

δ

(

v

,

λ

)?”, where

v

 ∈ 

V

is a vertex in the graph,

λ

 ∈ 

L

a vertex label, and

δ

(

v

,

λ

) is the distance (length of a shortest path) between

v

and the closest vertex labeled

λ

in

G

. We formalize this natural problem and provide a hierarchy of

approximate distance oracles

that require subquadratic space and return a distance of constant stretch. We also extend our solution to dynamic oracles that handle label changes in sublinear time.

Danny Hermelin, Avivit Levy, Oren Weimann, Raphael Yuster
Asymptotically Optimal Randomized Rumor Spreading

We propose a new protocol for the fundamental problem of disseminating a piece of information to all members of a group of

n

players. It builds upon the classical randomized rumor spreading protocol and several extensions. The main achievements are the following:

Our protocol spreads a rumor from one node to all other nodes in the asymptotically optimal time of (1 + 

o

(1)) log

2

n

. The whole process can be implemented in a way such that only

O

(

n

f

(

n

)) calls are made, where

f

(

n

) = 

ω

(1) can be arbitrary.

In spite of these quantities being close to the theoretical optima, the protocol remains relatively robust against failures; for

random

node failures, our algorithm again comes arbitrarily close to the theoretical optima.

The protocol can be extended to also deal with

adversarial

node failures. The price for that is only a constant factor increase in the run-time, where the constant factor depends on the fraction of failing nodes the protocol is supposed to cope with. It can easily be implemented such that only

O

(

n

) calls to properly working nodes are made.

In contrast to the push-pull protocol by Karp et al. [FOCS 2000], our algorithm only uses push operations, i.e., only informed nodes take active actions in the network. On the other hand, we discard address-obliviousness. To the best of our knowledge, this is the first randomized push algorithm that achieves an asymptotically optimal running time.

Benjamin Doerr, Mahmoud Fouz
Fast Convergence for Consensus in Dynamic Networks

We study the convergence time required to achieve consensus in dynamic networks. In each time step, a node’s value is updated to some weighted average of its neighbors’ and its old values. We study the case when the underlying network is dynamic, and investigate different averaging models. Both our analysis and experiments show that dynamic networks exhibit fast convergence behavior, even under very mild connectivity assumptions.

T-H. Hubert Chan, Li Ning

Session C2: Matchings and Equilibria

Linear Programming in the Semi-streaming Model with Application to the Maximum Matching Problem

In this paper, we study linear programming based approaches to the maximum matching problem in the semi-streaming model. The semi-streaming model has gained attention as a model for processing massive graphs as the importance of such graphs has increased. This is a model where edges are streamed-in in an adversarial order and we are allowed a space proportional to the number of vertices in a graph.

In recent years, there has been several new results in this semi-streaming model. However broad techniques such as linear programming have not been adapted to this model. We present several techniques to adapt and optimize linear programming based approaches in the semi-streaming model with an application to the maximum matching problem. As a consequence, we improve (almost) all previous results on this problem, and also prove new results on interesting variants.

Kook Jin Ahn, Sudipto Guha
Restoring Pure Equilibria to Weighted Congestion Games

Congestion games model several interesting applications, including routing and network formation games, and also possess attractive theoretical properties, including the existence of and convergence of natural dynamics to a pure Nash equilibrium. Weighted variants of congestion games that rely on sharing costs proportional to players’ weights do not generally have pure-strategy Nash equilibria. We propose a new way of assigning costs to players with weights in congestion games that recovers the important properties of the unweighted model. This method is derived from the Shapley value, and it always induces a game with a (weighted) potential function. For the special cases of weighted network cost-sharing and atomic selfish routing games (with Shapley value-based cost shares), we prove tight bounds on the price of stability and price of anarchy, respectively.

Konstantinos Kollias, Tim Roughgarden
Existence and Uniqueness of Equilibria for Flows over Time

Network flows that vary over time arise naturally when modeling rapidly evolving systems such as the Internet. In this paper, we continue the study of equilibria for flows over time in the single-source single-sink deterministic queuing model proposed by Koch and Skutella. We give a constructive proof for the existence and uniqueness of equilibria for the case of a piecewise constant inflow rate, through a detailed analysis of the static flows obtained as derivatives of a dynamic equilibrium.

Roberto Cominetti, José R. Correa, Omar Larré
Collusion in Atomic Splittable Routing Games

We investigate how collusion affects the social cost in atomic splittable routing games. Suppose that players form coalitions and each coalition behaves as if it were a single player controlling all the flows of its participants. It may be tempting to conjecture that the social cost would be lower after collusion, since there would be more coordination among the players. We construct examples to show that this conjecture is not true. These examples motivates the question:

under what conditions would the social cost of the post-collusion equilibrium be bounded by the social cost of the pre-collusion equilibrium?

We show that if (i) the network is “well-designed” (satisfying a natural condition), and (ii) the delay functions are affine, then collusion is always beneficial for the social cost in the Nash equilibria. On the other hand, if either of the above conditions is unsatisfied, collusion can worsen the social cost. Our main technique is a novel flow-augmenting algorithm to build Nash equilibria.

Chien-Chung Huang

Session C3: Privacy and Content Search

Privacy-Preserving Access of Outsourced Data via Oblivious RAM Simulation

We describe schemes for the

oblivious RAM simulation

problem with a small logarithmic or polylogarithmic amortized increase in access times, with a very high probability of success, while keeping the external storage to be of size

O

(

n

).

Michael T. Goodrich, Michael Mitzenmacher
Adaptively Secure Non-interactive Threshold Cryptosystems

Threshold cryptography aims at enhancing the availability and security of decryption and signature schemes by splitting private keys into several (say

n

) shares (typically, each of size comparable to the original secret key). In these schemes, a quorum of at least (

t

 ≤ 

n

) servers needs to act upon a message to produce the result (decrypted value or signature), while corrupting less than

t

servers maintains the scheme’s security. For about two decades, extensive study was dedicated to this subject, which created a number of notable results. So far, most practical threshold signatures, where servers act non-interactively, were analyzed in the limited static corruption model (where the adversary chooses which servers will be corrupted at the system’s initialization stage). Existing threshold encryption schemes that withstand the strongest combination of adaptive malicious corruptions (allowing the adversary to corrupt servers at any time based on its complete view), and chosen-ciphertext attacks (CCA) all require interaction (in the non-idealized model) and attempts to remedy this problem resulted only in relaxed schemes. The same is true for threshold signatures secure under chosen-message attacks (CMA).

To date (for about 10 years), it has been open whether there are non-interactive threshold schemes providing the highest security (namely, CCA-secure encryption and CMA-secure signature) with scalable shares (

i.e.

, as short as the original key) and adaptive security. This paper answers this question affirmatively by presenting such efficient decryption and signature schemes within a unified algebraic framework.

Benoît Libert, Moti Yung
Content Search through Comparisons

We study the problem of navigating through a database of similar objects using comparisons under heterogeneous demand, a problem closely related to small-world network design. We show that, under heterogeneous demand, the small-world network design problem is NP-hard. Given the above negative result, we propose a novel mechanism for small-world network design and provide an upper bound on its performance under heterogeneous demand. The above mechanism has a natural equivalent in the context of content search through comparisons, again under heterogeneous demand; we use this to establish both upper and lower bounds on content search through comparisons.

Amin Karbasi, Stratis Ioannidis, Laurent Massoulié

Session C4: Distributed Computation

Efficient Distributed Communication in Ad-Hoc Radio Networks

We present new distributed deterministic solutions to two communication problems in

n

-node ad-hoc radio networks: rumor gathering and multi-broadcast. In these problems, some or all nodes of the network initially contain input data called rumors, which have to be learned by other nodes. In rumor gathering, there are

k

rumors initially distributed arbitrarily among the nodes, and the goal is to collect all the rumors at one node. Our rumor gathering algorithm works in

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

time and our multi-broadcast algorithm works in

${\mathcal O}(k\log^3 n+n\log^4 n)$

time, for any

n

-node networks and

k

rumors (with arbitrary

k

), which is a substantial improvement over the best previously known deterministic solutions to these problems.

As a consequence, we

exponentially

decrease the gap between upper and lower bounds on the deterministic time complexity of four communication problems: rumor gathering, multi-broadcast, gossiping and routing, in the important case when every node has initially at most one rumor (this is the scenario for gossiping and for the usual formulation of routing). Indeed, for

$k={\mathcal O}(n)$

, our results simultaneously decrease the complexity gaps for these four problems from polynomial to polylogarithmic in the size of the graph. Moreover, our

deterministic

gathering algorithm applied for

$k={\mathcal O}(n)$

rumors, improves over the best previously known

randomized

algorithm of time

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

.

Bogdan S. Chlebus, Dariusz R. Kowalski, Andrzej Pelc, Mariusz A. Rokicki
Nearly Optimal Bounds for Distributed Wireless Scheduling in the SINR Model

We study the wireless scheduling problem in the physically realistic SINR model. More specifically: we are given a set of

n

links, each a sender-receiver pair. We would like to schedule the links using the minimum number of slots, using the SINR model of interference among simultaneously transmitting links. In the basic problem, all senders transmit with the same uniform power.

In this work, we provide a distributed

O

(log

n

)-approximation for the scheduling problem, matching the best ratio known for centralized algorithms. This is based on an algorithm studied by Kesselheim and Vöcking, improving their analysis by a logarithmic factor. We show this to be best possible for any such distributed algorithm.

Our analysis extends also to linear power assignments, and as well as for more general assignments, modulo assumptions about message acknowledgement mechanisms.

Magnús M. Halldórsson, Pradipta Mitra
Convergence Time of Power-Control Dynamics

We study two (classes of) distributed algorithms for power control in a general model of wireless networks. There are

n

wireless communication requests or

links

that experience interference and noise. To be successful a link must satisfy an SINR constraint. The goal is to find a set of powers such that all links are successful simultaneously. A classic algorithm for this problem is the fixed-point iteration due to Foschini and Miljanic [8], for which we prove the first bounds on worst-case running times – after roughly

O

(

n

log

n

) rounds all SINR constraints are nearly satisfied. When we try to satisfy each constraint exactly, however, convergence time is infinite. For this case, we design a novel framework for power control using regret learning algorithms and iterative discretization. While the exact convergence times must rely on a variety of parameters, we show that roughly a polynomial number of rounds suffices to make every link successful during at least a constant fraction of all previous rounds.

Johannes Dams, Martin Hoefer, Thomas Kesselheim
A New Approach for Analyzing Convergence Algorithms for Mobile Robots

Given a set of

n

mobile robots in the

d

-dimensional Euclidean space, the goal is to let them converge to a single not predefined point. The challenge is that the robots are limited in their capabilities. Robots can, upon activation, compute the positions of all other robots using an individual affine coordinate system. The robots are indistinguishable, oblivious and may have different affine coordinate systems. A very general discrete time model assumes that robots are activated in arbitrary order. Further, the computation of a new target point may happen much earlier than the movement, so that the movement is based on outdated information about other robot’s positions. Time is measured as the number of rounds, where a round ends as soon as each robot has moved at least once. In [6], the Center of Gravity is considered as target function, convergence was proven, and the number of rounds needed for halving the diameter of the convex hull of the robot’s positions was shown to be

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

and Ω(

n

). We present an easy-to-check property of target functions that guarantee convergence and yields upper time bounds. This property intuitively says that when a robot computes a new target point, this point is significantly within the current axes aligned minimal box containing all robots. This property holds, e.g., for the above-mentioned target function, and improves the above

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

to an asymptotically optimal

$\mathcal{O}(n)$

upper bound. Our technique also yields a constant time bound for a target function that requires all robots having identical coordinate axes.

Andreas Cord-Landwehr, Bastian Degener, Matthias Fischer, Martina Hüllmann, Barbara Kempkes, Alexander Klaas, Peter Kling, Sven Kurras, Marcus Märtens, Friedhelm Meyer auf der Heide, Christoph Raupach, Kamil Swierkot, Daniel Warner, Christoph Weddemann, Daniel Wonisch
Backmatter
Metadaten
Titel
Automata, Languages and Programming
herausgegeben von
Luca Aceto
Monika Henzinger
Jiří Sgall
Copyright-Jahr
2011
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-22012-8
Print ISBN
978-3-642-22011-1
DOI
https://doi.org/10.1007/978-3-642-22012-8

Premium Partner