TY - CONF
AB - Conventional type systems specify interfaces in terms of values and domains. We present a light-weight formalism that captures the temporal aspects of software component interfaces. Specifically, we use an automata-based language to capture both input assumptions about the order in which the methods of a component are called, and output guarantees about the order in which the component calls external methods. The formalism supports automatic compatability checks between interface models, and thus constitutes a type system for component interaction. Unlike traditional uses of automata, our formalism is based on an optimistic approach to composition, and on an alternating approach to design refinement. According to the optimistic approach, two components are compatible if there is some environment that can make them work together. According to the alternating approach, one interface refines another if it has weaker input assumptions, and stronger output guarantees. We show that these notions have game-theoretic foundations that lead to efficient algorithms for checking compatibility and refinement.
AU - de Alfaro, Luca
AU - Thomas Henzinger
ID - 4622
TI - Interface automata
ER -
TY - CONF
AB - We classify component-based models of computation into component models and interface models. A component model specifies for each component howthe component behaves in an arbitrary environment; an interface model specifies for each component what the component expects from the environment. Component models support compositional abstraction, and therefore component-based verification. Interface models support compositional refinement, and therefore componentbased design. Many aspects of interface models, such as compatibility and refinement checking between interfaces, are properly viewed in a gametheoretic setting, where the input and output values of an interface are chosen by different players.
AU - de Alfaro, Luca
AU - Thomas Henzinger
ID - 4623
TI - Interface theories for component-based design
VL - 2211
ER -
TY - CONF
AB - We present a compositional trace-based model for probabilistic systems. The behavior of a system with probabilistic choice is a stochastic process, namely, a probability distribution on traces, or “bundle.” Consequently, the semantics of a system with both nondeterministic and probabilistic choice is a set of bundles. The bundles of a composite system can be obtained by combining the bundles of the components in a simple mathematical way. Refinement between systems is bundle containment. We achieve assume-guarantee compositionality for bundle semantics by introducing two scoping mechanisms. The first mechanism, which is standard in compositional modeling, distinguishes inputs from outputs and hidden state. The second mechanism, which arises in probabilistic systems, partitions the state into probabilistically independent regions.
AU - de Alfaro, Luca
AU - Thomas Henzinger
AU - Jhala, Ranjit
ID - 4632
TI - Compositional methods for probabilistic systems
VL - 2154
ER -
TY - CONF
AB - A procedure for the analysis of state spaces is called symbolic if it manipulates not individual states, but sets of states that are represented by constraints. Such a procedure can be used for the analysis of infinite state spaces, provided termination is guaranteed. We present symbolic procedures, and corresponding termination criteria, for the solution of infinite-state games, which occur in the control and modular verification of infinite-state systems. To characterize the termination of symbolic procedures for solving infinite-state games, we classify these game structures into four increasingly restrictive categories:
1 Class 1 consists of infinite-state structures for which all safety and reachability games can be solved.
2 Class 2 consists of infinite-state structures for which all ω-regular games can be solved.
3 Class 3 consists of infinite-state structures for which all nested positive boolean combinations of ω-regular games can be solved.
4 Class 4 consists of infinite-state structures for which all nested boolean combinations of ω-regular games can be solved.
We give a structural characterization for each class, using equivalence relations on the state spaces of games which range from game versions of trace equivalence to a game version of bisimilarity. We provide infinite-state examples for all four classes of games from control problems for hybrid systems. We conclude by presenting symbolic algorithms for the synthesis of winning strategies (“controller synthesis”) for infinitestate games with arbitrary ω-regular objectives, and prove termination over all class-2 structures. This settles, in particular, the symbolic controller synthesis problem for rectangular hybrid systems.
AU - de Alfaro, Luca
AU - Thomas Henzinger
AU - Majumdar, Ritankar S
ID - 4633
TI - Symbolic algorithms for infinite-state games
VL - 2154
ER -
TY - CONF
AB - A controller is an environment for a system that achieves a particular control objective by providing inputs to the system without constraining the choices of the system. For synchronous systems, where system and controller make simultaneous and interdependent choices, the notion that a controller must not constrain the choices of the system can be formalized by type systems for composability. In a previous paper, we solved the control problem for static and dynamic types: a static type is a dependency relation between inputs and outputs, and composition is well-typed if it does not introduce cyclic dependencies; a dynamic type is a set of static types, one for each state. Static and dynamic types, however, cannot capture many important digital circuits, such as gated clocks, bidirectional buses, and random-access memory. We therefore introduce more general type systems, so-called dependent and bidirectional types, for modeling these situations, and we solve the corresponding control problems.
In a system with a dependent type, the dependencies between inputs and outputs are determined gradually through a game of the system against the controller. In a system with a bidirectional type, also the distinction between inputs and outputs is resolved dynamically by such a game. The game proceeds in several rounds. In each round the system and the controller choose to update some variables dependent on variables that have already been updated. The solution of the control problem for dependent and bidirectional types is based on algorithms for solving these games.
AU - de Alfaro, Luca
AU - Thomas Henzinger
AU - Mang, Freddy Y
ID - 4634
TI - The control of synchronous systems, Part II
VL - 2154
ER -
TY - CONF
AB - We show how model checking techniques can be applied to the analysis of connectivity and cost-of-traversal properties of Web sites.
AU - de Alfaro, Luca
AU - Thomas Henzinger
AU - Mang, Freddy Y
ID - 4635
TI - MCWEB: A model-checking tool for web-site debugging
ER -
TY - CONF
AB - Abstract. Dynamic programs, or fixpoint iteration schemes, are useful for solving many problems on state spaces, including model checking on Kripke structures (“verification”), computing shortest paths on weighted graphs (“optimization”), computing the value of games played on game graphs (“control”). For Kripke structures, a rich fixpoint theory is available in the form of the µ-calculus. Yet few connections have been made between different interpretations of fixpoint algorithms. We study the question of when a particular fixpoint iteration scheme ϕ for verifying an ω-regular property Ψ on a Kripke structure can be used also for solving a two-player game on a game graph with winning objective Ψ. We provide a sufficient and necessary criterion for the answer to be affirmative in the form of an extremal-model theorem for games: under a game interpretation, the dynamic program ϕ solves the game with objective Ψ if and only if both (1) under an existential interpretation on Kripke structures, ϕ is equivalent to ∃Ψ, and (2) under a universal interpretation on Kripke structures, ϕ is equivalent to ∀Ψ. In other words, ϕ is correct on all two-player game graphs iff it is correct on all extremal game graphs, where one or the other player has no choice of moves. The theorem generalizes to quantitative interpretations, where it connects two-player games with costs to weighted graphs. While the standard translations from ω-regular properties to the µ-calculus violate (1) or (2), we give a translation that satisfies both conditions. Our construction, therefore, yields fixpoint iteration schemes that can be uniformly applied on Kripke structures, weighted graphs, game graphs, and game graphs with costs, in order to meet or optimize a given ω-regular objective.
AU - de Alfaro, Luca
AU - Thomas Henzinger
AU - Majumdar, Ritankar S
ID - 4636
TI - From verification to control: dynamic programs for omega-regular objectives
ER -
TY - JOUR
AB - In this Note we present pairs of hyperkähler orbifolds which satisfy two different versions of mirror symmetry. On the one hand, we show that their Hodge numbers (or more precisely, stringy E-polynomials) are equal. On the other hand, we show that they satisfy the prescription of Strominger, Yau, and Zaslow (which in the present case goes back to Bershadsky, Johansen, Sadov and Vafa): that a Calabi-Yau and its mirror should fiber over the same real manifold, with special Lagrangian fibers which are tori dual to each other. Our examples arise as moduli spaces of local systems on a curve with structure group SL(n); the mirror is the corresponding space with structure group PGL(n). The special Lagrangian tori come from an algebraically completely integrable Hamiltonian system: the Hitchin system.
AU - Tamas Hausel
AU - Thaddeus, Michael
ID - 1452
IS - 4
JF - Comptes Rendus de l'Academie des Sciences - Series I: Mathematics
TI - Examples of mirror partners arising from integrable systems
VL - 333
ER -
TY - JOUR
AB - In this Letter we exhibit a one-parameter family of new Taub-NUT instantons parameterized by a half-line. The endpoint of the half-line will be the reducible Yang-Mills instanton corresponding to the Eguchi-Hanson-Gibbons L2 harmonic 2-form, while at an inner point we recover the Pope-Yuille instanton constructed as a projection of the Levi-Civitá connection onto the positive su(2)+ ⊂ so(4) subalgebra. Our method imitates the Jackiw-Nohl-Rebbi construction originally designed for flat R4. That is we find a one-parameter family of harmonic functions on the Taub-NUT space with a point singularity, rescale the metric and project the obtained Levi-Civitá connection onto the other negative su(2)- ⊂ so(4) part. Our solutions will possess the full U(2) symmetry, and thus provide more solutions to the recently proposed U(2) symmetric ansatz of Kim and Yoon.
AU - Etesi, Gábor
AU - Tamas Hausel
ID - 1453
IS - 1-2
JF - Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics
TI - Geometric construction of new Yang-Mills instantons over Taub-NUT space
VL - 514
ER -
TY - JOUR
AB - We address the problem of finding Abelian instantons of finite energy on the Euclidean Schwarzschild manifold. This amounts to construct self-dual L2 harmonic 2-forms on the space. Gibbons found a non-topological L2 harmonic form in the Taub-NUT metric, leading to Abelian instantons with continuous energy. We imitate his construction in the case of the Euclidean Schwarzschild manifold and find a non-topological self-dual L2 harmonic 2-form on it. We show how this gives rise to Abelian instantons and identify them with SU(2)-instantons of Pontryagin number 2n2 found by Charap and Duff in 1977. Using results of Dodziuk and Hitchin we also calculate the full L2 harmonic space for the Euclidean Schwarzschild manifold.
AU - Etesi, Gábor
AU - Tamas Hausel
ID - 1454
IS - 1-2
JF - Journal of Geometry and Physics
TI - Geometric interpretation of Schwarzschild instantons
VL - 37
ER -
TY - JOUR
AB - BACKGROUND: Detection of changes in a protein's evolutionary rate may reveal cases of change in that protein's function. We developed and implemented a simple relative rates test in an attempt to assess the rate constancy of protein evolution and to detect cases of functional diversification between orthologous proteins. The test was performed on clusters of orthologous protein sequences from complete bacterial genomes (Chlamydia trachomatis, C. muridarum and Chlamydophila pneumoniae), complete archaeal genomes (Pyrococcus horikoshii, P. abyssi and P. furiosus) and partially sequenced mammalian genomes (human, mouse and rat). RESULTS: Amino-acid sequence evolution rates are significantly correlated on different branches of phylogenetic trees representing the great majority of analyzed orthologous protein sets from all three domains of life. However, approximately 1% of the proteins from each group of species deviates from this pattern and instead shows variation that is consistent with an acceleration of the rate of amino-acid substitution, which may be due to functional diversification. Most of the putative functionally diversified proteins from all three species groups are predicted to function at the periphery of the cells and mediate their interaction with the environment. CONCLUSIONS: Relative rates of protein evolution are remarkably constant for the three species groups analyzed here. Deviations from this rate constancy are probably due to changes in selective constraints associated with diversification between orthologs. Functional diversification between orthologs is thought to be a relatively rare event. However, the resolution afforded by the test designed specifically for genomic-scale datasets allowed us to identify numerous cases of possible functional diversification between orthologous proteins.
AU - Jordan, Ingo K
AU - Fyodor Kondrashov
AU - Rogozin, Igor B
AU - Tatusov, Roman L
AU - Wolf, Yuri I
AU - Koonin, Eugene V
ID - 888
IS - 12
JF - Genome Biology
TI - Constant relative rate of protein evolution and detection of functional diversification among bacterial, archaeal and eukaryotic proteins
VL - 2
ER -
TY - JOUR
AB - 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.
AU - Wolf, Dominik
AU - Hallmann, Rupert
AU - Sass, Gabriele
AU - Michael Sixt
AU - Küsters, Sabine
AU - Fregien, Bastian
AU - Trautwein, Christian
AU - Tiegs, Gisa
ID - 3927
IS - 2
JF - Journal of Immunology
TI - TNF-α-induced expression of adhesion molecules in the liver is under the control of TNFR1--relevance for concanavalin A-induced hepatitis
VL - 166
ER -
TY - JOUR
AB - 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.
AU - Michael Sixt
AU - Hallmann, Rupert
AU - Wendler, Olaf
AU - Scharffetter-Kochanek, Karin
AU - Sorokin, Lydia M
ID - 3928
IS - 22
JF - Journal of Biological Chemistry
TI - Cell adhesion and migration properties of β2-integrin negative polymorphonuclear granulocytes on defined extracellular matrix molecules. Relevance for leukocyte extravasation
VL - 276
ER -
TY - JOUR
AB - 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.
AU - Michael Sixt
AU - Engelhardt, Britta
AU - Pausch, Friederike
AU - Hallmann, Rupert
AU - Wendler, Olaf
AU - Sorokin, Lydia M
ID - 3930
IS - 5
JF - Journal of Cell Biology
TI - Endothelial cell laminin isoforms, laminins 8 and 10, play decisive roles in T cell recruitment across the blood-brain barrier in experimental autoimmune encephalomyelitis
VL - 153
ER -
TY - JOUR
AB - 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.
AU - Cheng, Ho-Lun
AU - Herbert Edelsbrunner
AU - Fu, Ping
ID - 4001
IS - 2-3
JF - Computational Geometry: Theory and Applications
TI - Shape space from deformation
VL - 19
ER -
TY - JOUR
AB - 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.
AU - Cheng, Siu Wing
AU - Herbert Edelsbrunner
AU - Fu, Ping
AU - Lam, Ka Po
ID - 4002
IS - 2-3
JF - Computational Geometry: Theory and Applications
TI - Design and analysis of planar shape deformation
VL - 19
ER -
TY - CONF
AB - 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.
AU - Cheng, Ho-Lun
AU - Dey, Tamal K
AU - Herbert Edelsbrunner
AU - Sullivan, John
ID - 4005
TI - Dynamic skin triangulation
ER -
TY - JOUR
AB - 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.
AU - Herbert Edelsbrunner
ID - 4006
IS - 5
JF - Journal of Universal Computer Science
TI - 180 wrapped tubes
VL - 7
ER -
TY - JOUR
AB - 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.
AU - Cheng, Ho-Lun
AU - Dey, Tamal K
AU - Herbert Edelsbrunner
AU - Sullivan, John
ID - 4007
IS - 4
JF - Discrete & Computational Geometry
TI - Dynamic skin triangulation
VL - 25
ER -
TY - JOUR
AB - 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.
AU - Heisenberg, Carl-Philipp J
AU - Houart, Corinne
AU - Take Uchi, Masaya
AU - Rauch, Gerd
AU - Young, Neville
AU - Coutinho, Pedro
AU - Masai, Ichiro
AU - Caneparo, Luca
AU - Concha, Miguel
AU - Geisler, Robert
AU - Dale, Trevor
AU - Wilson, Stephen
AU - Stemple, Derek
ID - 4200
IS - 11
JF - Genes and Development
TI - A mutation in the Gsk3-binding domain of zebrafish Masterblind/Axin1 leads to a fate transformation of telencephalon and eyes to diencephalon
VL - 15
ER -