@inproceedings{4435, abstract = {An important case of hybrid systems are the rectangular automata. First, rectangular dynamics can naturally and arbitrarily closely approximate more general, nonlinear dynamics. Second, rectangular automata are the most general type of hybrid systems for which model checking -in particular, Ltl model checking- is decidable. However, on one hand, the original proofs of decidability did not suggest practical algorithms and, on the other hand, practical symbolic model-checking procedures -such as those implemented in HyTech- were not known to terminate on rectangular automata. We remedy this unsatisfactory situation: we present a symbolic method for Ltl model checking which can be performed by HyTech and is guaranteed to terminate on all rectangular automata. We do so by proving that our method for symbolic Ltl model checking terminates on an infinite-state transition system if the trace-equivalence relation of the system has finite index, which is the case for all rectangular automata.}, author = {Henzinger, Thomas A and Majumdar, Ritankar}, booktitle = {Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783540672821}, location = {Berlin, Germany}, pages = {142 -- 156}, publisher = {Springer}, title = {{Symbolic model checking for rectangular hybrid systems}}, doi = {10.1007/3-540-46419-0_11}, volume = {1785}, year = {2000}, } @inproceedings{4439, abstract = {We define five increasingly comprehensive classes of infinite-state systems, called STS1–5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems. STS1 These are the systems with finite bisimilarity quotients. They can be analyzed symbolically by (1) iterating the predecessor and boolean operations starting from a finite set of observable state sets, and (2) terminating when no new state sets are generated. This enables model checking of the μ-calculus. STS2 These are the systems with finite similarity quotients. They can be analyzed symbolically by iterating the predecessor and positive boolean operations. This enables model checking of the existential and universal fragments of the μ-calculus. STS3 These are the systems with finite trace-equivalence quotients. They can be analyzed symbolically by iterating the predecessor operation and a restricted form of positive boolean operations (intersection is restricted to intersection with observables). This enables model checking of linear temporal logic. STS4 These are the systems with finite distance-equivalence quotients (two states are equivalent if for every distance d, the same observables can be reached in d transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new state sets are generated. This enables model checking of the existential conjunction-free and universal disjunction-free fragments of the μ-calculus. STS5 These are the systems with finite bounded-reachability quotients (two states are equivalent if for every distance d, the same observables can be reached in d or fewer transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new states are encountered. This enables model checking of reachability properties.}, author = {Henzinger, Thomas A and Majumdar, Ritankar}, booktitle = {Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science}, isbn = {9783540671411}, location = {Lille, France}, pages = {13 -- 34}, publisher = {Springer}, title = {{A classification of symbolic transition systems}}, doi = {10.1007/3-540-46541-3_2}, volume = {1770}, year = {2000}, } @inproceedings{4481, abstract = {Since hybrid embedded systems are pervasive and often safety-critical, guarantees about their correct performance are desirable. The hybrid systems model checker HyTech provides such guarantees and has successfully verified some systems. However, HyTech severely restricts the continuous dynamics of the system being analyzed and, therefore, often forces the use of prohibitively expensive discrete and polyhedral abstractions. We have designed a new algorithm, which is capable of directly verifying hybrid systems with general continuous dynamics, such as linear and nonlinear differential equations. The new algorithm conservatively overapproximates the reachable states of a hybrid automaton by using interval numerical methods. Interval numerical methods return sets of points that enclose the true result of numerical computation and, thus, avoid distortions due to the accumulation of round-off errors. We have implemented the new algorithm in a successor tool to HyTech called HyperTech. We consider three examples: a thermostat with delay, a two-tank water system, and an air-traffic collision avoidance protocol. HyperTech enables the direct, fully automatic analysis of these systems, which is also more accurate than the use of polyhedral abstractions.}, author = {Henzinger, Thomas A and Horowitz, Benjamin and Majumdar, Ritankar and Wong Toi, Howard}, booktitle = {Proceedings of the 3rd International Workshop on Hybrid Systems}, isbn = {9783540672593}, location = {Pittsburgh, PA, USA}, pages = {130 -- 144}, publisher = {Springer}, title = {{Beyond HyTech: Hybrid systems analysis using interval numerical methods}}, doi = {10.1007/3-540-46430-1_14}, volume = {1790}, year = {2000}, } @inproceedings{4482, abstract = {We apply the theory of abstract interpretation to the verification of game properties for reactive systems. Unlike properties expressed in standard temporal logics, game properties can distinguish adversarial from collaborative relationships between the processes of a concurrent program, or the components of a parallel system. We consider two-player concurrent games –say, component vs. environment– and specify properties of such games –say, the component has a winning strategy to obtain a resource, no matter how the environment behaves– in the alternating-time μ-calculus (Aμ ). A sound abstraction of such a game must at the same time restrict the behaviors of the component and increase the behaviors of the environment: if a less powerful component can win against a more powerful environment, then surely the original component can win against the original environment. We formalize the concrete semantics of a concurrent game in terms of controllable and uncontrollable predecessor predicates, which suffice for model checking all Aμ properties by applying boolean operations and iteration. We then define the abstract semantics of a concurrent game in terms of abstractions for the controllable and uncontrollable predecessor predicates. This allows us to give general characterizations for the soundness and completeness of abstract games with respect to Aμ properties. We also present a simple programming language for multi-process programs, and show how approximations of the maximal abstraction (w.r.t. Aμ properties) can be obtained from the program text. We apply the theory to two practical verification examples, a communication protocol developed at the Berkeley Wireless Research Center, and a protocol converter. In the wireless protocol, both the use of a game property for specification and the use of abstraction for automatic verification were instrumental to uncover a subtle bug.}, author = {Henzinger, Thomas A and Majumdar, Ritankar and Mang, Freddy and Raskin, Jean}, booktitle = {Proceedings of the 7th International Symposium on Static Analysis}, isbn = {9783540676683}, location = {Santa Barbara, CA, USA}, pages = {220 -- 239}, publisher = {Springer}, title = {{Abstract interpretation of game properties}}, doi = {10.1007/978-3-540-45099-3_12}, volume = {1824}, year = {2000}, } @inproceedings{4483, abstract = {Model-checking algorithms can be used to verify, formally and automatically, if a low-level description of a design conforms with a high-level description. However, for designs with very large state spaces, prior to the application of an algorithm, the refinement-checking task needs to be decomposed into subtasks of manageable complexity. It is natural to decompose the task following the component structure of the design. However, an individual component often does not satisfy its requirements unless the component is put into the right context, which constrains the inputs to the component. Thus, in order to verify each component individually, we need to make assumptions about its inputs, which are provided by the other components of the design. This reasoning is circular: component A is verified under the assumption that context B behaves correctly, and symmetrically, B is verified assuming the correctness of A. The assume-guarantee paradigm provides a systematic theory and methodology for ensuring the soundness of the circular style of postulating and discharging assumptions in component-based reasoning.We give a tutorial introduction to the assume-guarantee paradigm for decomposing refinement-checking tasks. To illustrate the method, we step in detail through the formal verification of a processor pipeline against an instruction set architecture. In this example, the verification of a three-stage pipeline is broken up into three subtasks, one for each stage of the pipeline.}, author = {Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram}, booktitle = {Proceedings of the 2000 International Conference on Computer-Aided Design}, isbn = {0780364457}, location = {San Jose, CA, USA}, pages = {245 -- 252}, publisher = {IEEE}, title = {{Decomposing refinement proofs using assume-guarantee reasoning}}, doi = {10.1109/ICCAD.2000.896481}, year = {2000}, } @inproceedings{4512, abstract = {Masaccio is a formal model for hybrid dynamical systems which are built from atomic discrete components (difference equations) and atomic continuous components (differential equations) by parallel and serial composition, arbitrarily nested. Each system component consists of an interface, which determines the possible ways of using the component, and a set of executions, which define the possible behaviors of the component in real time. Version 1.0 (May 2000). }, author = {Henzinger, Thomas A}, booktitle = {Proceedings of the 1st International Conference on Theoretical Computer Science }, isbn = {9783540678236}, location = {Sendai, Japan}, pages = {549 -- 563}, publisher = {Springer}, title = {{Masaccio: A formal model for embedded components}}, doi = {10.1007/3-540-44929-9_38}, volume = {1872}, year = {2000}, } @inbook{4513, abstract = {A hybrid automaton is a formal model for a mixed discrete-continuous system. We classify hybrid automata according to what questions about their behavior can be answered algorithmically. The classification reveals structure on mixed discrete-continuous state spaces that was previously studied on purely discrete state spaces only. In particular, various classes of hybrid automata induce finitary trace equivalence (or similarity, or bisimilarity) relations on an uncountable state space, thus permitting the application of various model-checking techniques that were originally developed for finitestate systems. }, author = {Henzinger, Thomas A}, booktitle = {Verification of Digital and Hybrid Systems}, editor = {Inan, M. and Kurshan, Robert}, isbn = {9783642596155}, pages = {265 -- 292}, publisher = {Springer}, title = {{The theory of hybrid automata}}, doi = {10.1007/978-3-642-59615-5}, volume = {170}, year = {2000}, } @article{4598, abstract = {A hybrid system is a dynamical system with both discrete and continuous state changes. For analysis purposes, it is often useful to abstract a system in a way that preserves the properties being analyzed while hiding the details that are of no interest. We show that interesting classes of hybrid systems can be abstracted to purely discrete systems while preserving all properties that are definable in temporal logic. The classes that permit discrete abstractions fall into two categories. Either the continuous dynamics must be restricted, as is the case for timed and rectangular hybrid systems, or the discrete dynamics must be restricted, as is the case for o-minimal hybrid systems. In this paper, we survey and unify results from both areas.}, author = {Alur, Rajeev and Henzinger, Thomas A and Lafferriere, Gerardo and Pappas, George}, issn = {0018-9219}, journal = {Proceedings of the IEEE}, number = {7}, pages = {971 -- 984}, publisher = {IEEE}, title = {{Discrete abstractions of hybrid systems}}, doi = {10.1109/5.871304 }, volume = {88}, year = {2000}, } @inproceedings{4627, abstract = {We consider two-player games, which are played on a finite state space for an infinite number of rounds. The games are concurrent, that is, in each round, the two players choose their moves independently and simultaneously; the current state and the two moves determine a successor state. We consider omega-regular winning conditions on the resulting infinite state sequence. To model the independent choice of moves, both players are allowed to use randomization for selecting their moves. This gives rise to the following qualitative modes of winning, which can be studied without numerical considerations concerning probabilities: sure-win (player 1 can ensure winning with certainty), almost-sure-win (player 1 can ensure winning with probability 1), limit-win (player 1 can ensure winning with probability arbitrarily close to 1), bounded-win (player 1 can ensure winning with probability bounded away from 0), positive-win (player 1 can ensure winning with positive probability), and exist-win (player 1 can ensure that at least one possible outcome of the game satisfies the winning condition).We provide algorithms for computing the sets of winning states for each of these winning modes. In particular, we solve concurrent Rabin-chain games in n0 (m) time, where n is the size of the game structure and m is the number of pairs in the Rabin-chain condition. While this complexity is in line with traditional turn-based games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games are. This is because concurrent games violate two of the most fundamental properties of turn-based games. First, concurrent games are not determined, but rather exhibit a more general duality property, which involves multiple modes of winning. Second, winning strategies for concurrent games may require infinite memory.}, author = {De Alfaro, Luca and Henzinger, Thomas A}, booktitle = {Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science}, isbn = {0769507255}, location = {Santa Barbara, CA, USA}, pages = {141 -- 154}, publisher = {IEEE}, title = {{Concurrent omega-regular games}}, doi = {10.1109/LICS.2000.855763}, year = {2000}, } @inproceedings{4637, abstract = {In the synchronous composition of processes, one process may prevent another process from proceeding unless compositions without a well-defined product behavior are ruled out. They can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping processes with types, which make the dependencies between input and output signals transparent. We classify various typing mechanisms and study their effects on the control problem. A static type enforces fixed, acyclic dependencies between input and output ports. For example, synchronous hardware without combinational loops can be typed statically. A dynamic type may vary the dependencies from state to state, while maintaining acyclicity, as in level-sensitive latches. Then, two dynamically typed processes can be syntactically compatible, if all pairs of possible dependencies are compatible, or semantically compatible, if in each state the combined dependencies remain acyclic. For a given plant process and control objective, there may be a controller of a static type, or only a controller of a syntactically compatible dynamic type, or only a controller of a semantically compatible dynamic type. We show this to be a strict hierarchy of possibilities, and we present algorithms and determine the complexity of the corresponding control problems. Furthermore, we consider versions of the control problem in which the type of the controller (static or dynamic) is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions}, author = {De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy}, booktitle = {Proceedings of the 11th International Conference on Concurrency Theory}, isbn = {9783540678977}, location = {University Park, PA, USA}, pages = {458 -- 473}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{The control of synchronous systems}}, doi = {10.1007/3-540-44618-4_33}, volume = {1877}, year = {2000}, } @inproceedings{4638, abstract = {Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counterexample) rather than success (a correctness proof). We present a method for symbolic model checking that can lead to significant time and memory savings for model-checking runs that fail, while occurring only a small overhead for model-checking runs that succeed. Our method discovers an error as soon as it cannot be prevented, which can be long before it actually occurs; for example, the violation of an invariant may become unpreventable many transitions before the invariant is violated. The key observation is that “unpreventability” is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. Therefore, unpreventability is inexpensive to compute for each module, yet can save much work in the state exploration of the global, compound system. Based on different degrees of information available about the environment, we define and implement several notions of “unpreventability,” including the standard notion of uncontrollability from discrete-event control. We present experimental results for two examples, a distributed database protocol and a wireless communication protocol.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy}, booktitle = {Proceedings of the 12th International Conference on Computer Aided Verification}, isbn = {9783540677703}, location = {Chicago, IL, USA}, pages = {186 -- 201}, publisher = {Springer}, title = {{Detecting errors before reaching them}}, doi = {10.1007/10722167_17}, volume = {1855}, year = {2000}, } @article{8526, author = {Kaloshin, Vadim}, issn = {0003-486X}, journal = {The Annals of Mathematics}, keywords = {Statistics, Probability and Uncertainty, Statistics and Probability}, number = {2}, pages = {729--741}, publisher = {JSTOR}, title = {{An extension of the Artin-Mazur theorem}}, doi = {10.2307/121093}, volume = {150}, year = {1999}, } @article{883, abstract = {Sympatric speciation, the origin of two or more species from a single local population, has almost certainly been involved in formation of several species flocks, and may be fairly common in nature. The most straightforward scenario for sympatric speciation requires disruptive selection favouring two substantially different phenotypes, and consists of the evolution of reproductive isolation between them followed by the elimination of all intermediate phenotypes. Here we use the hypergeometric phenotypic model to show that sympatric speciation is possible even when fitness and mate choice depend on different quantitative traits, so that speciation must involve formation of covariance between these traits. The increase in the number of variable loci affecting fitness facilitates sympatric speciation, whereas the increase in the number of variable loci affecting mate choice has the opposite effect. These predictions may enable more cases of sympatric speciation to be identified.}, author = {Kondrashov, Alexey and Kondrashov, Fyodor}, issn = {0028-0836}, journal = {Nature}, number = {6742}, pages = {351 -- 354}, publisher = {Nature Publishing Group}, title = {{Interactions among quantitative traits in the course of sympatric speciation}}, doi = {10.1038/22514}, volume = {400}, year = {1999}, } @article{11679, abstract = {We are given a set T = {T 1 ,T 2 , . . .,T k } of rooted binary trees, each T i leaf-labeled by a subset L(Ti)⊂{1,2,...,n} . If T is a tree on {1,2, . . .,n }, we let T|L denote the minimal subtree of T induced by the nodes of L and all their ancestors. The consensus tree problem asks whether there exists a tree T * such that, for every i , T∗|L(Ti) is homeomorphic to T i . We present algorithms which test if a given set of trees has a consensus tree and if so, construct one. The deterministic algorithm takes time min{O(N n 1/2 ), O(N+ n 2 log n )}, where N=∑i|Ti| , and uses linear space. The randomized algorithm takes time O(N log3 n) and uses linear space. The previous best for this problem was a 1981 O(Nn) algorithm by Aho et al. Our faster deterministic algorithm uses a new efficient algorithm for the following interesting dynamic graph problem: Given a graph G with n nodes and m edges and a sequence of b batches of one or more edge deletions, then, after each batch, either find a new component that has just been created or determine that there is no such component. For this problem, we have a simple algorithm with running time O(n 2 log n + b 0 min{n 2 , m log n }), where b 0 is the number of batches which do not result in a new component. For our particular application, b0≤1 . If all edges are deleted, then the best previously known deterministic algorithm requires time O(mn−−√) to solve this problem. We also present two applications of these consensus tree algorithms which solve other problems in computational evolutionary biology.}, author = {Henzinger, Monika H and King, V. and Warnow, T.}, issn = {1432-0541}, journal = {Algorithmica}, keywords = {Algorithms, Data structures, Evolutionary biology, Theory of databases}, pages = {1--13}, publisher = {Springer Nature}, title = {{Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology}}, doi = {10.1007/pl00009268}, volume = {24}, year = {1999}, } @article{11687, abstract = {When using traditional search engines, users have to formulate queries to describe their information need. This paper discusses a different approach to Web searching where the input to the search process is not a set of query terms, but instead is the URL of a page, and the output is a set of related Web pages. A related Web page is one that addresses the same topic as the original page. For example, www.washingtonpost.com is a page related to www.nytimes.com, since both are online newspapers. We describe two algorithms to identify related Web pages. These algorithms use only the connectivity information in the Web (i.e., the links between pages) and not the content of pages or usage information. We have implemented both algorithms and measured their runtime performance. To evaluate the effectiveness of our algorithms, we performed a user study comparing our algorithms with Netscape's `What's Related' service (http://home.netscape.com/escapes/related/). Our study showed that the precision at 10 for our two algorithms are 73% better and 51% better than that of Netscape, despite the fact that Netscape uses both content and usage pattern information in addition to connectivity information.}, author = {Dean, Jeffrey and Henzinger, Monika H}, issn = {1389-1286}, journal = {Computer Networks}, keywords = {Search engines, Related pages, Searching paradigms}, number = {11-16}, pages = {1467--1479}, publisher = {Elsevier}, title = {{Finding related pages in the world wide Web}}, doi = {10.1016/s1389-1286(99)00022-5}, volume = {31}, year = {1999}, } @article{11688, abstract = {Recent research has studied how to measure the size of a search engine, in terms of the number of pages indexed. In this paper, we consider a different measure for search engines, namely the quality of the pages in a search engine index. We provide a simple, effective algorithm for approximating the quality of an index by performing a random walk on the Web, and we use this methodology to compare the index quality of several major search engines.}, author = {Henzinger, Monika H and Heydon, Allan and Mitzenmacher, Michael and Najork, Marc}, issn = {1389-1286}, journal = {Computer Networks}, keywords = {Search engines, Index quality, Random walks, PageRank}, number = {11-16}, pages = {1291--1303}, publisher = {Elsevier}, title = {{Measuring index quality using random walks on the web}}, doi = {10.1016/s1389-1286(99)00016-x}, volume = {31}, year = {1999}, } @inproceedings{11691, abstract = {In this paper we consider the online ftp problem. The goal is to service a sequence of file transfer requests given bandwidth constraints of the underlying communication network. The main result of the paper is a technique that leads to algorithms that optimize several natural metrics, such as max-stretch, total flow time, max flow time, and total completion time. In particular, we show how to achieve optimum total flow time and optimum max-stretch if we increase the capacity of the underlying network by a logarithmic factor. We show that the resource augmentation is necessary by proving polynomial lower bounds on the max-stretch and total flow time for the case where online and offline algorithms are using same-capacity edges. Moreover, we also give polylogarithmic lower bounds on the resource augmentation factor necessary in order to keep the total flow time and max-stretch within a constant factor of optimum.}, author = {Goel, Ashish and Henzinger, Monika H and Plotkin, Serge and Tardos, Eva}, booktitle = {Proceedings of the 31st annual ACM symposium on Theory of computing}, issn = {0196-6774}, keywords = {Scheduling, Flow time}, location = { Atlanta, GA, United States}, pages = {189--197}, publisher = {Association for Computing Machinery}, title = {{Scheduling data transfers in a network and the set scheduling problem}}, doi = {10.1145/301250.301300}, year = {1999}, } @article{11769, abstract = {This paper solves a longstanding open problem in fully dynamic algorithms: We present the first fully dynamic algorithms that maintain connectivity, bipartiteness, and approximate minimum spanning trees in polylogarithmic time per edge insertion or deletion. The algorithms are designed using a new dynamic technique that combines a novel graph decomposition with randomization. They are Las-Vegas type randomized algorithms which use simple data structures and have a small constant factor. Let n denote the number of nodes in the graph. For a sequence of Ω(m0) operations, where m0 is the number of edges in the initial graph, the expected time for p updates is O(p log3 n) (througout the paper the logarithms are based 2) for connectivity and bipartiteness. The worst-case time for one query is O(log n/log log n). For the k-edge witness problem (“Does the removal of k given edges disconnect the graph?”) the expected time for p updates is O(p log3 n) and the expected time for q queries is O(qk log3 n). Given a graph with k different weights, the minimum spanning tree can be maintained during a sequence of p updates in expected time O(pk log3 n). This implies an algorithm to maintain a 1 + ε-approximation of the minimum spanning tree in expected time O((p log3 n logU)/ε) for p updates, where the weights of the edges are between 1 and U.}, author = {Henzinger, Monika H and King, Valerie}, issn = {1557-735X}, journal = {Journal of the ACM}, number = {4}, pages = {502--516}, publisher = {Association for Computing Machinery}, title = {{Randomized fully dynamic graph algorithms with polylogarithmic time per operation}}, doi = {10.1145/320211.320215}, volume = {46}, year = {1999}, } @article{11895, abstract = {In this paper we present an analysis of an AltaVista Search Engine query log consisting of approximately 1 billion entries for search requests over a period of six weeks. This represents almost 285 million user sessions, each an attempt to fill a single information need. We present an analysis of individual queries, query duplication, and query sessions. We also present results of a correlation analysis of the log entries, studying the interaction of terms within queries. Our data supports the conjecture that web users differ significantly from the user assumed in the standard information retrieval literature. Specifically, we show that web users type in short queries, mostly look at the first 10 results only, and seldom modify the query. This suggests that traditional information retrieval techniques may not work well for answering web search requests. The correlation analysis showed that the most highly correlated items are constituents of phrases. This result indicates it may be useful for search engines to consider search terms as parts of phrases even if the user did not explicitly specify them as such.}, author = {Silverstein, Craig and Marais, Hannes and Henzinger, Monika H and Moricz, Michael}, issn = {0163-5840}, journal = {ACM SIGIR Forum}, number = {1}, pages = {6--12}, publisher = {Association for Computing Machinery}, title = {{Analysis of a very large web search engine query log}}, doi = {10.1145/331403.331405}, volume = {33}, year = {1999}, } @inproceedings{11925, abstract = {This paper studies the multicast routing and admission control problem on unit-capacity tree and mesh topologies in the throughput-model. The problem is a generalization of the edge-disjoint paths problem and is NPhard both on trees and meshes. We study both the offline and the online version of the problem: In the offline setting, we give the first constant-factor approximation algorithm for trees, and an O((log log n)*)-factor approximation algorithm for meshes, where n is the number of nodes in the graph. In the online setting, we give the first polylogarithrnic competitive online algorithm for tree and mesh topologies. No polylogarithmic-competitive algorithm is possible on general network topologies [8] and there exists a polylogarithmic lower bound on the competitive ratio of any online algorithm on tree topologies [l]. We prove the same lower bound for meshes. }, author = {Henzinger, Monika H and Leonardi , Stefano}, booktitle = {10th Annual ACM-SIAM Symposium on Discrete Algorithms}, isbn = {0898714346}, location = {Baltimore, MD, United States}, pages = {438--447}, publisher = {Society for Industrial & Applied Mathematics}, title = {{Scheduling multicasts on unit-capacity trees and meshes}}, year = {1999}, }