[{"author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"}],"conference":{"end_date":"2000-04-02","start_date":"2000-03-25","location":"Berlin, Germany","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"year":"2000","publication_identifier":{"isbn":["9783540672821"]},"publisher":"Springer","day":"01","doi":"10.1007/3-540-46419-0_11","oa_version":"None","quality_controlled":"1","publication_status":"published","abstract":[{"lang":"eng","text":"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."}],"publist_id":"293","language":[{"iso":"eng"}],"status":"public","citation":{"ieee":"T. A. Henzinger and R. Majumdar, “Symbolic model checking for rectangular hybrid systems,” in Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Berlin, Germany, 2000, vol. 1785, pp. 142–156.","short":"T.A. Henzinger, R. Majumdar, in:, Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2000, pp. 142–156.","apa":"Henzinger, T. A., & Majumdar, R. (2000). Symbolic model checking for rectangular hybrid systems. In Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 1785, pp. 142–156). Berlin, Germany: Springer. https://doi.org/10.1007/3-540-46419-0_11","mla":"Henzinger, Thomas A., and Ritankar Majumdar. “Symbolic Model Checking for Rectangular Hybrid Systems.” Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 1785, Springer, 2000, pp. 142–56, doi:10.1007/3-540-46419-0_11.","ista":"Henzinger TA, Majumdar R. 2000. Symbolic model checking for rectangular hybrid systems. Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1785, 142–156.","ama":"Henzinger TA, Majumdar R. Symbolic model checking for rectangular hybrid systems. In: Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol 1785. Springer; 2000:142-156. doi:10.1007/3-540-46419-0_11","chicago":"Henzinger, Thomas A, and Ritankar Majumdar. “Symbolic Model Checking for Rectangular Hybrid Systems.” In Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 1785:142–56. Springer, 2000. https://doi.org/10.1007/3-540-46419-0_11."},"type":"conference","date_published":"2000-01-01T00:00:00Z","article_processing_charge":"No","date_updated":"2023-04-18T13:08:09Z","title":"Symbolic model checking for rectangular hybrid systems","month":"01","_id":"4435","date_created":"2018-12-11T12:08:50Z","publication":"Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","page":"142 - 156","acknowledgement":"This research was supported in part by the DARPA (NASA) grant NAG2-1214, the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660, the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","intvolume":" 1785","alternative_title":["LNCS"],"volume":1785,"scopus_import":"1","extern":"1"},{"date_created":"2018-12-11T12:08:51Z","_id":"4439","page":"13 - 34","publication":"Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science","article_processing_charge":"No","date_published":"2000-01-01T00:00:00Z","month":"01","title":"A classification of symbolic transition systems","date_updated":"2023-04-18T13:02:39Z","extern":"1","scopus_import":"1","intvolume":" 1770","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"This research was supported in part by the DARPA (NASA) grant NAG2-1214, the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660, the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.","alternative_title":["LNCS"],"volume":1770,"day":"01","publisher":"Springer","oa_version":"None","doi":"10.1007/3-540-46541-3_2","conference":{"name":"STACS: Theoretical Aspects of Computer Science","location":"Lille, France","start_date":"2000-02-17","end_date":"2000-02-19"},"year":"2000","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"}],"publication_identifier":{"isbn":["9783540671411"]},"citation":{"ama":"Henzinger TA, Majumdar R. A classification of symbolic transition systems. In: Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science. Vol 1770. Springer; 2000:13-34. doi:10.1007/3-540-46541-3_2","chicago":"Henzinger, Thomas A, and Ritankar Majumdar. “A Classification of Symbolic Transition Systems.” In Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, 1770:13–34. Springer, 2000. https://doi.org/10.1007/3-540-46541-3_2.","ista":"Henzinger TA, Majumdar R. 2000. A classification of symbolic transition systems. Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science. STACS: Theoretical Aspects of Computer Science, LNCS, vol. 1770, 13–34.","mla":"Henzinger, Thomas A., and Ritankar Majumdar. “A Classification of Symbolic Transition Systems.” Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, vol. 1770, Springer, 2000, pp. 13–34, doi:10.1007/3-540-46541-3_2.","apa":"Henzinger, T. A., & Majumdar, R. (2000). A classification of symbolic transition systems. In Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science (Vol. 1770, pp. 13–34). Lille, France: Springer. https://doi.org/10.1007/3-540-46541-3_2","short":"T.A. Henzinger, R. Majumdar, in:, Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, Springer, 2000, pp. 13–34.","ieee":"T. A. Henzinger and R. Majumdar, “A classification of symbolic transition systems,” in Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, 2000, vol. 1770, pp. 13–34."},"type":"conference","quality_controlled":"1","status":"public","language":[{"iso":"eng"}],"publist_id":"292","abstract":[{"text":"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.\r\nSTS1 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.\r\nSTS2 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.\r\nSTS3 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.\r\nSTS4 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.\r\nSTS5 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.","lang":"eng"}],"publication_status":"published"},{"author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"first_name":"Benjamin","full_name":"Horowitz, Benjamin","last_name":"Horowitz"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar","first_name":"Ritankar"},{"first_name":"Howard","full_name":"Wong Toi, Howard","last_name":"Wong Toi"}],"year":"2000","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2000-03-25","location":"Pittsburgh, PA, USA","start_date":"2000-03-23"},"publication_identifier":{"isbn":["9783540672593"]},"day":"01","publisher":"Springer","oa_version":"None","doi":"10.1007/3-540-46430-1_14","quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","abstract":[{"lang":"eng","text":"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."}],"publication_status":"published","publist_id":"247","type":"conference","citation":{"ama":"Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. Beyond HyTech: Hybrid systems analysis using interval numerical methods. In: Proceedings of the 3rd International Workshop on Hybrid Systems. Vol 1790. Springer; 2000:130-144. doi:10.1007/3-540-46430-1_14","chicago":"Henzinger, Thomas A, Benjamin Horowitz, Ritankar Majumdar, and Howard Wong Toi. “Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods.” In Proceedings of the 3rd International Workshop on Hybrid Systems, 1790:130–44. Springer, 2000. https://doi.org/10.1007/3-540-46430-1_14.","mla":"Henzinger, Thomas A., et al. “Beyond HyTech: Hybrid Systems Analysis Using Interval Numerical Methods.” Proceedings of the 3rd International Workshop on Hybrid Systems, vol. 1790, Springer, 2000, pp. 130–44, doi:10.1007/3-540-46430-1_14.","ista":"Henzinger TA, Horowitz B, Majumdar R, Wong Toi H. 2000. Beyond HyTech: Hybrid systems analysis using interval numerical methods. Proceedings of the 3rd International Workshop on Hybrid Systems. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 1790, 130–144.","apa":"Henzinger, T. A., Horowitz, B., Majumdar, R., & Wong Toi, H. (2000). Beyond HyTech: Hybrid systems analysis using interval numerical methods. In Proceedings of the 3rd International Workshop on Hybrid Systems (Vol. 1790, pp. 130–144). Pittsburgh, PA, USA: Springer. https://doi.org/10.1007/3-540-46430-1_14","short":"T.A. Henzinger, B. Horowitz, R. Majumdar, H. Wong Toi, in:, Proceedings of the 3rd International Workshop on Hybrid Systems, Springer, 2000, pp. 130–144.","ieee":"T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong Toi, “Beyond HyTech: Hybrid systems analysis using interval numerical methods,” in Proceedings of the 3rd International Workshop on Hybrid Systems, Pittsburgh, PA, USA, 2000, vol. 1790, pp. 130–144."},"date_published":"2000-01-01T00:00:00Z","article_processing_charge":"No","month":"01","date_updated":"2023-04-18T12:44:52Z","title":"Beyond HyTech: Hybrid systems analysis using interval numerical methods","date_created":"2018-12-11T12:09:04Z","_id":"4481","page":"130 - 144","publication":"Proceedings of the 3rd International Workshop on Hybrid Systems","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"This research was supported in part by the DARPA (NASA) grant NAG2-1214, the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.","intvolume":" 1790","alternative_title":["LNCS"],"volume":1790,"scopus_import":"1","extern":"1"},{"month":"01","title":"Abstract interpretation of game properties","date_updated":"2023-04-18T12:49:56Z","date_published":"2000-01-01T00:00:00Z","article_processing_charge":"No","page":"220 - 239","publication":"Proceedings of the 7th International Symposium on Static Analysis","date_created":"2018-12-11T12:09:04Z","_id":"4482","volume":1824,"alternative_title":["LNCS"],"acknowledgement":"This research was supported in part by the DARPA (NASA) grant NAG2-1214, the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660, the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","intvolume":" 1824","scopus_import":"1","extern":"1","publication_identifier":{"isbn":["9783540676683"]},"author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"first_name":"Freddy","full_name":"Mang, Freddy","last_name":"Mang"},{"full_name":"Raskin, Jean","last_name":"Raskin","first_name":"Jean"}],"conference":{"end_date":"2000-07-06","start_date":"2000-06-29","location":"Santa Barbara, CA, USA","name":"SAS: Static Analysis Symposium"},"year":"2000","oa_version":"None","doi":"10.1007/978-3-540-45099-3_12","day":"01","publisher":"Springer","language":[{"iso":"eng"}],"status":"public","abstract":[{"lang":"eng","text":"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.\r\nWe 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."}],"publication_status":"published","publist_id":"248","quality_controlled":"1","citation":{"ista":"Henzinger TA, Majumdar R, Mang F, Raskin J. 2000. Abstract interpretation of game properties. Proceedings of the 7th International Symposium on Static Analysis. SAS: Static Analysis Symposium, LNCS, vol. 1824, 220–239.","mla":"Henzinger, Thomas A., et al. “Abstract Interpretation of Game Properties.” Proceedings of the 7th International Symposium on Static Analysis, vol. 1824, Springer, 2000, pp. 220–39, doi:10.1007/978-3-540-45099-3_12.","chicago":"Henzinger, Thomas A, Ritankar Majumdar, Freddy Mang, and Jean Raskin. “Abstract Interpretation of Game Properties.” In Proceedings of the 7th International Symposium on Static Analysis, 1824:220–39. Springer, 2000. https://doi.org/10.1007/978-3-540-45099-3_12.","ama":"Henzinger TA, Majumdar R, Mang F, Raskin J. Abstract interpretation of game properties. In: Proceedings of the 7th International Symposium on Static Analysis. Vol 1824. Springer; 2000:220-239. doi:10.1007/978-3-540-45099-3_12","ieee":"T. A. Henzinger, R. Majumdar, F. Mang, and J. Raskin, “Abstract interpretation of game properties,” in Proceedings of the 7th International Symposium on Static Analysis, Santa Barbara, CA, USA, 2000, vol. 1824, pp. 220–239.","apa":"Henzinger, T. A., Majumdar, R., Mang, F., & Raskin, J. (2000). Abstract interpretation of game properties. In Proceedings of the 7th International Symposium on Static Analysis (Vol. 1824, pp. 220–239). Santa Barbara, CA, USA: Springer. https://doi.org/10.1007/978-3-540-45099-3_12","short":"T.A. Henzinger, R. Majumdar, F. Mang, J. Raskin, in:, Proceedings of the 7th International Symposium on Static Analysis, Springer, 2000, pp. 220–239."},"type":"conference"},{"extern":"1","type":"conference","citation":{"apa":"Henzinger, T. A., Qadeer, S., & Rajamani, S. (2000). Decomposing refinement proofs using assume-guarantee reasoning. In Proceedings of the 2000 International Conference on Computer-Aided Design (pp. 245–252). San Jose, CA, USA: IEEE. https://doi.org/10.1109/ICCAD.2000.896481","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 2000 International Conference on Computer-Aided Design, IEEE, 2000, pp. 245–252.","ieee":"T. A. Henzinger, S. Qadeer, and S. Rajamani, “Decomposing refinement proofs using assume-guarantee reasoning,” in Proceedings of the 2000 International Conference on Computer-Aided Design, San Jose, CA, USA, 2000, pp. 245–252.","chicago":"Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Decomposing Refinement Proofs Using Assume-Guarantee Reasoning.” In Proceedings of the 2000 International Conference on Computer-Aided Design, 245–52. IEEE, 2000. https://doi.org/10.1109/ICCAD.2000.896481.","ama":"Henzinger TA, Qadeer S, Rajamani S. Decomposing refinement proofs using assume-guarantee reasoning. In: Proceedings of the 2000 International Conference on Computer-Aided Design. IEEE; 2000:245-252. doi:10.1109/ICCAD.2000.896481","mla":"Henzinger, Thomas A., et al. “Decomposing Refinement Proofs Using Assume-Guarantee Reasoning.” Proceedings of the 2000 International Conference on Computer-Aided Design, IEEE, 2000, pp. 245–52, doi:10.1109/ICCAD.2000.896481.","ista":"Henzinger TA, Qadeer S, Rajamani S. 2000. Decomposing refinement proofs using assume-guarantee reasoning. Proceedings of the 2000 International Conference on Computer-Aided Design. ICCAD: Computer-Aided Design, 245–252."},"status":"public","language":[{"iso":"eng"}],"publist_id":"249","abstract":[{"lang":"eng","text":"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."}],"publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"Supported in part by DARPA Information Technology Office, by the MARC0 Gigascale Silicon Research Center, and by the National Science Foundation. ","quality_controlled":"1","page":"245 - 252","oa_version":"None","publication":"Proceedings of the 2000 International Conference on Computer-Aided Design","doi":"10.1109/ICCAD.2000.896481","day":"01","date_created":"2018-12-11T12:09:05Z","publisher":"IEEE","_id":"4483","month":"01","publication_identifier":{"isbn":["0780364457"]},"title":"Decomposing refinement proofs using assume-guarantee reasoning","date_updated":"2023-04-18T12:57:52Z","conference":{"name":"ICCAD: Computer-Aided Design","location":"San Jose, CA, USA","start_date":"2000-11-05","end_date":"2000-11-09"},"year":"2000","article_processing_charge":"No","date_published":"2000-01-01T00:00:00Z","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"first_name":"Sriram","last_name":"Rajamani","full_name":"Rajamani, Sriram"}]},{"publisher":"Springer","day":"01","doi":"10.1007/3-540-44929-9_38","oa_version":"None","year":"2000","conference":{"location":"Sendai, Japan","start_date":"2000-08-17","end_date":"2000-08-19","name":"TCS: Theoretical Computer Science"},"author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"publication_identifier":{"isbn":["9783540678236"]},"citation":{"apa":"Henzinger, T. A. (2000). Masaccio: A formal model for embedded components. In Proceedings of the 1st International Conference on Theoretical Computer Science (Vol. 1872, pp. 549–563). Sendai, Japan: Springer. https://doi.org/10.1007/3-540-44929-9_38","short":"T.A. Henzinger, in:, Proceedings of the 1st International Conference on Theoretical Computer Science , Springer, 2000, pp. 549–563.","ieee":"T. A. Henzinger, “Masaccio: A formal model for embedded components,” in Proceedings of the 1st International Conference on Theoretical Computer Science , Sendai, Japan, 2000, vol. 1872, pp. 549–563.","chicago":"Henzinger, Thomas A. “Masaccio: A Formal Model for Embedded Components.” In Proceedings of the 1st International Conference on Theoretical Computer Science , 1872:549–63. Springer, 2000. https://doi.org/10.1007/3-540-44929-9_38.","ama":"Henzinger TA. Masaccio: A formal model for embedded components. In: Proceedings of the 1st International Conference on Theoretical Computer Science . Vol 1872. Springer; 2000:549-563. doi:10.1007/3-540-44929-9_38","mla":"Henzinger, Thomas A. “Masaccio: A Formal Model for Embedded Components.” Proceedings of the 1st International Conference on Theoretical Computer Science , vol. 1872, Springer, 2000, pp. 549–63, doi:10.1007/3-540-44929-9_38.","ista":"Henzinger TA. 2000. Masaccio: A formal model for embedded components. Proceedings of the 1st International Conference on Theoretical Computer Science . TCS: Theoretical Computer Science, LNCS, vol. 1872, 549–563."},"type":"conference","quality_controlled":"1","publist_id":"215","publication_status":"published","abstract":[{"text":"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.\r\nVersion 1.0 (May 2000).\r\n","lang":"eng"}],"status":"public","language":[{"iso":"eng"}],"_id":"4512","date_created":"2018-12-11T12:09:14Z","publication":"Proceedings of the 1st International Conference on Theoretical Computer Science ","page":"549 - 563","article_processing_charge":"No","date_published":"2000-01-01T00:00:00Z","title":"Masaccio: A formal model for embedded components","date_updated":"2023-04-13T13:48:08Z","month":"01","extern":"1","scopus_import":"1","intvolume":" 1872","acknowledgement":"This research was supported in part by the DARPA grants NAG2-1214 and F33615-C-98-3614, and by the MARCO grant 98-DT-660.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","alternative_title":["LNCS"],"volume":1872},{"publist_id":"216","abstract":[{"lang":"eng","text":"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. "}],"publication_status":"published","status":"public","language":[{"iso":"eng"}],"quality_controlled":"1","citation":{"apa":"Henzinger, T. A. (2000). The theory of hybrid automata. In M. Inan & R. Kurshan (Eds.), Verification of Digital and Hybrid Systems (Vol. 170, pp. 265–292). Springer. https://doi.org/10.1007/978-3-642-59615-5","short":"T.A. Henzinger, in:, M. Inan, R. Kurshan (Eds.), Verification of Digital and Hybrid Systems, Springer, 2000, pp. 265–292.","ieee":"T. A. Henzinger, “The theory of hybrid automata,” in Verification of Digital and Hybrid Systems, vol. 170, M. Inan and R. Kurshan, Eds. Springer, 2000, pp. 265–292.","chicago":"Henzinger, Thomas A. “The Theory of Hybrid Automata.” In Verification of Digital and Hybrid Systems, edited by M. Inan and Robert Kurshan, 170:265–92. Springer, 2000. https://doi.org/10.1007/978-3-642-59615-5.","ama":"Henzinger TA. The theory of hybrid automata. In: Inan M, Kurshan R, eds. Verification of Digital and Hybrid Systems. Vol 170. Springer; 2000:265-292. doi:10.1007/978-3-642-59615-5","mla":"Henzinger, Thomas A. “The Theory of Hybrid Automata.” Verification of Digital and Hybrid Systems, edited by M. Inan and Robert Kurshan, vol. 170, Springer, 2000, pp. 265–92, doi:10.1007/978-3-642-59615-5.","ista":"Henzinger TA. 2000.The theory of hybrid automata. In: Verification of Digital and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, vol. 170, 265–292."},"type":"book_chapter","publication_identifier":{"isbn":["9783642596155"]},"year":"2000","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"editor":[{"full_name":"Inan, M.","last_name":"Inan","first_name":"M."},{"first_name":"Robert","full_name":"Kurshan, Robert","last_name":"Kurshan"}],"doi":"10.1007/978-3-642-59615-5","oa_version":"None","publisher":"Springer","day":"28","volume":170,"alternative_title":["NATO ASI Series F: Computer and Systems Sciences"],"intvolume":" 170","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CR9504469, by the Air Force Office of Scientific Research contract F49620-93-1-0056, by the Army Research Office MURI grant DAAH-04-96-1-0341, by the Advanced Research Projects Agency grant NAG2-892, and by the Semiconductor Research Corporation contract 96-DC-324.036. ","extern":"1","scopus_import":"1","title":"The theory of hybrid automata","date_updated":"2023-04-18T12:37:17Z","month":"04","article_processing_charge":"No","date_published":"2000-04-28T00:00:00Z","publication":"Verification of Digital and Hybrid Systems","page":"265 - 292","_id":"4513","date_created":"2018-12-11T12:09:14Z"},{"title":"Discrete abstractions of hybrid systems","date_updated":"2023-04-13T13:32:11Z","month":"07","date_published":"2000-07-01T00:00:00Z","article_processing_charge":"No","publication":"Proceedings of the IEEE","page":"971 - 984","_id":"4598","date_created":"2018-12-11T12:09:41Z","volume":88,"issue":"7","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"The authors would like to thank the reviewers for their detailed comments.","intvolume":" 88","scopus_import":"1","extern":"1","publication_identifier":{"issn":["0018-9219"]},"author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Gerardo","full_name":"Lafferriere, Gerardo","last_name":"Lafferriere"},{"first_name":"George","full_name":"Pappas, George","last_name":"Pappas"}],"year":"2000","doi":"10.1109/5.871304 ","oa_version":"None","publisher":"IEEE","day":"01","publication_status":"published","abstract":[{"lang":"eng","text":"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."}],"publist_id":"107","language":[{"iso":"eng"}],"status":"public","quality_controlled":"1","type":"journal_article","citation":{"apa":"Alur, R., Henzinger, T. A., Lafferriere, G., & Pappas, G. (2000). Discrete abstractions of hybrid systems. Proceedings of the IEEE. IEEE. https://doi.org/10.1109/5.871304 ","short":"R. Alur, T.A. Henzinger, G. Lafferriere, G. Pappas, Proceedings of the IEEE 88 (2000) 971–984.","ieee":"R. Alur, T. A. Henzinger, G. Lafferriere, and G. Pappas, “Discrete abstractions of hybrid systems,” Proceedings of the IEEE, vol. 88, no. 7. IEEE, pp. 971–984, 2000.","chicago":"Alur, Rajeev, Thomas A Henzinger, Gerardo Lafferriere, and George Pappas. “Discrete Abstractions of Hybrid Systems.” Proceedings of the IEEE. IEEE, 2000. https://doi.org/10.1109/5.871304 .","ama":"Alur R, Henzinger TA, Lafferriere G, Pappas G. Discrete abstractions of hybrid systems. Proceedings of the IEEE. 2000;88(7):971-984. doi:10.1109/5.871304 ","ista":"Alur R, Henzinger TA, Lafferriere G, Pappas G. 2000. Discrete abstractions of hybrid systems. Proceedings of the IEEE. 88(7), 971–984.","mla":"Alur, Rajeev, et al. “Discrete Abstractions of Hybrid Systems.” Proceedings of the IEEE, vol. 88, no. 7, IEEE, 2000, pp. 971–84, doi:10.1109/5.871304 ."},"article_type":"original"},{"doi":"10.1109/LICS.2000.855763","publication":"Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science","oa_version":"None","page":"141 - 154","publisher":"IEEE","_id":"4627","day":"01","date_created":"2018-12-11T12:09:50Z","publication_identifier":{"isbn":["0769507255"]},"date_updated":"2023-04-13T13:24:29Z","title":"Concurrent omega-regular games","month":"01","conference":{"location":"Santa Barbara, CA, USA","start_date":"2000-06-26","end_date":"2000-06-28","name":"LICS: Logic in Computer Science"},"year":"2000","article_processing_charge":"No","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2000-01-01T00:00:00Z","extern":"1","type":"conference","citation":{"mla":"De Alfaro, Luca, and Thomas A. Henzinger. “Concurrent Omega-Regular Games.” Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, IEEE, 2000, pp. 141–54, doi:10.1109/LICS.2000.855763.","ista":"De Alfaro L, Henzinger TA. 2000. Concurrent omega-regular games. Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 141–154.","chicago":"De Alfaro, Luca, and Thomas A Henzinger. “Concurrent Omega-Regular Games.” In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 141–54. IEEE, 2000. https://doi.org/10.1109/LICS.2000.855763.","ama":"De Alfaro L, Henzinger TA. Concurrent omega-regular games. In: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science. IEEE; 2000:141-154. doi:10.1109/LICS.2000.855763","ieee":"L. De Alfaro and T. A. Henzinger, “Concurrent omega-regular games,” in Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, CA, USA, 2000, pp. 141–154.","apa":"De Alfaro, L., & Henzinger, T. A. (2000). Concurrent omega-regular games. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (pp. 141–154). Santa Barbara, CA, USA: IEEE. https://doi.org/10.1109/LICS.2000.855763","short":"L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, IEEE, 2000, pp. 141–154."},"scopus_import":"1","publist_id":"82","abstract":[{"lang":"eng","text":"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."}],"publication_status":"published","status":"public","language":[{"iso":"eng"}],"quality_controlled":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17"},{"month":"01","date_updated":"2023-04-13T11:00:46Z","title":"The control of synchronous systems","article_processing_charge":"No","date_published":"2000-01-01T00:00:00Z","page":"458 - 473","publication":"Proceedings of the 11th International Conference on Concurrency Theory","date_created":"2018-12-11T12:09:53Z","_id":"4637","volume":1877,"alternative_title":["LNCS"],"intvolume":" 1877","acknowledgement":"This research was supported in part by the DARPA grants NAG2-1214 and F33615-C-98-3614, the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660, and the NSF CAREER award CCR-9501708.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","publication_identifier":{"isbn":["9783540678977"]},"year":"2000","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2000-08-22","location":"University Park, PA, USA","end_date":"2000-08-25"},"author":[{"first_name":"Luca","full_name":"De Alfaro, Luca","last_name":"De Alfaro"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Freddy","full_name":"Mang, Freddy","last_name":"Mang"}],"oa_version":"None","doi":"10.1007/3-540-44618-4_33","day":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","status":"public","language":[{"iso":"eng"}],"publist_id":"69","publication_status":"published","abstract":[{"lang":"eng","text":"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.\r\nA 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.\r\nFurthermore, 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"}],"quality_controlled":"1","type":"conference","citation":{"ieee":"L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems,” in Proceedings of the 11th International Conference on Concurrency Theory, University Park, PA, USA, 2000, vol. 1877, pp. 458–473.","short":"L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 11th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2000, pp. 458–473.","apa":"De Alfaro, L., Henzinger, T. A., & Mang, F. (2000). The control of synchronous systems. In Proceedings of the 11th International Conference on Concurrency Theory (Vol. 1877, pp. 458–473). University Park, PA, USA: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44618-4_33","mla":"De Alfaro, Luca, et al. “The Control of Synchronous Systems.” Proceedings of the 11th International Conference on Concurrency Theory, vol. 1877, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2000, pp. 458–73, doi:10.1007/3-540-44618-4_33.","ista":"De Alfaro L, Henzinger TA, Mang F. 2000. The control of synchronous systems. Proceedings of the 11th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1877, 458–473.","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous Systems.” In Proceedings of the 11th International Conference on Concurrency Theory, 1877:458–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2000. https://doi.org/10.1007/3-540-44618-4_33.","ama":"De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems. In: Proceedings of the 11th International Conference on Concurrency Theory. Vol 1877. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2000:458-473. doi:10.1007/3-540-44618-4_33"}},{"publisher":"Springer","day":"01","doi":"10.1007/10722167_17","oa_version":"None","year":"2000","conference":{"start_date":"2000-07-15","location":"Chicago, IL, USA","end_date":"2000-07-19","name":"CAV: Computer-Aided Verification"},"author":[{"full_name":"De Alfaro, Luca","last_name":"De Alfaro","first_name":"Luca"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Freddy","last_name":"Mang","full_name":"Mang, Freddy"}],"publication_identifier":{"isbn":["9783540677703"]},"citation":{"ista":"De Alfaro L, Henzinger TA, Mang F. 2000. Detecting errors before reaching them. Proceedings of the 12th International Conference on Computer Aided Verification. CAV: Computer-Aided Verification, LNCS, vol. 1855, 186–201.","mla":"De Alfaro, Luca, et al. “Detecting Errors before Reaching Them.” Proceedings of the 12th International Conference on Computer Aided Verification, vol. 1855, Springer, 2000, pp. 186–201, doi:10.1007/10722167_17.","ama":"De Alfaro L, Henzinger TA, Mang F. Detecting errors before reaching them. In: Proceedings of the 12th International Conference on Computer Aided Verification. Vol 1855. Springer; 2000:186-201. doi:10.1007/10722167_17","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “Detecting Errors before Reaching Them.” In Proceedings of the 12th International Conference on Computer Aided Verification, 1855:186–201. Springer, 2000. https://doi.org/10.1007/10722167_17.","ieee":"L. De Alfaro, T. A. Henzinger, and F. Mang, “Detecting errors before reaching them,” in Proceedings of the 12th International Conference on Computer Aided Verification, Chicago, IL, USA, 2000, vol. 1855, pp. 186–201.","apa":"De Alfaro, L., Henzinger, T. A., & Mang, F. (2000). Detecting errors before reaching them. In Proceedings of the 12th International Conference on Computer Aided Verification (Vol. 1855, pp. 186–201). Chicago, IL, USA: Springer. https://doi.org/10.1007/10722167_17","short":"L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International Conference on Computer Aided Verification, Springer, 2000, pp. 186–201."},"type":"conference","quality_controlled":"1","publist_id":"70","publication_status":"published","abstract":[{"lang":"eng","text":"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.\r\nThe 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."}],"status":"public","language":[{"iso":"eng"}],"_id":"4638","date_created":"2018-12-11T12:09:53Z","publication":"Proceedings of the 12th International Conference on Computer Aided Verification","page":"186 - 201","article_processing_charge":"No","date_published":"2000-01-01T00:00:00Z","title":"Detecting errors before reaching them","date_updated":"2023-04-13T13:18:06Z","month":"01","extern":"1","scopus_import":"1","intvolume":" 1855","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"This research was supported in part by the DARPA (NASA) grant NAG2-1214, the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660, the DARPA (MARCO) grant MDA972-99-1-0001, and the NSF CAREER award CCR-9501708.","volume":1855,"alternative_title":["LNCS"]},{"extern":"1","citation":{"chicago":"Kaloshin, Vadim. “An Extension of the Artin-Mazur Theorem.” The Annals of Mathematics. JSTOR, 1999. https://doi.org/10.2307/121093.","ama":"Kaloshin V. An extension of the Artin-Mazur theorem. The Annals of Mathematics. 1999;150(2):729-741. doi:10.2307/121093","mla":"Kaloshin, Vadim. “An Extension of the Artin-Mazur Theorem.” The Annals of Mathematics, vol. 150, no. 2, JSTOR, 1999, pp. 729–41, doi:10.2307/121093.","ista":"Kaloshin V. 1999. An extension of the Artin-Mazur theorem. The Annals of Mathematics. 150(2), 729–741.","short":"V. Kaloshin, The Annals of Mathematics 150 (1999) 729–741.","apa":"Kaloshin, V. (1999). An extension of the Artin-Mazur theorem. The Annals of Mathematics. JSTOR. https://doi.org/10.2307/121093","ieee":"V. Kaloshin, “An extension of the Artin-Mazur theorem,” The Annals of Mathematics, vol. 150, no. 2. JSTOR, pp. 729–741, 1999."},"type":"journal_article","article_type":"original","publication_status":"published","volume":150,"status":"public","language":[{"iso":"eng"}],"quality_controlled":"1","intvolume":" 150","issue":"2","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"The Annals of Mathematics","doi":"10.2307/121093","page":"729-741","oa_version":"None","_id":"8526","publisher":"JSTOR","day":"01","date_created":"2020-09-18T10:50:28Z","publication_identifier":{"issn":["0003-486X"]},"title":"An extension of the Artin-Mazur theorem","date_updated":"2021-01-12T08:19:53Z","month":"09","keyword":["Statistics","Probability and Uncertainty","Statistics and Probability"],"article_processing_charge":"No","year":"1999","author":[{"id":"FE553552-CDE8-11E9-B324-C0EBE5697425","first_name":"Vadim","full_name":"Kaloshin, Vadim","orcid":"0000-0002-6051-2628","last_name":"Kaloshin"}],"date_published":"1999-09-01T00:00:00Z"},{"pmid":1,"status":"public","language":[{"iso":"eng"}],"publist_id":"6761","publication_status":"published","abstract":[{"lang":"eng","text":"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."}],"quality_controlled":"1","citation":{"chicago":"Kondrashov, Alexey, and Fyodor Kondrashov. “Interactions among Quantitative Traits in the Course of Sympatric Speciation.” Nature. Nature Publishing Group, 1999. https://doi.org/10.1038/22514.","ama":"Kondrashov A, Kondrashov F. Interactions among quantitative traits in the course of sympatric speciation. Nature. 1999;400(6742):351-354. doi:10.1038/22514","mla":"Kondrashov, Alexey, and Fyodor Kondrashov. “Interactions among Quantitative Traits in the Course of Sympatric Speciation.” Nature, vol. 400, no. 6742, Nature Publishing Group, 1999, pp. 351–54, doi:10.1038/22514.","ista":"Kondrashov A, Kondrashov F. 1999. Interactions among quantitative traits in the course of sympatric speciation. Nature. 400(6742), 351–354.","short":"A. Kondrashov, F. Kondrashov, Nature 400 (1999) 351–354.","apa":"Kondrashov, A., & Kondrashov, F. (1999). Interactions among quantitative traits in the course of sympatric speciation. Nature. Nature Publishing Group. https://doi.org/10.1038/22514","ieee":"A. Kondrashov and F. Kondrashov, “Interactions among quantitative traits in the course of sympatric speciation,” Nature, vol. 400, no. 6742. Nature Publishing Group, pp. 351–354, 1999."},"type":"journal_article","article_type":"original","publication_identifier":{"issn":["0028-0836"]},"year":"1999","author":[{"first_name":"Alexey","full_name":"Kondrashov, Alexey","last_name":"Kondrashov"},{"id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","first_name":"Fyodor","orcid":"0000-0001-8243-4694","full_name":"Kondrashov, Fyodor","last_name":"Kondrashov"}],"oa_version":"None","doi":"10.1038/22514","day":"01","publisher":"Nature Publishing Group","volume":400,"intvolume":" 400","acknowledgement":"This study was supported by a grant from the NSF.","issue":"6742","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","scopus_import":"1","month":"07","date_updated":"2023-04-13T10:33:44Z","title":"Interactions among quantitative traits in the course of sympatric speciation","article_processing_charge":"No","date_published":"1999-07-01T00:00:00Z","page":"351 - 354","publication":"Nature","external_id":{"pmid":["10432111"]},"date_created":"2018-12-11T11:49:00Z","_id":"883"},{"date_published":"1999-05-01T00:00:00Z","keyword":["Algorithms","Data structures","Evolutionary biology","Theory of databases"],"article_processing_charge":"No","month":"05","date_updated":"2023-02-21T16:33:24Z","title":"Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology","date_created":"2022-07-27T15:02:28Z","_id":"11679","page":"1-13","publication":"Algorithmica","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 24","volume":24,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"11927"}]},"scopus_import":"1","extern":"1","author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","last_name":"Henzinger","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530"},{"full_name":"King, V.","last_name":"King","first_name":"V."},{"full_name":"Warnow, T.","last_name":"Warnow","first_name":"T."}],"year":"1999","publication_identifier":{"eissn":["1432-0541"],"issn":["0178-4617"]},"day":"01","publisher":"Springer Nature","oa_version":"None","doi":"10.1007/pl00009268","quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","publication_status":"published","abstract":[{"text":"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 .\r\n\r\nWe 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.","lang":"eng"}],"article_type":"original","citation":{"ista":"Henzinger MH, King V, Warnow T. 1999. Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology. Algorithmica. 24, 1–13.","mla":"Henzinger, Monika H., et al. “Constructing a Tree from Homeomorphic Subtrees, with Applications to Computational Evolutionary Biology.” Algorithmica, vol. 24, Springer Nature, 1999, pp. 1–13, doi:10.1007/pl00009268.","ama":"Henzinger MH, King V, Warnow T. Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology. Algorithmica. 1999;24:1-13. doi:10.1007/pl00009268","chicago":"Henzinger, Monika H, V. King, and T. Warnow. “Constructing a Tree from Homeomorphic Subtrees, with Applications to Computational Evolutionary Biology.” Algorithmica. Springer Nature, 1999. https://doi.org/10.1007/pl00009268.","ieee":"M. H. Henzinger, V. King, and T. Warnow, “Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology,” Algorithmica, vol. 24. Springer Nature, pp. 1–13, 1999.","short":"M.H. Henzinger, V. King, T. Warnow, Algorithmica 24 (1999) 1–13.","apa":"Henzinger, M. H., King, V., & Warnow, T. (1999). Constructing a tree from homeomorphic subtrees, with applications to computational evolutionary biology. Algorithmica. Springer Nature. https://doi.org/10.1007/pl00009268"},"type":"journal_article"},{"language":[{"iso":"eng"}],"status":"public","publication_status":"published","abstract":[{"text":"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.\r\n\r\nWe 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.","lang":"eng"}],"quality_controlled":"1","citation":{"apa":"Dean, J., & Henzinger, M. H. (1999). Finding related pages in the world wide Web. Computer Networks. Elsevier. https://doi.org/10.1016/s1389-1286(99)00022-5","short":"J. Dean, M.H. Henzinger, Computer Networks 31 (1999) 1467–1479.","ieee":"J. Dean and M. H. Henzinger, “Finding related pages in the world wide Web,” Computer Networks, vol. 31, no. 11–16. Elsevier, pp. 1467–1479, 1999.","chicago":"Dean, Jeffrey, and Monika H Henzinger. “Finding Related Pages in the World Wide Web.” Computer Networks. Elsevier, 1999. https://doi.org/10.1016/s1389-1286(99)00022-5.","ama":"Dean J, Henzinger MH. Finding related pages in the world wide Web. Computer Networks. 1999;31(11-16):1467-1479. doi:10.1016/s1389-1286(99)00022-5","mla":"Dean, Jeffrey, and Monika H. Henzinger. “Finding Related Pages in the World Wide Web.” Computer Networks, vol. 31, no. 11–16, Elsevier, 1999, pp. 1467–79, doi:10.1016/s1389-1286(99)00022-5.","ista":"Dean J, Henzinger MH. 1999. Finding related pages in the world wide Web. Computer Networks. 31(11–16), 1467–1479."},"type":"journal_article","article_type":"original","publication_identifier":{"issn":["1389-1286"]},"author":[{"first_name":"Jeffrey","full_name":"Dean, Jeffrey","last_name":"Dean"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","last_name":"Henzinger","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530"}],"year":"1999","oa_version":"None","doi":"10.1016/s1389-1286(99)00022-5","day":"17","publisher":"Elsevier","volume":31,"issue":"11-16","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 31","scopus_import":"1","extern":"1","month":"05","title":"Finding related pages in the world wide Web","date_updated":"2022-09-12T09:12:21Z","date_published":"1999-05-17T00:00:00Z","article_processing_charge":"No","keyword":["Search engines","Related pages","Searching paradigms"],"page":"1467-1479","publication":"Computer Networks","date_created":"2022-07-29T06:55:26Z","_id":"11687"},{"quality_controlled":"1","publication_status":"published","abstract":[{"text":"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.","lang":"eng"}],"status":"public","language":[{"iso":"eng"}],"article_type":"original","type":"journal_article","citation":{"ista":"Henzinger MH, Heydon A, Mitzenmacher M, Najork M. 1999. Measuring index quality using random walks on the web. Computer Networks. 31(11–16), 1291–1303.","mla":"Henzinger, Monika H., et al. “Measuring Index Quality Using Random Walks on the Web.” Computer Networks, vol. 31, no. 11–16, Elsevier, 1999, pp. 1291–303, doi:10.1016/s1389-1286(99)00016-x.","ama":"Henzinger MH, Heydon A, Mitzenmacher M, Najork M. Measuring index quality using random walks on the web. Computer Networks. 1999;31(11-16):1291-1303. doi:10.1016/s1389-1286(99)00016-x","chicago":"Henzinger, Monika H, Allan Heydon, Michael Mitzenmacher, and Marc Najork. “Measuring Index Quality Using Random Walks on the Web.” Computer Networks. Elsevier, 1999. https://doi.org/10.1016/s1389-1286(99)00016-x.","ieee":"M. H. Henzinger, A. Heydon, M. Mitzenmacher, and M. Najork, “Measuring index quality using random walks on the web,” Computer Networks, vol. 31, no. 11–16. Elsevier, pp. 1291–1303, 1999.","apa":"Henzinger, M. H., Heydon, A., Mitzenmacher, M., & Najork, M. (1999). Measuring index quality using random walks on the web. Computer Networks. Elsevier. https://doi.org/10.1016/s1389-1286(99)00016-x","short":"M.H. Henzinger, A. Heydon, M. Mitzenmacher, M. Najork, Computer Networks 31 (1999) 1291–1303."},"year":"1999","author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger"},{"last_name":"Heydon","full_name":"Heydon, Allan","first_name":"Allan"},{"first_name":"Michael","last_name":"Mitzenmacher","full_name":"Mitzenmacher, Michael"},{"last_name":"Najork","full_name":"Najork, Marc","first_name":"Marc"}],"publication_identifier":{"issn":["1389-1286"]},"publisher":"Elsevier","day":"17","doi":"10.1016/s1389-1286(99)00016-x","oa_version":"None","intvolume":" 31","issue":"11-16","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":31,"extern":"1","scopus_import":"1","article_processing_charge":"No","keyword":["Search engines","Index quality","Random walks","PageRank"],"date_published":"1999-05-17T00:00:00Z","title":"Measuring index quality using random walks on the web","date_updated":"2022-09-12T09:13:55Z","month":"05","_id":"11688","date_created":"2022-07-29T07:00:28Z","publication":"Computer Networks","page":"1291-1303"},{"extern":"1","scopus_import":"1","type":"conference","citation":{"chicago":"Goel, Ashish, Monika H Henzinger, Serge Plotkin, and Eva Tardos. “Scheduling Data Transfers in a Network and the Set Scheduling Problem.” In Proceedings of the 31st Annual ACM Symposium on Theory of Computing, 189–97. Association for Computing Machinery, 1999. https://doi.org/10.1145/301250.301300.","ama":"Goel A, Henzinger MH, Plotkin S, Tardos E. Scheduling data transfers in a network and the set scheduling problem. In: Proceedings of the 31st Annual ACM Symposium on Theory of Computing. Association for Computing Machinery; 1999:189-197. doi:10.1145/301250.301300","ista":"Goel A, Henzinger MH, Plotkin S, Tardos E. 1999. Scheduling data transfers in a network and the set scheduling problem. Proceedings of the 31st annual ACM symposium on Theory of computing. STOC: Symposium on Theory of Computing, 189–197.","mla":"Goel, Ashish, et al. “Scheduling Data Transfers in a Network and the Set Scheduling Problem.” Proceedings of the 31st Annual ACM Symposium on Theory of Computing, Association for Computing Machinery, 1999, pp. 189–97, doi:10.1145/301250.301300.","apa":"Goel, A., Henzinger, M. H., Plotkin, S., & Tardos, E. (1999). Scheduling data transfers in a network and the set scheduling problem. In Proceedings of the 31st annual ACM symposium on Theory of computing (pp. 189–197). Atlanta, GA, United States: Association for Computing Machinery. https://doi.org/10.1145/301250.301300","short":"A. Goel, M.H. Henzinger, S. Plotkin, E. Tardos, in:, Proceedings of the 31st Annual ACM Symposium on Theory of Computing, Association for Computing Machinery, 1999, pp. 189–197.","ieee":"A. Goel, M. H. Henzinger, S. Plotkin, and E. Tardos, “Scheduling data transfers in a network and the set scheduling problem,” in Proceedings of the 31st annual ACM symposium on Theory of computing, Atlanta, GA, United States, 1999, pp. 189–197."},"status":"public","language":[{"iso":"eng"}],"publication_status":"published","abstract":[{"text":"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.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","page":"189-197","oa_version":"None","publication":"Proceedings of the 31st annual ACM symposium on Theory of computing","doi":"10.1145/301250.301300","day":"01","date_created":"2022-07-29T07:43:00Z","publisher":"Association for Computing Machinery","_id":"11691","month":"05","publication_identifier":{"issn":["0196-6774"]},"date_updated":"2023-02-09T11:47:09Z","title":"Scheduling data transfers in a network and the set scheduling problem","keyword":["Scheduling","Flow time"],"year":"1999","article_processing_charge":"No","conference":{"start_date":"1999-05-01","location":" Atlanta, GA, United States","end_date":"1999-05-04","name":"STOC: Symposium on Theory of Computing"},"author":[{"full_name":"Goel, Ashish","last_name":"Goel","first_name":"Ashish"},{"full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"Plotkin","full_name":"Plotkin, Serge","first_name":"Serge"},{"first_name":"Eva","full_name":"Tardos, Eva","last_name":"Tardos"}],"date_published":"1999-05-01T00:00:00Z"},{"publication_status":"published","abstract":[{"text":"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.\r\nLet 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.","lang":"eng"}],"volume":46,"language":[{"iso":"eng"}],"status":"public","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"4","intvolume":" 46","citation":{"chicago":"Henzinger, Monika H, and Valerie King. “Randomized Fully Dynamic Graph Algorithms with Polylogarithmic Time per Operation.” Journal of the ACM. Association for Computing Machinery, 1999. https://doi.org/10.1145/320211.320215.","ama":"Henzinger MH, King V. Randomized fully dynamic graph algorithms with polylogarithmic time per operation. Journal of the ACM. 1999;46(4):502-516. doi:10.1145/320211.320215","ista":"Henzinger MH, King V. 1999. Randomized fully dynamic graph algorithms with polylogarithmic time per operation. Journal of the ACM. 46(4), 502–516.","mla":"Henzinger, Monika H., and Valerie King. “Randomized Fully Dynamic Graph Algorithms with Polylogarithmic Time per Operation.” Journal of the ACM, vol. 46, no. 4, Association for Computing Machinery, 1999, pp. 502–16, doi:10.1145/320211.320215.","short":"M.H. Henzinger, V. King, Journal of the ACM 46 (1999) 502–516.","apa":"Henzinger, M. H., & King, V. (1999). Randomized fully dynamic graph algorithms with polylogarithmic time per operation. Journal of the ACM. Association for Computing Machinery. https://doi.org/10.1145/320211.320215","ieee":"M. H. Henzinger and V. King, “Randomized fully dynamic graph algorithms with polylogarithmic time per operation,” Journal of the ACM, vol. 46, no. 4. Association for Computing Machinery, pp. 502–516, 1999."},"scopus_import":"1","type":"journal_article","extern":"1","article_type":"original","title":"Randomized fully dynamic graph algorithms with polylogarithmic time per operation","date_updated":"2022-09-12T10:50:08Z","publication_identifier":{"issn":["0004-5411"],"eissn":["1557-735X"]},"month":"07","author":[{"last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"King, Valerie","last_name":"King","first_name":"Valerie"}],"date_published":"1999-07-01T00:00:00Z","year":"1999","article_processing_charge":"No","doi":"10.1145/320211.320215","publication":"Journal of the ACM","oa_version":"None","page":"502-516","publisher":"Association for Computing Machinery","_id":"11769","date_created":"2022-08-08T12:50:25Z","day":"01"},{"article_processing_charge":"No","date_published":"1999-01-01T00:00:00Z","date_updated":"2023-02-17T14:46:04Z","title":"Analysis of a very large web search engine query log","month":"01","_id":"11895","date_created":"2022-08-17T08:53:02Z","publication":"ACM SIGIR Forum","page":"6-12","intvolume":" 33","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/331403.331405"}],"volume":33,"extern":"1","scopus_import":"1","year":"1999","author":[{"first_name":"Craig","full_name":"Silverstein, Craig","last_name":"Silverstein"},{"first_name":"Hannes","last_name":"Marais","full_name":"Marais, Hannes"},{"full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H"},{"full_name":"Moricz, Michael","last_name":"Moricz","first_name":"Michael"}],"publication_identifier":{"issn":["0163-5840"]},"publisher":"Association for Computing Machinery","day":"01","doi":"10.1145/331403.331405","oa_version":"Published Version","quality_controlled":"1","publication_status":"published","abstract":[{"lang":"eng","text":"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."}],"status":"public","language":[{"iso":"eng"}],"article_type":"original","citation":{"short":"C. Silverstein, H. Marais, M.H. Henzinger, M. Moricz, ACM SIGIR Forum 33 (1999) 6–12.","apa":"Silverstein, C., Marais, H., Henzinger, M. H., & Moricz, M. (1999). Analysis of a very large web search engine query log. ACM SIGIR Forum. Association for Computing Machinery. https://doi.org/10.1145/331403.331405","ieee":"C. Silverstein, H. Marais, M. H. Henzinger, and M. Moricz, “Analysis of a very large web search engine query log,” ACM SIGIR Forum, vol. 33, no. 1. Association for Computing Machinery, pp. 6–12, 1999.","ama":"Silverstein C, Marais H, Henzinger MH, Moricz M. Analysis of a very large web search engine query log. ACM SIGIR Forum. 1999;33(1):6-12. doi:10.1145/331403.331405","chicago":"Silverstein, Craig, Hannes Marais, Monika H Henzinger, and Michael Moricz. “Analysis of a Very Large Web Search Engine Query Log.” ACM SIGIR Forum. Association for Computing Machinery, 1999. https://doi.org/10.1145/331403.331405.","ista":"Silverstein C, Marais H, Henzinger MH, Moricz M. 1999. Analysis of a very large web search engine query log. ACM SIGIR Forum. 33(1), 6–12.","mla":"Silverstein, Craig, et al. “Analysis of a Very Large Web Search Engine Query Log.” ACM SIGIR Forum, vol. 33, no. 1, Association for Computing Machinery, 1999, pp. 6–12, doi:10.1145/331403.331405."},"type":"journal_article"},{"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"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\r\nconstant-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\r\nexists a polylogarithmic lower bound on the competitive ratio of any online algorithm on tree topologies [l]. We prove the same lower bound for meshes. ","lang":"eng"}],"publication_status":"published","status":"public","language":[{"iso":"eng"}],"extern":"1","scopus_import":"1","citation":{"short":"M.H. Henzinger, S. Leonardi , in:, 10th Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial & Applied Mathematics, 1999, pp. 438–447.","apa":"Henzinger, M. H., & Leonardi , S. (1999). Scheduling multicasts on unit-capacity trees and meshes. In 10th Annual ACM-SIAM Symposium on Discrete Algorithms (pp. 438–447). Baltimore, MD, United States: Society for Industrial & Applied Mathematics.","ieee":"M. H. Henzinger and S. Leonardi , “Scheduling multicasts on unit-capacity trees and meshes,” in 10th Annual ACM-SIAM Symposium on Discrete Algorithms, Baltimore, MD, United States, 1999, pp. 438–447.","chicago":"Henzinger, Monika H, and Stefano Leonardi . “Scheduling Multicasts on Unit-Capacity Trees and Meshes.” In 10th Annual ACM-SIAM Symposium on Discrete Algorithms, 438–47. Society for Industrial & Applied Mathematics, 1999.","ama":"Henzinger MH, Leonardi S. Scheduling multicasts on unit-capacity trees and meshes. In: 10th Annual ACM-SIAM Symposium on Discrete Algorithms. Society for Industrial & Applied Mathematics; 1999:438-447.","mla":"Henzinger, Monika H., and Stefano Leonardi . “Scheduling Multicasts on Unit-Capacity Trees and Meshes.” 10th Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial & Applied Mathematics, 1999, pp. 438–47.","ista":"Henzinger MH, Leonardi S. 1999. Scheduling multicasts on unit-capacity trees and meshes. 10th Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 438–447."},"type":"conference","article_processing_charge":"No","year":"1999","conference":{"start_date":"1999-01-17","location":"Baltimore, MD, United States","end_date":"1999-01-19","name":"SODA: Symposium on Discrete Algorithms"},"author":[{"last_name":"Henzinger","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H"},{"full_name":"Leonardi , Stefano","last_name":"Leonardi ","first_name":"Stefano"}],"date_published":"1999-01-01T00:00:00Z","publication_identifier":{"isbn":["0898714346"]},"date_updated":"2023-02-17T12:08:26Z","title":"Scheduling multicasts on unit-capacity trees and meshes","month":"01","_id":"11925","publisher":"Society for Industrial & Applied Mathematics","day":"01","date_created":"2022-08-18T12:45:50Z","publication":"10th Annual ACM-SIAM Symposium on Discrete Algorithms","page":"438-447","oa_version":"None"}]