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