Mathematical Foundations of Computer Science 2002: 27th International Symposium, MFCS 2002, Warsaw, Poland, August 26-30, 2002. Proceedings (Lecture Notes in Computer Science, 2420)

This book constitutes the refereed proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science, MFCS 2002, held in Warsaw, Poland in August 2002. The 48 revised full papers presented together with 5 invited papers were carefully reviewed and selected from 108 submissions. All relevant aspects of theoretical computer science are addressed, ranging from discrete mathematics, combinatorial optimization, graph theory, algorithms, and complexity to programming theory, formal methods, and mathematical logic. Mathematical Foundations of Computer Science 2002 Preface Table of Contents Global Development via Local Observational Construction Steps* 1 Introduction 2 Signatures, Models and Specifications 3 Program Development and Refinements 4 Observational Equivalence 5 Observational Refinement Steps 6 Architectural Specifications 7 Observational Interpretation of Architectural Specifications 8 Conclusions and Further Work References Edge-Colouring Pairs of Binary Trees: Towards a Concise Proof of the Four-Colour Theorem of Planar Maps 1 Introduction 2 Preliminaries 3 Rotations and Colour-Constrained Trees 4 Colouring Topologies 5 Summary and Further Work References Applications of Finite Automata* 1 Introduction 2 Notation 3 Isomorphisms of F-Semigroups 4 Nonperiodic Tilings 5 Image Manipulation Acknowlegment References Approximability of the Minimum Bisection Problem: An Algorithmic Challenge 1 Introduction 2 Instances of MIN-BISECTION Problem 3 Dense Instances of MIN-BISECTION, Paired MIN-BISECTION, and MIN-2SAT 4 Planar Instances of MIN-BISECTION 5 Metric Instances of MIN-BISECTION 6 Sparse Instances of MIN-BISECTION 7 Summary of Known Approximation Results for MIN-BISECTION 8 Further Research Acknowledgments References Low Stretch Spanning Trees 1 Introduction 2 Low Stretch and Low Communication Trees 2.1 Low Stretch Trees 2.2 Low Communication Trees 3 Basic Properties 3.1 Hardness 3.2 Constructions and Bounds for General Graph Classes 4 Low Stretch Trees in Metric Spaces 4.1 Low-Distortion Embeddings in Metric Spaces 4.2 Probabilistic Approximation by Tree Metrics 5 MCT on Restricted Instances References On Radiocoloring Hierarchically Specified Planar Graphs: SSPACE -Completeness and Approximations 1 Introduction, Our Results and Related Work 1.1 Motivation 1.2 Summary of Our Results 1.3 Related Work and Comparison 2 Preliminaries 3 The Complexity of the Radiocoloring Problem 3.1 The NP-Completeness of RCP for Planar Graphs 3.2 The PSPACE-Completeness of RCP for Hierarchical Planar Graphs 4 Approximations to RCP for WS Fully Planar Graphs 4.1 A 4-Approximation Algorithm HRC_1 4.2 A 3-Approximation Algorithm HRC_2 References Finite Domain Constraint Satisfaction Using Quantum Computation 1 Introduction 2 Preliminaries 3 Algorithm for (d,2)-CSP 4 The Special Cases |D| = 3 and |D| = 5 5 Algorithm for 3-Colourability 5.1 Case 1: |G_u| = C . |G| 5.3 Complexity Analysis Acknowledgments References Fast Algorithms with Algebraic Monge Properties* 1 Introduction 2 Algorithms for Algebraic Shortest-Path Problems 3 Algorithms for the Bottleneck Shortest-Path Problems 4 An Alternate Algorithm for the Bottleneck k-Edge Shortest-Path 5 A Paragraph-Formation Problem 6 A Special Case of the Bottleneck Traveling-Salesman Problem References Packing Edges in Random Regular Graphs 1 Introduction 2 Lower Bounds 2.1 Dense Matchings 2.2 Sparse Matchings 3 The Upper Bounds References Appendix A Lower Bound Technique for Nondeterministic Graph-Driven Read-Once-Branching Programs and Its Applications 1 Introduction and Results 2 A Lower Bound Technique for Nondeterministic Graph-Driven BP1s 3 An Exponential Lower Bound for Integer Multiplication 4 Separating Well-Structured Nondeterministic Graph-Driven BP1s from Nondeterministic {textup {unhbox voidb @x hbox {BP1}}}s Acknowledgment References Matroid Intersections, Polymatroid Inequalities, and Related Problems* 1 Introduction 2 An Inequality for Polymatroid Functions 3 Applications 4 Proof of Theorem 2 5 Proper Mappings of Independent Sets into Binary Trees 6 Proof of Main Lemmas References Accessibility in Automata on Scattered Linear Orderings 1 Introduction 2 Words on Linear Orderings 2.1 Rational Words 3 Automata 4 A Pumping Lemma 5 Accessibility References On Infinite Terms Having a Decidable Monadic Theory 1 Introduction 2 A Hierarchy of Tree Families 3 A Hierarchy of Term Families 4 Conclusion References A Chomsky-Like Hierarchy of Infinite Graphs 1 Introduction 2 Preliminaries 3 Graphs Defined by String-Rewriting 4 Prefix-Recognizable Graphs 5 Rational Graphs 6 Recursively Enumerable Graphs 7 Conclusion References Competitive Analysis of On-line Stream Merging Algorithms 1 Introduction 2 Preliminaries 3.1 The α-Dyadic Schedule 3.1 The relax mathversion alpha-Dyadic Schedule 3.2 Analysis of the alpha-Dyadic Schedule 4 Maximum Bandwidth 4.1 Compact Point Sequence 4.2 The Connector Algorithm 4.3 Analysis of the Connector and the alpha-Dyadic Algorithms References Coloring k-Colorable Semirandom Graphs in Polynomial Expected Time via Semidefinite Programming 1 Introduction 2 A Semi-random Model for the Independent Set Problem 3 Preprocessing the Input via Semidefinite Programming 4 Finding Large Independent Sets 5 Coloring k-Colorable Graphs References On Word Equations in One Variable 1 Introduction 2 Preliminaries 3 Solutions 4 Verification References Autoreducibility of Random Sets: A Sharp Bound on the Density of Guessed Bits 1 Introduction 1.1 Notation 2 Random Sets 3 Autoreducibility 4 Autoreducing Random Sets: Negative Results on Density 5 Autoreducing Random Sets: Positive Results on Density Acknowledgments References Two-Way Finite State Transducers with Nested Pebbles 1 Introduction 2 Decomposition and Composition 3 Hierarchy of Transductions 4 Hierarchy of Output Languages Acknowledgement References Optimal Non-preemptive Semi-online Scheduling on Two Related Machines 1 Introduction 2 The Function 3 Analysis of the Overall Competitive Ratio 4 Properties and Assumptions 5 New Algorithms 5.1 The First Four Intervals 5.2 Intervals 9 and 10, 13 and 14 5.3 Intervals 11 and 12 6 Matching Lower Bounds 7 Conclusion References More on Weighted Servers or FIFO is Better than LRU 1 Introduction 2 Marking Algorithms 3 Two Servers 4 Lower Bounds for Trackless Algorithms References On Maximizing the Throughput of Multiprocessor Tasks* 1 Introduction 2 Scheduling Parallel Tasks 3 Scheduling Dedicated Tasks 4 Conclusions Acknowledgment References Some Results on Random Unsatisfiable k-Sat Instances and Approximation Algorithms Applied to Random Structures Introduction 1 Certifying Discrepancy Properties of Random Graphs 2 Certifying Discrepancy Properties of Random Uniform Hypergraphs 3 Applications to Random Unsatisfiable k-Sat Instances 4 Approximation Algorithms Applied to Random Instances Conclusions References Evolutive Tandem Repeats Using Hamming Distance 1 Introduction 2 Preliminaries 3 Global vs Local: The Evolutive Repeats 3.1 Definitions 3.2 The Real Evolutive Tandem Repeats 4 Algorithms 4.1 Equivalence Classes of Positions 4.2 E_l-Class Graph 4.3 l-Position Graph 4.4 Longest Path 4.5 Conclusion 5 Improvement: Progressive Computation of the Distances 6 Conclusion References Subgraph Isomorphism, log-Bounded Fragmentation and Graphs of (Locally) Bounded Treewidth* 1 Introduction 2 Preliminaries 3 General Dynamic-Programming Approach for Graphs of Bounded Treewidth 4 Subgraph Isomorphism for log-Bounded Fragmentation Graphs 5 Extension to Graphs of Locally Bounded Treewidth 6 Conclusions and Future Work Acknowledgments References Computing Partial Information out of Intractable One - The First Digit of 2n at Base 3 as an Example* 1 Introduction 2 Preliminaries 3 The Algorithms 4 Validity of the Algorithms 5 Conclusion Acknowledgement References Algorithms for Computing Small NFAs 1 Introduction 2 Basic Notions 3 Position Automata 4 Partial Derivative Automata 5 Follow Automata 6 Basic Idea for Reducing Arbitrary NFAs 7 Computing Inequivalent States 8 Merging the States of A_(pos) 9 Examples 10 Reducing NFAs in Both Directions 11 Conclusions and Further Research References Space-Economical Construction of Index Structures for All Suffixes of a String 1 Introduction 2 Minimum All-Suffixes Directed Acyclic Word Graphs 3 Minimum All-Suffixes Compact Directed Acyclic Word Graphs 4 Concluding Remarks References An Explicit Lower Bound of 5n-o(n) for Boolean Circuits 1 Introduction 2 Boolean Circuits over U_2 3 Basic Ideas 4 Strongly Two Dependent Boolean Functions 5 The Lower Bound 5.1 The Lower Bound 5.2 Preliminaries for the Proof of Lemma 5.1 5.3 Proof of Lemma 5.1 Acknowledgment References Computational Complexity in the Hyperbolic Plane 1 Introduction 2 Cellular Automata in the Hyperbolic Plane 2.1 Tiling of the Hyperbolic Plane 2.2 Fibonacci Trees 2.3 Hyperbolic CA 3 Main Results 4 Deterministic Simulation of Nondeterministic HCA 4.1 Basic Properties of NHCA 4.2 Deterministic Algorithm Using Binary Tree Structure 5 Time Hierarchy of Hyperbolic Cellular Automata 5.1 Language Not Accepted by t_1(n)-Time NHCA 5.2 DHCA Accepting the Language L(t_1(n)) 6 Space Hierarchy of Hyperbolic Cellular Automata References On a Mereological System for Relational Software Specifications* 1 Introduction 2 Grids 3 Mereological Systems 4 Mereological Systems for Direct Products 5 Final Comment Acknowledgement References An Optimal Lower Bound for Resolution with 2-Conjunctions* 1 Introduction 2 Definitions and Results 3 Width of Restricted Res(2)-Proofs 4 Existence of Useful Graphs References Improved Parameterized Algorithms for Planar Dominating Set* 1 Introduction 2 Preliminaries and Background 3 A Note on Baker's Algorithm 4 Separation of Non-shallow Components 4.1 Middle Triples 4.2 Lower Triples 4.3 Upper Triples 5 The Algorithm References Optimal Free Binary Decision Diagrams for Computation of EARn 1 Introduction 2 Definitions and Notation 3 Upper Bound 4 Lower Bound 4.1 Notation Used in the Lower Bound Proof 4.2 Adversary Strategy 4.3 Analysis of the Strategy 4.4 The Bound Acknowledgement References Unification Modulo Associativity and Idempotency Is NP-complete* 1 Introduction 2 Preliminaries 3 Simple AIU-Unification Problem 4 Conclusion Acknowledgments References On the Complexity of Semantic Equivalences for Pushdown Automata and BPA 1 Introduction 2 Lower Bounds 3 Upper Bounds 4 Conclusions References An Improved Algorithm for the Membership Problem for Extended Regular Expressions 1 Introduction 2 Definitions 2.1 Extended Regular Expressions 2.2 Alternating Automata with Synchronized Universality 2.3 Alternating Automata with Synchronized Universality and Negation 3 ASUN for ERE 4 The Membership Problem References Efficient Algorithms for Locating the Length-Constrained Heaviest Segments, with Applications to Biomolecular Sequence Analysis 1 Introduction 2 Maximum Sum Consecutive Subsequence with Length Constraints 3 Maximum Average Consecutive Subsequence with Length Constraints 4 Implementation and Preliminary Experiments 5 Concluding Remarks Acknowledgements References Derivation of Rational Expressions with Multiplicity 1 Introduction 2 Rational Expressions with Multiplicity 3 Derivatives 4 Derived Terms 5 The Automaton of Derived Terms 6 Shadow Derived Terms 7 Further Developments References Hypothesis-Founded Semantics for Datalog Programs with Negation 1 Introduction 2 Preliminaries 2.1 Well-Founded Semantics 2.2 Kripke-Kleene Semantics 3 Hypothesis Testing 3.1 The Support of a Hypothesis 4 Hypothesis Founded Semantics 5 Concluding Remarks References On the Problem of Scheduling Flows on Distributed Networks* 1 Introduction 2 Definitions 3 Worst-Case Analysis for Distributed Scheduling Strategies 4 The Distributed Algorithm 4.1 Flow Graphs (G,l,f) on Tree Networks with Directed Tree G 4.2 Arbitrary Flow Graphs (G,l,f) on Tree Networks 5 Conclusion Acknowledgment References Unit Testing for C88 ASL Architectural Specifications 1 Introduction 2 Preliminary Definitions 3 Formal Testing from Algebraic Specifications 4 Testing from Non-generic Unit Specifications 5 Testing from Generic Unit Specifications 6 Concluding Remarks Acknowledgments References Symbolic Semantics and Analysis for Crypto-CCS with (Almost) Generic Inference Systems* 1 Introduction 2 Crypto-CCS: An Operational Language for the Description of Cryptographic Protocols 2.1 Messages and Inference Systems 2.2 Agents and Systems 2.3 Symbolic Operational Semantics 3 Symbolic Analysis 4 Security Analysis: The Most General Intruder Approach Acknowledgments References The Complexity of Tree Multicolorings 1 Introduction 2 Preliminaries 3 The Penalty Gadgets 4 The Reduction Acknowledgments References On Verifying Fair Lossy Channel Systems 1 Introduction 2 Channel Systems 2.1 (Perfect) Channel Systems 2.2 Lossy Channel Systems 2.3 Fair Scheduling 2.4 Communication Layouts 3 Fair Termination without Multiplexed Channel 4 Weakly Fair Termination for Single-Channel Systems 5 Classifying Communication Layouts 6 Other Verification Problems with Fair Scheduling 7 Conclusions References Parameterized Counting Problems 1 Introduction 2 Classical Counting Problems and #P 3 #W[1] - A Parameterized Counting Class 3.1 A Definition for #W[1] 3.2 A Fundamental Complete Problem for #W[1] 4 Populating #W[1] 5 Conclusions References On the Construction of Effective Random Sets 1 Introduction 1.1 Notation 1.2 Reducibilities 2 Random Sets 3 Every Set Is Reducible to a Martin-Löf Random Set 4 Selfreductions of Martin-Löf Random Sets and Computably Enumerable Reals 5 Autoreductions of Rec-random Sets Acknowledgments References On the Structure of the Simulation Order of Proof Systems 1 Introduction 2 Preliminaries 3 Basic Observations 4 Presentability 5 The Embedding Theorem 6 Conclusion References Comorphism-Based Grothendieck Logics 1 Introduction and Motivation 2 Institutions, Logics, Morphisms and Comorphisms 3 Grothendieck Institutions and Logics 4 Heterogeneous Development Graphs 5 Conclusion and Related Work Acknowledgments References Finite Test-Sets for Overlap-Free Morphisms 1 Introduction 2 Words and Morphisms 3 Test-Sets for Overlap-Freeness 4 Binary Morphisms 5 Non-binary Morphisms 6 Uniform Non-binary Morphisms 7 Uniform Binary Morphisms 8 Test-Words Acknowledgment References Characterizing Simpler Recognizable Sets of Integers 1 Introduction 2 Characterization of Star-Free Languages 3 Numeration Systems 3.1 Syntax of Logical Formulas in L_(2,n) 4 Base Dependence 4.1 The Case of Ultimately Periodic Sets 5 k-adic Number Systems Acknowledgments References Towards a Cardinality Theorem for Finite Automata 1 Introduction 1.1 History of the Cardinality Theorem 1.2 Finite Automata and the Cardinality Theorem 1.3 Reformulations of the Cardinality Theorem 2 Finite Automata Versions of the Cardinality Theorem 3 Regular Relations and Cardinality Computations 4 Counter-example to a Theorem of Kinber 5 Conclusion Acknowledgements References An Approximation Semantics for the Propositional Mu-Calculus* 1 Introduction 2 Approximation Semantics 3 Sequent Calculus 4 Some Examples of the Proof System References Author Index

This book constitutes the refereed proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science, MFCS 2002, held in Warsaw, Poland in August 2002.
The 48 revised full papers presented together with 5 invited papers were carefully reviewed and selected from 108 submissions. All relevant aspects of theoretical computer science are addressed, ranging from discrete mathematics, combinatorial optimization, graph theory, algorithms, and complexity to programming theory, formal methods, and mathematical logic.

There has been a great deal of work in the algebraic specification tradition on formalizing the rather intuitive and appealing idea of program development by stepwise refinement, including [EKMP82,Gan83,GM82,Sch87,ST88b]; for a recent survey, see [EK99]).