@inproceedings{4477, abstract = {The assume-guarantee paradigm is a powerful divide-and-conquer mechanism for decomposing a verification task about a system into subtasks about the individual components of the system. The key to assume-guarantee reasoning is to consider each component not in isolation, but in conjunction with assumptions about the context of the component. Assume-guarantee principles are known for purely concurrent contexts, which constrain the input data of a component, as well as for purely sequential contexts, which constrain the entry configurations of a component. We present a model for hierarchical system design which permits the arbitrary nesting of parallel as well as serial composition, and which supports an assume-guarantee principle for mixed parallel-serial contexts. Our model also supports both discrete and continuous processes, and is therefore well-suited for the modeling and analysis of embedded software systems which interact with real-world environments. Using an example of two cooperating robots, we show refinement between a high-level model which specifies continuous timing constraints and an implementation which relies on discrete sampling.}, author = {Henzinger, Thomas A and Minea, Marius and Prabhu, Vinayak}, booktitle = {Proceedings of the 4th International Workshop on Hybrid Systems}, isbn = {9783540418665}, location = {Rome, Italy}, pages = {275 -- 290}, publisher = {Springer}, title = {{Assume-guarantee reasoning for hierarchical hybrid systems}}, doi = {10.1007/3-540-45351-2_24}, volume = {2034}, year = {2001}, } @inproceedings{4478, abstract = {Giotto is a principled, tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPUs, and networks. Giotto is based on the principle that time-triggered task invocations plus time-triggered mode switches can form the abstract essence of programming real-time control systems. Giotto consists of a programming language with a formal semantics, and a retargetable compiler and runtime library. Giotto supports the automation of control system design by strictly separating platform-independent functionality and timing concerns from platform-dependent scheduling and communication issues. The time-triggered predictability of Giotto makes it particularly suitable for safety-critical applications with hard real-time constraints. We illustrate the platform-independence and time-triggered execution of Giotto by coordinating a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots.}, author = {Henzinger, Thomas A and Horowitz, Benjamin and Kirsch, Christoph}, booktitle = {Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems}, isbn = {9781581134254}, location = {New York, NY, United States}, pages = {64 -- 72}, publisher = {ACM}, title = {{Embedded control systems development with Giotto}}, doi = {10.1145/384197.384208}, year = {2001}, } @inproceedings{4479, abstract = {Giotto provides an abstract programmer’s model for the implementation of embedded control systems with hard real-time constraints. A typical control application consists of periodic software tasks together with a mode switching logic for enabling and disabling tasks. Giotto specifies time-triggered sensor readings, task invocations, and mode switches independent of any implementation platform. Giotto can be annotated with platform constraints such as task-to-host mappings, and task and communication schedules. The annotations are directives for the Giotto compiler, but they do not alter the functionality and timing of a Giotto program. By separating the platform-independent from the platform-dependent concerns, Giotto enables a great deal of flexibility in choosing control platforms as well as a great deal of automation in the validation and synthesis of control software. The time-triggered nature of Giotto achieves timing predictability, which makes Giotto particularly suitable for safety-critical applications.}, author = {Henzinger, Thomas A and Horowitz, Benjamin and Kirsch, Christoph}, booktitle = {Proceedings of the 1st International Workshop on Embedded Software}, isbn = {9783540426738}, location = {Tahoe City, CA, USA}, pages = {166 -- 184}, publisher = {ACM}, title = {{Giotto: A time-triggered language for embedded programming}}, doi = {10.1007/3-540-45449-7_12}, volume = {2211}, year = {2001}, } @inproceedings{4475, abstract = {We provide an overview of the current status of HYTECH, and reflect on some of the lessons learned from our experiences with the tool. HYTECH is a symbolic model checker for mixed discrete-continuous systems that are modeled as automata with piecewise-constant polyhedral differential inclusions. The use of a formal input language and automated procedures for state-space traversal lay the foundation for formally verifying properties of hybrid dynamical systems. We describe some recent experiences analyzing three hybrid systems. We point out the successes and limitations of the tool. The analysis procedure has been extended in a number of ways to address some of the tool's shortcomings. We evaluate these extensions, and conclude with some desiderata for verification tools for hybrid systems.}, author = {Henzinger, Thomas A and Preussig, Joerg and Wong Toi, Howard}, booktitle = {Proceedings of the 40th IEEE Conference on Decision and Control}, isbn = {0780370619}, location = {Orlando, FL, USA}, pages = {2887 -- 2892}, publisher = {IEEE}, title = {{Some lessons from the HYTECH experience}}, doi = {10.1109/.2001.980714}, volume = {3}, year = {2001}, } @proceedings{4449, abstract = {Embedded software is software that interacts with physical processes. As em- bedded systems increasingly permeate our daily lives on all levels, from micros- copic devices to international networks, the cost-efficient development of reliable embedded software is one of the grand challenges in computer science today. The purpose of the workshop is to bring together researchers in all areas of computer science that are traditionally distinct but relevant to embedded software develop- ment, and to incubate a research community in this way. The workshop aims to cover all aspects of the design and implementation of embedded software, inclu- ding operating systems and middleware, programming languages and compilers, modeling and validation, software engineering and programming methodologies, scheduling and execution time analysis, networking and fault tolerance, as well as application areas, such as embedded control, real-time signal processing, and telecommunications.}, editor = {Henzinger, Thomas A}, isbn = {9783540426738}, location = {Tahoe City, CA, USA}, publisher = {ACM}, title = {{EMSOFT: Embedded Software}}, doi = {10.1007/3-540-45449-7}, volume = {2211}, year = {2001}, } @inbook{4278, abstract = {The ability of species to migrate that has interested ecologists for many years. Now that so many species and ecosystems face major environmental change, the ability of species to adapt to these changes by dispersing, migrating, or moving between different patches of habitat can be crucial to ensuring their survivial. This book provides a timely and wide-ranging overview of the study of dispersal and incorporates much of the latest research. The causes, mechanisms, and consequences of dispersal at the individual, population, species and community levels are considered. The potential of new techniques and models for studying dispersal, drawn from molecular biology and demography, is also explored. Perspectives and insights are offered from the fields of evolution, conservation biology and genetics. Throughout the book, theoretical approaches are combined with empirical data, and care has been taken to include examples from as wide a range of species as possible. }, author = {Barton, Nicholas H}, booktitle = {Dispersal}, isbn = {9780198506591}, publisher = {Oxford University Press}, title = {{The evolutionary consequences of gene flow and local adaptation: Future approaches}}, year = {2001}, } @article{4200, abstract = {Zebrafish embryos homozygous for the masterblind (mb1) mutation exhibit a striking phenotype in which the eyes and telencephalon are reduced or absent and diencephalic fates expand to the front of the brain. Here we show that mb1(-/-) embryos carry an amino-acid change at a conserved site in the Wnt pathway scaffolding protein, Axin1. The amino-acid substitution present in the mbl allele abolishes the binding of Axin to Gsk3 and affects Tcf-dependent transcription. Therefore, Gsk3 activity may be decreased in mbl(-/-) embryos and in support of this possibility, overexpression of either wild-type Axin1 or Gsk3 beta can restore eye and telencephalic fates to mb1(-/-) embryos. Our data reveal a crucial role for Axin1-dependent inhibition of the Wnt pathway in the early regional subdivision of the anterior neural plate into telencephalic, diencephalic, and eye-forming territories.}, author = {Heisenberg, Carl-Philipp J and Houart, Corinne and Take Uchi, Masaya and Rauch, Gerd and Young, Neville and Coutinho, Pedro and Masai, Ichiro and Caneparo, Luca and Concha, Miguel and Geisler, Robert and Dale, Trevor and Wilson, Stephen and Stemple, Derek}, issn = {0890-9369}, journal = {Genes and Development}, number = {11}, pages = {1427 -- 1434}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{A mutation in the Gsk3-binding domain of zebrafish Masterblind/Axin1 leads to a fate transformation of telencephalon and eyes to diencephalon}}, doi = {10.1101/gad.194301}, volume = {15}, year = {2001}, } @article{4266, abstract = {Hybridization may influence evolution in a variety of ways. If hybrids are less fit, the geographical range of ecologically divergent populations may be limited, and prezygotic reproductive isolation may be reinforced. If some hybrid genotypes are fitter than one or both parents, at least in some environments, then hybridization could make a positive contribution. Single alleles that are at an advantage in the alternative environment and genetic background will introgress readily, although such introgression may be hard to detect. 'Hybrid speciation', in which fit combinations of alleles are established, is more problematic; its likelihood depends on how divergent populations meet, and on the structure of epistasis. These issues are illustrated using Fisher's model of stabilizing selection on multiple traits, under which reproductive isolation evolves as a side-effect of adaptation in allopatry. This confirms a priori arguments that while recombinant hybrids are less fit on average, some gene combinations may be fitter than the parents, even in the parental environment. Fisher's model does predict heterosis in diploid F1s, asymmetric incompatibility in reciprocal backcrosses, and (when dominance is included) Haldane's Rule. However, heterosis arises only when traits are additive, whereas the latter two patterns require dominance. Moreover, because adaptation is via substitutions of small effect, Fisher's model does not generate the strong effects of single chromosome regions often observed in species crosses.}, author = {Barton, Nicholas H}, issn = {962-1083}, journal = {Molecular Ecology}, number = {3}, pages = {551 -- 568}, publisher = {Wiley-Blackwell}, title = {{The role of hybridization in evolution}}, doi = {10.1046/j.1365-294X.2001.01216.x}, volume = {10}, year = {2001}, } @article{4265, abstract = {The reasons that sex and recombination are so widespread remain elusive. One popular hypothesis is that sex and recombination promote adaptation to a changing environment. The strongest evidence that increased recombination may evolve because recombination promotes adaptation comes from artificially selected populations. Recombination rates have been found to increase as a correlated response to selection on traits unrelated to recombination in several artificial selection experiments and in a comparison of domesticated and nondomesticated mammals. There are, however, several alternative explanations for the increase in recombination in such populations, including two different evolutionary explanations. The first is that the form of selection is epistatic, generating linkage disequilibria among selected loci, which can indirectly favor modifier alleles that increase recombination. The second is that random genetic drift in selected populations tends to generate disequilibria such that beneficial alleles are often found in different individuals; modifier alleles that increase recombination can bring together such favorable alleles and thus may be found in individuals with greater fitness. In this paper, we compare the evolutionary forces acting on recombination in finite populations subject to strong selection, To our surprise, we found that drift accounted for the majority of selection for increased recombination observed in simulations of small to moderately large populations, suggesting that, unless selected populations are large, epistasis plays a secondary role in the evolution of recombination.}, author = {Otto, Sarah and Barton, Nicholas H}, issn = {0014-3820}, journal = {Evolution; International Journal of Organic Evolution}, number = {10}, pages = {1921 -- 1931}, publisher = {Wiley-Blackwell}, title = {{Selection for recombination in small populations}}, doi = {10.1111/j.0014-3820.2001.tb01310.x}, volume = {55}, year = {2001}, } @article{4229, abstract = {Bacteriophage of the family Leviviridae have played an important role in molecular biology where representative species, such as Qβ and MS2, have been studied as model systems for replication, translation, and the role of secondary structure in gene regulation. Using nucleotide sequences from the coat and replicase genes we present the first statistical estimate of phylogeny for the family Leviviridae using maximum-likelihood and Bayesian estimation. Our analyses reveal that the coliphage species are a monophyletic group consisting of two clades representing the genera Levivirus and Allolevivirus. The Pseudomonas species PP7 diverged from its common ancestor with the coliphage prior to the ancient split between these genera and their subsequent diversification. Differences in genome size, gene composition, and gene expression are shown with a high probability to have changed along the lineage leading to the Allolevivirus through gene expansion. The change in genome size of the Allolevivirus ancestor may have catalyzed subsequent changes that led to their current genome organization and gene expression.}, author = {Bollback, Jonathan P and Huelsenbeck, John}, issn = {0022-2844}, journal = {Journal of Molecular Evolution}, number = {2}, pages = {117 -- 128}, publisher = {Springer}, title = {{Phylogeny, genome evolution, and host specificity of single-stranded RNA bacteriophage (Family Leviviridae)}}, doi = {10.1007/s002390010140}, volume = {52}, year = {2001}, } @article{4264, abstract = {The study of speciation has become one of the most active areas of evolutionary biology, and substantial progress has been made in documenting and understanding phenomena ranging from sympatric speciation and reinforcement to the evolutionary genetics of postzygotic isolation. This progress has been driven largely by empirical results, and most useful theoretical work has concentrated on making sense of empirical patterns. Given the complexity of speciation, mathematical theory is subordinate to verbal theory and generalizations about data. Nevertheless, mathematical theory can provide a useful classification of verbal theories; can help determine the biological plausibility of verbal theories; can determine whether alternative mechanisms of speciation are consistent with empirical patterns; and can occasionally provide predictions that go beyond empirical generalizations. We discuss recent examples of progress in each of these areas.}, author = {Turelli, Michael and Barton, Nicholas H and Coyne, Jerry}, issn = {0169-5347}, journal = {Trends in Ecology and Evolution}, number = {7}, pages = {330 -- 343}, publisher = {Cell Press}, title = {{Theory and speciation}}, doi = {10.1016/S0169-5347(01)02177-2}, volume = {16}, year = {2001}, } @inbook{4267, abstract = {The flow of genes from the dense and well-adapted centre of a species' distribution interferes with adaptation to marginal environments, and may sharply limit a species' range. Deterministic models of a linear habitat suggest that populations could in principle adapt to very steep environmental gradients, by increasing their genetic variability. However, random fluctuations in sparse populations reduce this variance, and may be crucial in limiting the species' range.}, author = {Barton, Nicholas H}, booktitle = {Integrating ecology and evolution in a spatial context}, isbn = {9780521840002}, pages = {365 -- 392}, publisher = {Cambridge University Press}, title = {{Adaptation at the edge of a species' range}}, year = {2001}, } @article{4002, abstract = {Shape deformation refers to the continuous change of one geometric object to another. We develop a software tool for planning, analyzing and visualizing deformations between two shapes in R-2. The deformation is generated automatically without any user intervention or specification of feature correspondences. A unique property of the tool is the explicit availability of a two-dimensional shape space, which can be used for designing the deformation either automatically by following constraints and objectives or manually by drawing deformation paths.}, author = {Cheng, Siu and Edelsbrunner, Herbert and Fu, Ping and Lam, Ka}, issn = {0925-7721}, journal = {Computational Geometry: Theory and Applications}, number = {2-3}, pages = {205 -- 218}, publisher = {Elsevier}, title = {{Design and analysis of planar shape deformation}}, doi = {10.1016/S0925-7721(01)00020-7}, volume = {19}, year = {2001}, } @article{4001, abstract = {The construction of shape spaces is studied from a mathematical and a computational viewpoint. A program is outlined reducing the problem to four tasks: the representation of geometry, the canonical deformation of geometry, the measuring of distance in shape space, and the selection of base shapes. The technical part of this paper focuses on the second task: the specification of a deformation mixing two or more shapes in continuously changing proportions. (C) 2001 Elsevier Science B.V All rights reserved.}, author = {Cheng, Ho and Edelsbrunner, Herbert and Fu, Ping}, issn = {0925-7721}, journal = {Computational Geometry: Theory and Applications}, number = {2-3}, pages = {191 -- 204}, publisher = {Elsevier}, title = {{Shape space from deformation}}, doi = {10.1016/S0925-7721(01)00021-9}, volume = {19}, year = {2001}, } @inproceedings{4005, abstract = {This paper describes an algorithm for maintaining an approximating triangulation of a deforming surface in R-3. The triangulation adapts dynamically to changing shape, curvature, and topology of the surface.}, author = {Cheng, Ho and Dey, Tamal and Edelsbrunner, Herbert and Sullivan, John}, booktitle = {Proceedings of the 12th annual ACM-SIAM symposium on Discrete algorithms}, isbn = {9780898714906}, location = {Washington, DC, USA }, pages = {47 -- 56}, publisher = {SIAM}, title = {{Dynamic skin triangulation}}, year = {2001}, } @article{4007, abstract = {This paper describes an algorithm for maintaining an approximating triangulation of a deforming surface in R 3 . The surface is the envelope of an infinite family of spheres defined and controlled by a finite collection of weighted points. The triangulation adapts dynamically to changing shape, curvature, and topology of the surface. }, author = {Cheng, Ho and Dey, Tamal and Edelsbrunner, Herbert and Sullivan, John}, issn = {0179-5376}, journal = {Discrete & Computational Geometry}, number = {4}, pages = {525 -- 568}, publisher = {Springer}, title = {{Dynamic skin triangulation}}, doi = {10.1007/s00454-001-0007-1}, volume = {25}, year = {2001}, } @article{4006, abstract = {The 180 models collected in this paper are produced by sampling and wrapping point sets on tubes. The surfaces are represented as triangulated 2-manifolds and available as st1-files from the author's web site at www.cs.duke.edu/similar toedels. Each tube is obtained by thickening a circle or a smooth torus knot, and for some we use the degrees of freedom in the thickening process to encode meaningful information, such as curvature or torsion.}, author = {Edelsbrunner, Herbert}, issn = {0948-695X}, journal = {Journal of Universal Computer Science}, number = {5}, pages = {379 -- 399}, publisher = {Springer}, title = {{180 wrapped tubes}}, doi = {10.3217/jucs-007-05-0379}, volume = {7}, year = {2001}, } @article{3928, abstract = {Regulated adhesion of leukocytes to the extracellular matrix is essential for transmigration of blood vessels and subsequent migration into the stroma of inflamed tissues. Although beta(2)-integrins play an indisputable role in adhesion of polymorphonuclear granulocytes (PMN) to endothelium, we show here that beta(1)- and beta(3)-integrins but not beta(2)-integrin are essential for the adhesion to and migration on extracellular matrix molecules of the endothelial cell basement membrane and subjacent interstitial matrix. Mouse wild type and beta(2)-integrin null PMN and the progranulocytic cell line 32DC13 were employed in in vitro adhesion and migration assays using extracellular matrix molecules expressed at sites of extravasation in vivo, in particular the endothelial cell laminins 8 and 10. Wild type and beta(2)-integrin null PMN showed the same pattern of ECM binding, indicating that beta(2)-integrins do not mediate specific adhesion of PMN to the extracellular matrix molecules tested; binding was observed to the interstitial matrix molecules, fibronectin and vitronectin, via integrins alpha(5)beta(1) and alpha(v)beta(3), respectively; to laminin 10 via alpha(6)beta(1); but not to laminins 1, 2, and 8, collagen type I and IV, perlecan, or tenascin-C. PMN binding to laminins 1, 2, and 8 could not be induced despite surface expression of functionally active integrin alpha(6)beta(1), a major laminin receptor, demonstrating that expression of alpha(6)beta(1) alone is insufficient for ligand binding and suggesting the involvement of accessory factors. Nevertheless, laminins 1, 8, and 10 supported PMN migration, indicating that differential cellular signaling via laminins is independent of the extent of adhesion. The data demonstrate that adhesive and nonadhesive interactions with components of the endothelial cell basement membrane and subjacent interstitium play decisive roles in controlling PMN movement into sites of inflammation and illustrate that beta(2)-integrins are not essential for such interactions.}, author = {Sixt, Michael K and Hallmann, Rupert and Wendler, Olaf and Scharffetter Kochanek, Karin and Sorokin, Lydia}, issn = {0021-9258}, journal = {Journal of Biological Chemistry}, number = {22}, pages = {18878 -- 18887}, publisher = {American Society for Biochemistry and Molecular Biology}, title = {{Cell adhesion and migration properties of β2-integrin negative polymorphonuclear granulocytes on defined extracellular matrix molecules. Relevance for leukocyte extravasation}}, doi = {10.1074/jbc.M010898200}, volume = {276}, year = {2001}, } @article{3927, abstract = {TNF-alpha has been clearly identified as central mediator of T cell activation-induced acute hepatic injury in mice, e.g., Con A hepatitis. In this model, liver injury depends on both TNFRs, i.e., the 55-kDa TNFR1 as well as the 75-kDa TNFR2. We show in this report that the hepatic TNFRs are not transcriptionally regulated, but are regulated by receptor shedding. TNF directly mediates hepatocellular death by activation of TNFR1 but also induces the expression of inflammatory proteins, such as cytokines and adhesion molecules. Here we provide evidence that resistance of TNFR1(-/-) and TNFR2(-/-) mice against Con A hepatitis is not due to an impaired production of the central mediators TNF and IFN-gamma. Con A injection results in a massive induction of ICAM-1, VCAM-1, and E-selectin in the liver. Lack of either one of both TNFRs did not change adhesion molecule expression in the livers of Con A-treated mice, presumably reflecting the fact that other endothelial cell-activating cytokines up-regulated adhesion molecule expression. However, treatment of TNFR1(-/-) and TNFR2(-/-) mice with murine rTNF revealed a predominant role for TNFR1 for the induction of hepatic adhesion molecule expression. Pretreatment with blocking Abs against E- and P-selectin or of ICAM(-/-) mice with anti-VCAM-1 Abs failed to prevent Con A hepatitis, although accumulation of the critical cell population, i.e., CD4(+) T cells was significantly inhibited. Hence, up-regulation of adhesion molecules during acute hepatitis unlikely contributes to organ injury but rather represents a defense mechanism.}, author = {Wolf, Dominik and Hallmann, Rupert and Sass, Gabriele and Sixt, Michael K and Küsters, Sabine and Fregien, Bastian and Trautwein, Christian and Tiegs, Gisa}, issn = {0022-1767}, journal = {Journal of Immunology}, number = {2}, pages = {1300 -- 1307}, publisher = {American Association of Immunologists}, title = {{TNF-α-induced expression of adhesion molecules in the liver is under the control of TNFR1--relevance for concanavalin A-induced hepatitis}}, doi = {10.4049/jimmunol.166.2.1300}, volume = {166}, year = {2001}, } @article{3930, abstract = {An active involvement of blood-brain barrier endothelial cell basement membranes in development of inflammatory lesions in the central nervous system (CNS) has not been considered to date. Here we investigated the molecular composition and possible function of the extracellular matrix encountered by extravasating T lymphocytes during experimental autoimmune encephalomyelitis (EAE). Endothelial basement membranes contained laminin 8 (alpha4beta1gamma1) and/or 10 (alpha5beta1gamma1) and their expression was influenced by proinflammatory cytokines or angiostatic agents. T cells emigrating into the CNS during EAE encountered two biochemically distinct basement membranes, the endothelial (containing laminins 8 and 10) and the parenchymal (containing laminins 1 and 2) basement membranes. However, inflammatory cuffs occurred exclusively around endothelial basement membranes containing laminin 8, whereas in the presence of laminin 10 no infiltration was detectable. In vitro assays using encephalitogenic T cell lines revealed adhesion to laminins 8 and 10, whereas binding to laminins 1 and 2 could not be induced. Downregulation of integrin alpha6 on cerebral endothelium at sites of T cell infiltration, plus a high turnover of laminin 8 at these sites, suggested two possible roles for laminin 8 in the endothelial basement membrane: one at the level of the endothelial cells resulting in reduced adhesion and, thereby, increased penetrability of the monolayer; and secondly at the level of the T cells providing direct signals to the transmigrating cells.}, author = {Sixt, Michael K and Engelhardt, Britta and Pausch, Friederike and Hallmann, Rupert and Wendler, Olaf and Sorokin, Lydia}, issn = {0021-9525}, journal = {Journal of Cell Biology}, number = {5}, pages = {933 -- 946}, publisher = {Rockefeller University Press}, title = {{Endothelial cell laminin isoforms, laminins 8 and 10, play decisive roles in T cell recruitment across the blood-brain barrier in experimental autoimmune encephalomyelitis}}, doi = {10.1083/jcb.153.5.933 }, volume = {153}, year = {2001}, }