Automata, Languages and Programming
38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2010. Proceedings, Part II
Published on 21. June 2011
XXVI, 666 pages
978-3-642-22012-8 (ISBN)
Description
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.
More details
Other editions
Additional editions
Luca Aceto | Monika Henzinger | Jiri Sgall
Automata, Languages and Programming
38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2010. Proceedings, Part II
Book
06/2011
1st Edition
Springer
€106.99
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Lectures
- Nondeterministic Streaming String Transducers
- Introduction
- Transducer Models
- Background
- Streaming String Transducers
- Expressiveness Results
- Properties of nssts
- Comparison with Existing Models
- Decision Problems
- Discussion
- References
- An Introduction to Randomness Extractors
- Introduction
- Deterministic Extractors
- =.26em plus .1em minus .1em Min-entropy: Measuring the Number of Random Bits in a Source
- Explicitness
- Deterministic Extractors for von-Neumann Sources
- Impossibility of Extraction from Santha-Vazirani Sources
- Bit-Fixing Sources and Privacy Amplification
- =.26em plus .1em minus .1em Families of Sources in the Literature on Deterministic Extraction
- Seeded Extractors
- Explicit Constructions and Lower Bounds
- Simulating BPP with Access to a Weak Random Source
- Seeded Extractors and List-Decodable Error-Correcting Codes
- Seeded Dispersers as Graphs with Expansion Properties
- Graphs with Expansion Beating the Eigenvalue Bound
- Seeded Extractors and Averaging Samplers
- Extractors for Multiple Independent Sources
- Generating Keys for Cryptographic Protocols
- 2-Source Dispersers and Ramsey Graphs
- Explicit Constructions of -Source Extractors and Dispersers
- Some Open Problems
- References
- Invitation to Algorithmic Uses of Inclusion-Exclusion
- The principle of inclusion-exclusion.
- Graph colouring.
- Counting the number of independent sets.
- Perfect matchings in bipartite graphs.
- Perfect matchings in general graphs.
- Inclusion-exclusion for sets.
- Hamiltonian paths.
- Steiner tree.
- Long paths.
- Yates's algorithm.
- Möbius inversion.
- Covering by Möbius inversion.
- References
- On the Relation between Differential Privacy and Quantitative Information Flow
- Introduction
- Preliminaries
- Database Domain and Differential Privacy
- Information Theory and Application to Information Flow
- Graph Symmetries
- Deriving the Relation between Differential Privacy and QIF on the Basis of the Graph Structure
- Application to Leakage
- Application to Utility
- Related Work
- Conclusion and Future Work
- References
- Best Student Papers
- A 1.488 Approximation Algorithm for the Uncapacitated Facility Location Problem
- Introduction
- Review of the Algorithm A1() in Byr07
- A 1.488 Approximation Algorithm for the UFL Problem
- Upper-Bounding the Expected Connection Cost of a Client
- An Explicit Distribution of $\gamma$
- References
- Rice's Theorem for $\mu$-Limit Sets of Cellular Automata
- Introduction
- Definitions
- Words and Density
- Cellular Automata
- $\mu$-Limit Sets
- Properties of $\mu$-Limit Sets
- Counters
- Merging Segments
- Rice Theorem
- Construction
- H $\mu$-Nilpotent
- H Not $\mu$-Nilpotent
- Rice Theorem
- Conclusion
- References
- Fault-Tolerant Compact Routing Schemes for General Graphs
- Introduction
- General Framework
- Routing on a Tree with Faults
- Preprocessing
- The Routing Process
- Analysis
- Analysis for the Entire Routing Scheme
- References
- Best Papers
- Local Matching Dynamics in Social Networks
- Introduction
- Model and Initial Results
- Convergence of Better-Response Dynamics
- Two-Sided Matching and Stable Marriage
- Dynamics with Memory
- References
- Regular Languages of Words over Countable Linear Orderings
- Introduction
- Preliminaries
- Semigroups and Algebras for Countable Linear Orderings
- From Monadic Second-Order Logic to -Algebras
- From -Algebras to Monadic Second-Order Logic
- Conclusion
- References
- Algebraic Independence and Blackbox Identity Testing
- Introduction
- Our Main Results
- Organization and Our Approach
- Preliminaries: Perron, Jacobi and Krull
- Perron's Criterion (Arbitrary Characteristic)
- Jacobi's Criterion (Large or Zero Characteristic)
- Krull Dimension of Affine Algebras
- Faithful Homomorphisms: Reducing the Variables
- A Kronecker-Inspired Map (Arbitrary Characteristic)
- A Vandermonde-Inspired Map (Large or Zero Characteristic)
- Circuits with Sparse Inputs of Low Transcendence Degree (Proving Theorem 1)
- Depth-4 Circuits with Bounded Top and Bottom Fanin
- Gcd, Simple Parts and the Rank Bounds
- Preserving the Simple Part (Towards Theorem 2)
- A Hitting Set (Proving Theorems 2 and 3)
- Conclusion
- References
- Session B1: Foundations of Program Semantics
- A Fragment of ML Decidable by Visibly Pushdown Automata
- Introduction
- RML, Game Semantics and Visibly Pushdown Automata
- Characterising the O-Strict Fragment of RML
- The O-Strict Fragment is VPA-Decidable
- Complexity
- References
- Krivine Machines and Higher-Order Schemes
- Introduction
- Basic Notions
- Game Over Configurations of the Krivine Machine
- Finite Game G(A,M)
- Equivalence of K(A,M) and G(A,M)
- Global Model Checking
- Conclusions
- References
- Relating Computational Effects by $\tau\tau$-Lifting
- Introduction
- The$\lambda$c-Calculus with Algebraic Operations
- Effect Simulation Problem
- Effect Simulation by Monad Morphism
- Comparing Two Monadic Semantics of ?-Calculus
- Extending $\lambda$c(B, $\Sigma$) with Recursive Functions
- Related Work
- References
- Constructing Differential Categories and Deconstructing Categories of Games
- Introduction
- Differential Categories and Resource PCF
- A Cartesian Closed Differential Category of Games
- Constructing Differential Categories
- Deconstructing Categories of Games
- Analysing Models of Resource PCF
- References
- Session B2: Automata and Formal Languages
- Nondeterminism Is Essential in Small 2FAs with Few Reversals
- Introduction
- Preparation
- Building Hard Instances
- Generic Strings
- Blocks
- The Proof
- The Hard Instances
- The Bound
- Conclusion
- References
- Isomorphism of Regular Trees and Words
- Introduction
- Preliminaries
- Trees
- Linear Orders and Generalized Words
- Isomorphism Problem for Regular Trees
- Isomorphism Problem for Regular Words
- Upper Bounds
- Lower Bounds for Regular Linear Orders
- Conclusion and Open Problems
- References
- On the Capabilities of Grammars, Automata, and Transducers Controlled by Monoids
- Introduction
- Basic Notions
- A Dichotomy of Monoids
- Capabilities of Valence Automata and Transducers
- Capabilities of Valence Grammars
- References
- The Cost of Traveling between Languages
- Introduction
- Problem Setting
- Asymptotic Cost in the Non-streaming Case
- Asymptotic Cost in the Streaming Case
- Conclusions
- References
- Session B3: Model Checking
- Emptiness and Universality Problems in Timed Automata with Positive Frequency
- Introduction
- Definitions and Preliminaries
- Timed Automata and Frequencies
- A Brief Comparison with Usual Semantics
- Set of Frequencies of Runs in One-Clock Timed Automata
- The Corner-Point Abstraction
- From A to AcpF, and Vice-Versa
- Set of Frequencies of Runs in A
- Emptiness and Universality Problems
- Conclusion
- References
- B\"{u}chi Automata Can Have Smaller Quotients
- Introduction
- Preliminaries
- Quotienting with Forward Simulations
- Fixed-Word Delayed Simulation
- Multipebble Fixed-Word Delayed Simulation
- Jumping-Safe Relations
- Refinement Transformers
- Delayed-Like Refinement Transformers
- Proxy Simulations
- Direct Proxy Simulation
- Delayed Proxy Simulation
- Conclusions and Future Work
- References
- Automata-Based CSL Model Checking
- Introduction
- Preliminaries
- Markov Chains
- Deterministic Finite Automata
- Continuous Stochastic Logic (CSL)
- Stratified CTMCs
- Usefulness of Stratification
- Product CTMC
- Automaton for a CSL Formula
- Product CTMC
- Computing Pr()
- Model Checking Algorithm
- Related Work
- Conclusion
- References
- A Progress Measure for Explicit-State Probabilistic Model-Checkers
- Introduction
- Probabilistic Transition Systems
- A Progress Measure
- Characterization of Progress for Invariants
- Computation of Progress for Invariants
- Conclusion
- References
- Session B4: Probabilistic Systems
- Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation
- Introduction
- Bisimulation and Simulation in PLTSs
- Shells
- Bisimulation as a Shell
- Simulation as a Shell
- A New Efficient Probabilistic Simulation Algorithm
- Future Work
- References
- On the Semantics of Markov Automata
- Introduction
- Markov Automata
- Composing Markov Automata
- Soundness and Completeness
- Conclusion and RelatedWork
- References
- Runtime Analysis of Probabilistic Programs with Unbounded Recursion
- Introduction
- Preliminaries
- TheResults
- Transforming pPDA into pBPA
- Analysis of pBPA
- Conclusions and Future Work
- References
- Approximating the Termination Value of One-Counter MDPs and Stochastic Games
- Introduction
- Definitions
- Main Result
- Proof Sketch
- Bounding Counter Value N for Maximizing OC-MDPs
- Bounding N for General SSGs
- References
- Session B5: Logic in Computer Science
- Generic Expression Hardness Results for Primitive Positive Formula Comparison
- Introduction
- Preliminaries
- Unary Type
- Algebra
- Reduction
- Non-congruence Modularity
- Algebra
- Reductions
- References
- Guarded Negation
- Introduction
- Preliminaries
- The Satisfiability Problem for GNFO
- The Satisfiability Problem for GNFP
- Additional Results
- Discussion
- References
- Locality of Queries Definable in Invariant First-Order Logic with Arbitrary Built-in Predicates
- Introduction
- Preliminaries
- Gaifman Locality
- Unary Formulas
- k-ary Formulas
- Hanf Locality
- Discussion
- References
- Modular Markovian Logic
- Introduction
- Preliminary Definitions
- Modular Markov Processes
- Synchronization
- Parallel Composition
- Modular Markovian Logic
- A Complete Hilbert-Style Axiomatization for MML
- Conclusions and Future Work
- References
- Session B6: Hybrid Systems
- Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
- Introduction
- A Nonstandard Analysis Primer
- Programming Language WHILE$^dt$
- Syntax
- Denotational Semantics
- Assertion Language ASSN$^dt$
- Program Logic HOARE$^dt$
- Verification with HOARE$^dt$
- References
- Model Checking the Quantitative $\mu$-Calculus on Linear Hybrid Systems
- Introduction
- Hybrid Systems and Quantitative Logics
- Quantitative -Calculus
- Interval Games
- Model Checking Games for Q
- Basic Properties of Interval Games
- Flattening Initialised Interval Games
- Multiplying Interval Games
- Discrete Strategies
- Choosing Discrete Moves
- Counter-Reset Games
- Conclusions and Future Work
- References
- On Reachability for Hybrid Automata over Bounded Time
- Introduction
- Definitions
- Decidability for RHA with Non-negative Rates
- Undecidability Results
- References
- Session B7: Specification and Verification
- Deciding Robustness against Total Store Ordering
- Introduction
- Programs, Memory Models, and Robustness
- Concurrent Programs
- Sequential Consistency and Total Store Ordering Semantics
- Traces
- Happens Before
- SC Characterisation of Violating TSO Computations
- Minimal Violating Computations
- From Many to Few: Locality of Reorderings
- From Few to SC: Variable Accesses and Main Result
- Complexity of Robustness
- Conclusion and Future Work
- References
- Multiply-Recursive Upper Bounds with Higman's Lemma
- Introduction
- Normed Wqo's and Controlled Bad Sequences
- An Algebra of Normed Wqo's
- Reflecting Residuals in Ordinal Arithmetic
- Classifying L Using Subrecursive Hierarchies
- Refined Complexity Bounds for Verification Problems
- Concluding Remarks
- References
- Liveness-Preserving Atomicity Abstraction
- Introduction
- Preliminaries
- Concurrent Library Semantics and Linearizability
- Atomicity Abstraction
- Linearization-Closed Properties
- Compositional Liveness Proofs for Concurrent Algorithms
- Example
- Related Work
- References
- On Stabilization in Herman's Algorithm
- Introduction
- Preliminaries
- Bounds on ET for Arbitrary Configurations
- Expressions for ET
- The Full Configuration
- Restabilization
- Conclusions and Future Work
- References
- Session C1: Graphs
- Online Graph Exploration: New Results on Old and New Algorithms
- Introduction
- The Exploration Algorithm of Kalyanasundaram and Pruhs
- A Lower Bound Construction
- Graphs with a Bounded Number of Distinct Weights
- Concluding Remarks
- References
- Distance Oracles for Vertex-Labeled Graphs
- Introduction
- Adaptation of Thorup-Zwick Oracles
- More Compact Oracles
- The Data Structure
- Vertex-Label Queries
- Construction
- Oracles Supporting Dynamic Labels
- The Data Structure
- Label Changes
- Vertex-Label Queries
- Small Stretch vs. Efficient Update/Space
- Discussion
- References
- Asymptotically Optimal Randomized Rumor Spreading
- Introduction
- The Protocol by Karp et al. [14]
- Our Results
- Disclaimers
- The Basic Protocol
- Running Time and Number of Calls
- Robustness against Random Node Failures
- Making the Protocol Robust against an Adversary
- References
- Fast Convergence for Consensus in Dynamic Networks
- Introduction
- Preliminary
- Convergence Model for Dynamic Networks
- Stochastic Matrices
- Static Weight Model: Limited Degree Variation and Well-Connected Dynamic Networks
- Analysis of the Uniform Averaging Model
- Weakly Connected Networks
- Random Networks
- Experiments
- References
- Session C2: Matchings and Equilibria
- Linear Programming in the Semi-streaming Model with Application to the Maximum Matching Problem
- Introduction
- The Multiplicative Weights Update Meta-method
- Warming Up: O(13logn)-Pass Algorithms
- Reducing Passes and Space Requirement
- Reducing Space Required to Run Parallel Guesses
- Removing the Dependency on n
- References
- Restoring Pure Equilibria to Weighted Congestion Games
- Introduction
- Preliminaries
- Weighted Network Cost-Sharing
- Atomic Selfish Routing
- Weighted Network Cost-Sharing
- Lower Bounding the Price of Stability
- Upper Bounding the Price of Stability
- Further Analysis of the Price of Stability
- Atomic Selfish Routing
- Upper Bounding the Price of Anarchy
- Lower Bounding the Price of Anarchy
- References
- Existence and Uniqueness of Equilibria for Flows over Time
- Introduction
- A Model for Dynamic Routing Games
- Flows over Time
- Label Functions for Flows over Time
- Equilibria
- Derivative of an Equilibrium Flow: A Special Labeling
- Existence of Thin Flows with Resetting
- Uniqueness of Thin Flows with Resetting
- Existence and Uniqueness of Equilibria for Flows over Time
- Existence for Piecewise Constant Inflow Rate
- Uniqueness for Piecewise Constant Inflow Rate
- Existence for General Inflow Rate
- References
- Collusion in Atomic Splittable Routing Games
- Introduction
- Preliminaries
- Proof of Lemma 1
- Characterizing Well-Designed Networks
- Constructing Nash Equilibria in Well-Designed Networks
- Comparing the Social Cost of Two Different Profiles
- References
- Session C3: Privacy and Content Search
- Privacy-Preserving Access of Outsourced Data via Oblivious RAM Simulation
- Introduction
- Preliminaries
- MapReduce Cuckoo Hashing
- Simulating a MapReduce Algorithm Obliviously
- Oblivious RAM Simulations
- References
- Adaptively Secure Non-interactive Threshold Cryptosystems
- Introduction
- Background and Definitions
- Definitions for Threshold Public Key Encryption
- Bilinear Maps and Hardness Assumptions
- A Non-interactive CCA2-Secure Threshold Cryptosystem with Adaptive Corruptions
- Description
- Security
- References
- Content Search through Comparisons
- Introduction
- Related Work
- Definitions and Notation
- Problem Statement
- Content Search Through Comparisons
- Small-World Network Design
- Main Results
- Proof of Theorem 2
- Proof of Theorem 4
- Conclusions
- References
- Session C4: Distributed Computation
- Efficient Distributed Communication in Ad-Hoc Radio Networks
- Introduction
- Preliminaries
- Building Blocks
- Breadth-Then-Depth Search (BTD)
- Computing Weights on a Tree
- Rumor Spreading on a Path
- Gathering Rumors
- Multi-Broadcast
- References
- Nearly Optimal Bounds for Distributed Wireless Scheduling in the SINR Model
- Introduction
- Preliminaries and Contributions
- Our Contributions and Related Work
- O(logn)-Approximate Distributed Scheduling Algorithm
- Bounding the Measure
- Duality and Acknowledgements
- $\Omega$(logn)-Factor Lower Bound for Distributed Scheduling
- References
- Convergence Time of Power-Control Dynamics
- Introduction
- Formal Problem Statement
- Related Work
- Convergence Time of the Foschini-Miljanic Iteration
- Power Control via Regret Learning
- Computing No-Swap-Regret Sequences
- Convergence of No-Swap-Regret Sequences
- Discussion and Open Problems
- References
- A New Approach for Analyzing Convergence Algorithms for Mobile Robots
- Introduction
- Our Contribution
- Ours and Other's Models
- Related Work
- Organization of the Paper
- Convergence Speed of d-inner Target Functions
- Convergence Speed in the Asynchronous LCM$\infty$ Model
- Convergence Speed in Asynchronous LCMS Model
- Runtime of the Center of Gravity Algorithm
- The Center of Minbox Algorithm
- Conclusion and Outlook
- References
- Author Index
