Automata, Languages, and Programming
39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II
Published on 24. June 2012
700 pages
978-3-642-31585-5 (ISBN)
Description
This two-volume set of LNCS 7391 and LNCS 7392 constitutes the refereed proceedings of the 39th International Colloquium on Automata, Languages and Programming, ICALP 2012, held in Warwick, UK, in July 2012.
The total of 123 revised full papers presented in this volume were carefully reviewed and selected from 432 submissions. They are organized in three tracks focussing on algorithms, complexity and games; logic, semantics, automata and theory of programming; and foundations of networked computation.
More details
Other editions
Additional editions
Artur Czumaj | Kurt Mehlhorn | Andrew Pitts
Automata, Languages, and Programming
39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II
Book
07/2012
Springer
€53.49
Shipment within 7-9 days
Content
- Title Page
- Preface
- Organization
- Table of Contents
- Invited Talks
- On Multiple Keyword Sponsored Search Auctions with Budgets
- Introduction
- Problem Statement and Definitions
- Deterministic Clinching Auction for the Divisible Case
- Characterization of Pareto Optimality
- Multiple Keyword Auction for the Divisible Case
- Randomized Clinching Auction for the Indivisible Case
- The Combinatorial Case with Multiple Slots
- Impossibility for Diminishing Marginal Valuations
- References
- A Theory Independent Curry-De Bruijn-Howard Correspondence
- References
- Standing on the Shoulders of a Giant
- References
- Session Types and Distributed Computing
- Algorithms, Graph Theory, and the Solution of Laplacian Linear Equations
- References
- Randomized Mechanisms for Multi-unit Auctions
- References
- Track B - Logic Semantics, Automata and Theory of Programming
- Algebraic Synchronization Trees and Processes
- Introduction
- Continuous Categorical Algebras
- Synchronization Trees
- Algebraic Objects and Functors
- Comparing the Expressiveness of Classes of Recursion Schemes
- Branch Languages of Bounded Synchronization Trees
- References
- Streaming Tree Transducers
- Introduction
- Transducer Model
- Properties and Variants
- Expressiveness
- Decision Problems
- References
- Causal Graph Dynamics
- Introduction
- Graphs Dynamics
- Causal Dynamics
- Localizable Dynamics
- Properties
- Future Work
- References
- Degree Lower Bounds of Tower-Type for Approximating Formulas with Parity Quantifiers
- Introduction
- Preliminaries
- Fooling Polynomials of Low Degree
- Defining a Linear Pre-order of Width Two
- The Lower Bound and Final Remarks
- References
- Monadic Datalog Containment
- Introduction
- Background
- Monadic Datalog Containment in General
- Reducing the Complexity
- Equivalence of Nodes in Tree-Like Instances
- Global Restrictions and Diversified Instances
- Conclusions and Related Work
- References
- A Machine-Independent Characterization of Timed Languages
- Introduction
- Timed Register Automata
- Fraenkel-Mostowski Sets and Their Automata
- Characterization of Deterministic Timed Automata
- Future Work
- References
- Regular Languages of Infinite Trees That Are Boolean Combinations of Open Sets
- Introduction
- A Game Characterization
- Preliminaries on Trees
- Tree Languages and Algebra
- Boolean Combinations of Open Sets of Trees
- The Infinite Game
- The Effective Characterization
- Conclusion
- References
- Toward Model Theory with Data Values
- Introduction
- Preliminaries
- Relational Structures
- Logic
- Definition of FM First-Order Logic
- Elimination of Orbit-Finite Disjunction
- Standard Data Words
- Functionality and Locality
- Conclusions
- References
- Robust Reachability in Timed Automata: A Game-Based Approach
- Introduction
- Robust Reachability in Timed Automata
- Timed Automata and Robust Reachability
- Motivating Example: Robust Real-Time Scheduling
- Related Work: Robustness in Timed Automata and Games
- Shrinking DBMs
- Regions, Zones and DBMs
- Shrinking
- Shrunk DBMs
- Shrinking constraints
- Neighborhoods
- Two Crucial Properties for the Construction of the Abstraction
- A Finite Game Abstraction
- Conclusion
- References
- Minimizing Expected Termination Time in One-Counter Markov Decision Processes
- Introduction
- Preliminaries
- Upper Bounds
- Strongly Connected OC-MDP
- General OC-MDP
- Lower Bounds
- References
- Prefix Rewriting for Nested-Words and Collapsible Pushdown Automata
- Introduction
- Prefix Rewriting on Nested-Words
- Nested-Words
- Prefix and Suffix Rewriting
- (C)PDA Graphs
- Higher-Order Stacks
- Collapsible Pushdown Stacks
- The Automata and Their Graphs
- Characterising 2-(C)PDA Graphs as Prefix Rewrite Systems
- From Rewrite Systems to 2-(C)PDA
- (Tree) Isophilic and Dendrisophilic Structures
- From (C)PDA to Rewrite Systems
- First-Order Logic on 3{2}-CPDA Graphs
- Further Directions
- References
- A Saturation Method for Collapsible Pushdown Systems
- Introduction
- Preliminaries
- Annotated Pushdown Systems
- Regularity of Annotated Stacks
- Algorithm
- Notation and Conventions
- The Saturation Function
- Correctness and Complexity
- Perspectives
- References
- Regular Languages Are Church-Rosser Congruential
- Introduction
- Preliminaries
- Finite Groups
- Groups without Proper Cyclic Quotient Groups
- The General Case for Group Languages
- Arbitrary Finite Monoids
- The Main Result
- Conclusion
- References
- Time and Parallelizability Results for Parity Games with Bounded Treewidth
- Introduction
- Preliminaries
- Strategy Profiles
- Time Complexity Results for Parity Games
- Parity Games with Bounded Treewidth Are In NC$^ 2$
- References
- Nominal Completion for Rewrite Systems with Binders
- Introduction
- Preliminaries
- Reduction Orderings for Nominal Terms
- Completion for Nominal Rewriting Systems
- Conclusions
- References
- Discrete Generalised Polynomial Functors
- Introduction
- Generalised Logic
- Polynomial Functors
- Generalised Polynomial Functors
- Discrete Generalised Polynomial Functors
- Equational Systems
- Applications
- Nominal Effects
- Abstract Syntax
- Dependent Programming
- References
- Computing Game Metrics on Markov Decision Processes
- Introduction
- Markov Decision Processes
- Game Metrics on Markov Decision Processes
- Approximations of the Game Metrics
- Complexity for the Undiscounted Metric
- Conclusion and Related Work
- References
- Deciding First Order Properties of Matroids
- Introduction
- Notation
- Tree-Width and Local Tree-Width
- Matroids
- Matroid Algorithms
- Branch-Width and Local Branch-Width
- FO and MSO Properties
- Local Tree-Width vs. Local Branch-Width
- Constructing Gaifman Graph
- Deciding First Order Properties
- References
- Pebble Games with Algebraic Rules
- Introduction
- Preliminaries
- A Game Characterisation of Rank Logics
- Playing with Invertible Linear Maps
- Invertible-Map Game
- Complexity of the Game Equivalence
- Application to the Graph Isomorphism Problem
- Discussion
- References
- Exponential Lower Bounds and Separation for Query Rewriting
- Introduction
- Queries over $OWL2QL$ Ontologies
- Boolean Circuits, CNFs and OBDA
- Rewritings Long and Short
- Conclusion
- References
- Lattices of Logical Fragments over Words
- Introduction
- Preliminaries
- Fragments and C-Varieties
- Stutter-Invariant Piecewise Testable Languages
- The Acyclic Fragment of $\sum_ 2$
- References
- On the Expressive Power of Cost Logics over Infinite Words
- Introduction
- Related Work and Motivation
- Notation
- Contributions
- Cost Logics
- Cost First-Order Logic
- Cost Monadic Second-Order Logic
- Cost Weak Monadic Second-Order Logic
- Link with Languages
- Cost Linear Temporal Logic
- Cost Automata on Infinite Words
- B-Valuation
- B- and S-Automata
- Weak Automata.
- Very-Weak Automata.
- First-Order Fragment
- CFO to CLTL
- B-VWAA to CLTL
- Expressive Completeness of CWMSO
- B-NBA to B-WAA
- Conclusion
- References
- Coalgebraic Predicate Logic
- Introduction
- Syntax, Semantics and Examples
- Completeness
- Correspondence with Coalgebraic Modal Logic
- Beginning Model Theory
- Conclusions and Further Work
- References
- Algorithmic Games for Full Ground References
- Introduction
- GRef
- Game Semantics
- Undecidability Arguments
- Decidability
- References
- Two-Level Game Semantics, Intersection Types, and Recursion Schemes
- Introduction
- Two Structures of Intersection Type System
- Two-Level Game Semantics
- Interpretation of Intersection Types
- Applications to HORS Model-Checking
- References
- An Automata-Theoretic Model of Idealized Algol
- Introduction
- Motivation
- The Semantic Framework
- Stores as Automata
- Semantics
- Conclusion
- References
- Towards a Unified Theory of Operational and Axiomatic Semantics
- Introduction
- Operational Semantics, Reduction Rules, and Transition Systems
- Matching Logic Patterns
- Matching Logic Reachability
- Sound Proof System
- Implementation in MatchC
- Conclusion, Additional Related Work, and Future Work
- References
- Loader and Urzyczyn Are Logically Related
- Preliminaries: Some Syntax, Some Semantics
- Typed Lambda Calculi
- Type Structures Modelling the Simply Typed Lambda Calculus
- Uniform Intersection Types and CDV
- The Continuous Model over $ P(X)$
- Inhabitation Reduces to Definability
- Definability Reduces to Inhabitation
- References
- Languages of Profinite Words and the Limitedness Problem
- Introduction
- Preliminaries
- Languages of Profinite Words
- Recognizable Languages
- The Main Results
- From Infinite Words to Profinite Words
- References
- The Complexity of Mean-Payoff Automaton Expression
- Introduction
- Mean-Payoff Automaton Expression
- PSPACE Algorithm for Computing the Maximum Value of max-free Expressions
- The Emptiness Problem for Intersection of LimSupAvg Automata
- The Emptiness Problem for Intersection of LimInfAvg Automata
- The Emptiness Problem for Intersection of LimSupAvg and LimInfAvg Automata
- The Emptiness Problem for max-free Expressions
- PSPACE Algorithm for the Emptiness Problem of max-free Expressions
- The Complexity of Mean-Payoff Expression Problems
- Conclusion and Future Work
- References
- Track C - Foundations of Networked Computation
- On the Locality of Some NP-Complete Problems
- Introduction
- The Model
- Problems and Results
- The Difficulty of Solving NP-Complete Problems Locally
- Our Techniques
- Related Work
- Preliminaries
- Approximating Minimum-Coloring Using Network Decompositions
- Computing Network Decompositions
- Partitioning Procedure
- Network-Decompositions in Graphs with Bounded Degree
- Network-Decompositions in Graphs with Small Dominating Set
- References
- Growing Half-Balls: Minimizing Storage and Communication Costs in CDNs
- Introduction
- Preliminaries
- Online Algorithm for General Networks
- Approximation Algorithm for the Grid Network
- References
- Super-Fast Distributed Algorithms for Metric Facility Location
- Introduction
- Results
- Overview of Technical Contributions
- Reduction to the O(1)-Ruling Set Problem
- A New Lower Bound for Non-uniform Metric Facility Location
- Algorithm
- Analysis
- Computing a 2-Ruling Set
- A Useful Subroutine
- Algorithm
- Analysis
- Conclusions
- References
- Preventing Unraveling in Social Networks: The Anchored k-Core Problem
- Introduction
- General Graphs
- Anchored 2-Core
- Inapproximability of k 3
- Graphs with Bounded Treewidth
- The Algorithm
- Concluding Remarks
- References
- Edge Fault Tolerance on Sparse Networks
- Introduction
- Model, Definitions and Building Blocks
- A.E. Agreement on Low-Degree Networks
- A.e. Agreement on O(Vn log n)-Degree Graphs
- A.e. Agreement on O(n^{\epsilon} )-Degree Graphs
- References
- Incentive Ratios of Fisher Markets
- Introduction
- Related Work
- Preliminary
- Incentive Ratio
- Linear Utility Functions
- Cobb-Douglas Utility Functions
- Manipulation on Endowments
- Reductions on Market Sizes
- Incentive Ratio
- Conclusions
- References
- Computational Complexity of Traffic Hijacking under BGP and S-BGP
- Introduction and Overview
- A Model for BGP Routing
- Understanding Hacking Strategies
- Checking If an Origin-Spoofing BGP Attack Exists
- S-BGP Gives Hackers Hard Times
- Conclusions and Open Problems
- References
- Efficiency-Revenue Trade-Offs in Auctions
- Introduction
- Our Results
- Related Work
- Preliminaries
- Bayesian Mechanism Design
- Multi-objective Optimization
- The Complexity of Pareto Optimal Auctions
- An FPTAS for 2 Bidders
- An Algorithm for the Exact Version of Bi-Criterion Auction
- The Case of n Bidders
- Open Questions
- References
- Deterministic Network Exploration by Anonymous Silent Agents with Local Traffic Reports
- Introduction
- Preliminaries
- An Auxiliary Algorithm: Exploration with Tokens
- The Main Algorithm
- Analysis of the Algorithm
- References
- AQPTAS for e-Envy-Free Profit-Maximizing Pricing on Line Graphs
- Introduction
- The Highway Problem
- Hierarchical Decomposition for Line Semi-metrics
- Basic Definitions
- Basic Hierarchical Decomposition for Line Semi-metrics
- Refined Hierarchical Decomposition for Line Semi-metrics
- A Dynamic Program for -Envy Free Pricing
- Restricting the Search Space for Pricing
- Restricting the Search Space for the Consumed Capacities
- Dynamic Program for the Limited Supply Case
- References
- Minimizing Rosenthal Potential in Multicast Games
- Introduction
- Preliminaries
- Minimizing Rosenthal Potential
- Intractability of Local Search for Rosenthal Potential
- References
- Multiparty Proximity Testing with Dishonest Majority from Equality Testing
- Introduction
- Preliminaries, Model and Privacy Definition
- n-Party PET with an Honest-But-Curious Server
- Homomorphic PET Schemes
- Private Homomorphic PET against Malicious Adversaries
- Realizing PET via PAKE
- References
- Anonymous Card Shuffling and Its Applications to Parallel Mixnets
- Introduction
- Previous Related Work
- Our Results
- Anonymity Measures
- Algorithms and Analysis
- Extensions to Mixnets with Corrupted Servers
- Extensions to Mixnets with Corrupted Inputs
- Extensions to Mixnets with Corrupted Servers and Inputs
- Conclusion and Open Problems
- References
- Byzantine Agreement with a Rational Adversary
- Introduction
- Our Results
- Related Work
- Byzantine Agreement
- Rational Byzantine Agreement
- Rational Byzantine Agreement: Basic Results
- Feasibility Assuming Complete Knowledge
- Feasibility with Partial Knowledge
- References
- Random Hyperbolic Graphs: Degree Sequence and Clustering
- Introduction
- Model and Results
- Properties of the Model
- Proofs of the Main Results
- The Clustering Coefficient
- References
- Topology-Aware VM Migration in Bandwidth Oversubscribed Datacenter Networks
- Introduction
- The Constrained Migration Problem (CoMP)
- Relieving a Single Hot Spot (Single Source CoMP)
- Converting a Fractional Migration from a Single Hot Server
- Multiflows on a Directed Tree
- Total Unimodularity (TUM) of the Routing Constraints in T*
- All-or-Nothing with Multiple Servers in Directed Trees
- Maximum throughput and b-Matched Multiflows
- References
- Counting Arbitrary Subgraphs in Data Streams
- Introduction
- An Unbiased Estimator for Counting Subgraphs
- Analysis of the Estimator
- Extensions
- References
- k-Chordal Graphs: From Cops and Robber to Compact Routing via Treewidth
- Introduction
- Our Results
- Related Work
- A Detour through Cops and Robber Games
- Structured Tree-Decomposition
- Application of k-Good Tree-Decompositions for Routing
- Model and Performance of the Routing Scheme
- Data Structures
- Routing Algorithm in k-Good Tree-Decomposable Graphs
- Conclusion and Further Work
- References
- Contention Issues in Congestion Games
- Introduction
- Nash Equilibria of the Boat Model
- Nash Equilibria of the Conveyor Belt Model
- References
- Online Mechanism Design (Randomized Rounding on the Fly)
- Introduction
- Formal Description of the Problem
- Our Contribution
- The Overselling MPU Algorithm
- The MPU Algorithm with Oblivious Randomized Rounding
- Analysis for CAs with Bundles of Bounded Cardinality
- Algorithm for General CAs with Multiplicity
- Analysis for CAs with XOS Valuations
- Truthful Mechanisms for Different Kind of Arrivals
- References
- Online Packing with Gradually Improving Capacity Estimations and Applications to Network Lifetime Maximization
- Introduction
- Model for the Competitive Analysis
- New Results
- Lifetime Maximization for Sensor Networks
- Related Work
- Competitiveness of the GREEDY-Algorithm
- The EQUITABLE-Algorithm
- Competitiveness of EQUITABLE
- Upper Bound on the Competitiveness of EQUITABLE
- AnO(1/Va) Upper Bound on Packing Spanning Trees
- A Deterministic Upper Bound
- An Upper Bound on Randomized Algorithms
- Conclusion
- References
- Distributed Algorithms for Network Diameter and Girth
- Introduction
- Exact All-Pairs of Shortest Paths and Diameter
- An Approximation Algorithm for the Diameter
- Approximating the Girth
- References
- Author Index
