@article{4218,
abstract = {The molecular and cellular mechanisms governing cell motility and directed migration in response to the chemokine SDF-1 are largely unknown. Here, we demonstrate that zebrafish primordial germ cells whose migration is guided by SDF-1 generate bleb-like protrusions that are powered by cytoplasmic flow. Protrusions are formed at sites of higher levels of free calcium where activation of myosin contraction occurs. Separation of the acto-myosin cortex from the plasma membrane at these sites is followed by a flow of cytoplasm into the forming bleb. We propose that polarized activation of the receptor CXCR4 leads to a rise in free calcium that in turn activates myosin contraction in the part of the cell responding to higher levels of the ligand SDF-1. The biased formation of new protrusions in a particular region of the cell in response to SDF-1 defines the leading edge and the direction of cell migration.},
author = {Blaser, Heiko and Reichman Fried, Michal and Castanon, Irinka and Dumstrei, Karin and Marlow, Florence and Kawakami, Koichi and Solnica Krezel, Lilianna and Heisenberg, Carl-Philipp J and Raz, Erez},
journal = {Developmental Cell},
number = {5},
pages = {613 -- 627},
publisher = {Cell Press},
title = {{Migration of zebrafish primordial germ cells: A role for myosin contraction and cytoplasmic flow}},
doi = {10.1016/j.devcel.2006.09.023},
volume = {11},
year = {2006},
}
@article{4237,
abstract = {The growth function of populations is central in biomathematics. The main dogma is the existence of density-dependence mechanisms, which can be modelled with distinct functional forms that depend on the size of the Population. One important class of regulatory functions is the theta-logistic, which generalizes the logistic equation. Using this model as a motivation, this paper introduces a simple dynamical reformulation that generalizes many growth functions. The reformulation consists of two equations, one for population size, and one for the growth rate. Furthermore, the model shows that although population is density-dependent, the dynamics of the growth rate does not depend either on population size, nor on the carrying capacity. Actually, the growth equation is uncoupled from the population size equation, and the model has only two parameters, a Malthusian parameter rho and a competition coefficient theta. Distinct sign combinations of these parameters reproduce not only the family of theta-logistics, but also the van Bertalanffy, Gompertz and Potential Growth equations, among other possibilities. It is also shown that, except for two critical points, there is a general size-scaling relation that includes those appearing in the most important allometric theories, including the recently proposed Metabolic Theory of Ecology. With this model, several issues of general interest are discussed such as the growth of animal population, extinctions, cell growth and allometry, and the effect of environment over a population. (c) 2005 Elsevier Ltd. All rights reserved.},
author = {de Vladar, Harold},
journal = {Journal of Theoretical Biology},
number = {2},
pages = {245 -- 256},
publisher = {Elsevier},
title = {{Density-dependence as a size-independent regulatory mechanism}},
doi = {3802},
volume = {238},
year = {2006},
}
@article{8514,
abstract = {We study the extent to which the Hausdorff dimension of a compact subset of an infinite-dimensional Banach space is affected by a typical mapping into a finite-dimensional space. It is possible that the dimension drops under all such mappings, but the amount by which it typically drops is controlled by the ‘thickness exponent’ of the set, which was defined by Hunt and Kaloshin (Nonlinearity12 (1999), 1263–1275). More precisely, let $X$ be a compact subset of a Banach space $B$ with thickness exponent $\tau$ and Hausdorff dimension $d$. Let $M$ be any subspace of the (locally) Lipschitz functions from $B$ to $\mathbb{R}^{m}$ that contains the space of bounded linear functions. We prove that for almost every (in the sense of prevalence) function $f \in M$, the Hausdorff dimension of $f(X)$ is at least $\min\{ m, d / (1 + \tau) \}$. We also prove an analogous result for a certain part of the dimension spectra of Borel probability measures supported on $X$. The factor $1 / (1 + \tau)$ can be improved to $1 / (1 + \tau / 2)$ if $B$ is a Hilbert space. Since dimension cannot increase under a (locally) Lipschitz function, these theorems become dimension preservation results when $\tau = 0$. We conjecture that many of the attractors associated with the evolution equations of mathematical physics have thickness exponent zero. We also discuss the sharpness of our results in the case $\tau > 0$.},
author = {OTT, WILLIAM and HUNT, BRIAN and Kaloshin, Vadim},
issn = {0143-3857},
journal = {Ergodic Theory and Dynamical Systems},
number = {3},
pages = {869--891},
publisher = {Cambridge University Press},
title = {{The effect of projections on fractal sets and measures in Banach spaces}},
doi = {10.1017/s0143385705000714},
volume = {26},
year = {2006},
}
@inproceedings{8515,
abstract = {We consider the evolution of a set carried by a space periodic incompressible stochastic flow in a Euclidean space. We
report on three main results obtained in [8, 9, 10] concerning long time behaviour for a typical realization of the stochastic flow. First, at time t most of the particles are at a distance of order √t away from the origin. Moreover, we prove a Central Limit Theorem for the evolution of a measure carried by the flow, which holds for almost every realization of the flow. Second, we show the existence of a zero measure full Hausdorff dimension set of points, which
escape to infinity at a linear rate. Third, in the 2-dimensional case, we study the set of points visited by the original set by time t. Such a set, when scaled down by the factor of t, has a limiting non random shape.},
author = {Kaloshin, Vadim and DOLGOPYAT, D. and KORALOV, L.},
booktitle = {XIVth International Congress on Mathematical Physics},
isbn = {9789812562012},
location = {Lisbon, Portugal},
pages = {290--295},
publisher = {World Scientific},
title = {{Long time behaviour of periodic stochastic flows}},
doi = {10.1142/9789812704016_0026},
year = {2006},
}
@article{8513,
author = {Kaloshin, Vadim and Saprykina, Maria},
issn = {1553-5231},
journal = {Discrete & Continuous Dynamical Systems - A},
number = {2},
pages = {611--640},
publisher = {American Institute of Mathematical Sciences (AIMS)},
title = {{Generic 3-dimensional volume-preserving diffeomorphisms with superexponential growth of number of periodic orbits}},
doi = {10.3934/dcds.2006.15.611},
volume = {15},
year = {2006},
}
@article{8490,
abstract = {We demonstrate the feasibility of recording 1H–15N correlation spectra of proteins in only one second of acquisition time. The experiment combines recently proposed SOFAST-HMQC with Hadamard-type 15N frequency encoding. This allows site-resolved real-time NMR studies of kinetic processes in proteins with an increased time resolution. The sensitivity of the experiment is sufficient to be applicable to a wide range of molecular systems available at millimolar concentration on a high magnetic field spectrometer.},
author = {Schanda, Paul and Brutscher, Bernhard},
issn = {1090-7807},
journal = {Journal of Magnetic Resonance},
keywords = {Nuclear and High Energy Physics, Biophysics, Biochemistry, Condensed Matter Physics},
number = {2},
pages = {334--339},
publisher = {Elsevier},
title = {{Hadamard frequency-encoded SOFAST-HMQC for ultrafast two-dimensional protein NMR}},
doi = {10.1016/j.jmr.2005.10.007},
volume = {178},
year = {2006},
}
@article{8489,
abstract = {Structure elucidation of proteins by either NMR or X‐ray crystallography often requires the screening of a large number of samples for promising protein constructs and optimum solution conditions. For large‐scale screening of protein samples in solution, robust methods are needed that allow a rapid assessment of the folding of a polypeptide under diverse sample conditions. Here we present HET‐SOFAST NMR, a highly sensitive new method for semi‐quantitative characterization of the structural compactness and heterogeneity of polypeptide chains in solution. On the basis of one‐dimensional 1H HET‐SOFAST NMR data, obtained on well‐folded, molten globular, partially‐ and completely unfolded proteins, we define empirical thresholds that can be used as quantitative benchmarks for protein compactness. For 15N‐enriched protein samples, two‐dimensional 1H‐15N HET‐SOFAST correlation spectra provide site‐specific information about the structural heterogeneity along the polypeptide chain.},
author = {Schanda, Paul and Forge, Vincent and Brutscher, Bernhard},
issn = {0749-1581},
journal = {Magnetic Resonance in Chemistry},
number = {S1},
pages = {S177--S184},
publisher = {Wiley},
title = {{HET-SOFAST NMR for fast detection of structural compactness and heterogeneity along polypeptide chains}},
doi = {10.1002/mrc.1825},
volume = {44},
year = {2006},
}
@article{8488,
abstract = {We demonstrate for different protein samples that three-dimensional HNCO and HNCA correlation spectra may be recorded in a few minutes acquisition time using the band-selective excitation short-transient sequences presented here. This opens new perspectives for the NMR structural investigation of unstable protein samples and real-time site-resolved studies of protein kinetics.},
author = {Schanda, Paul and Van Melckebeke, Hélène and Brutscher, Bernhard},
issn = {0002-7863},
journal = {Journal of the American Chemical Society},
keywords = {Colloid and Surface Chemistry, Biochemistry, General Chemistry, Catalysis},
number = {28},
pages = {9042--9043},
publisher = {American Chemical Society},
title = {{Speeding up three-dimensional protein NMR experiments to a few minutes}},
doi = {10.1021/ja062025p},
volume = {128},
year = {2006},
}
@book{210,
abstract = {Harold Davenport was one of the truly great mathematicians of the twentieth century. Based on lectures he gave at the University of Michigan in the early 1960s, this book is concerned with the use of analytic methods in the study of integer solutions to Diophantine equations and Diophantine inequalities. It provides an excellent introduction to a timeless area of number theory that is still as widely researched today as it was when the book originally appeared. The three main themes of the book are Waring's problem and the representation of integers by diagonal forms, the solubility in integers of systems of forms in many variables, and the solubility in integers of diagonal inequalities. For the second edition of the book a comprehensive foreword has been added in which three prominent authorities describe the modern context and recent developments. A thorough bibliography has also been added.},
author = {Davenport, Harold and Timothy Browning},
booktitle = {Analytic methods for diophantine equations and diophantine inequalities},
pages = {1 -- 140},
publisher = {Cambridge University Press},
title = {{Analytic methods for diophantine equations and diophantine inequalities}},
doi = {10.1017/CBO9780511542893},
year = {2005},
}
@article{211,
abstract = {Let f ∈ ℤ[x] be a polynomial of degree d. The paucity of non-trivial positive integer solutions to the equation f(x1)+f(x 2)=f(x3)+f(x4) is established, provided that d ≤ 7$. Also the corresponding situation is investigated for equal sums of three like polynomials.},
author = {Timothy Browning},
journal = {Bulletin of the London Mathematical Society},
number = {6},
pages = {801 -- 808},
publisher = {John Wiley and Sons Ltd},
title = {{Equal sums of like polynomials}},
doi = {10.1112/S0024609305004741},
volume = {37},
year = {2005},
}
@article{212,
abstract = {For any n ≧ 2, let F ∈ ℤ [ x 1, … , xn ] be a form of degree d≧ 2, which produces a geometrically irreducible hypersurface in ℙn–1. This paper is concerned with the number N(F;B) of rational points on F = 0 which have height at most B. For any ε > 0 we establish the estimate N(F; B) = O(B n− 2+ ε ), whenever either n ≦ 5 or the hypersurface is not a union of lines. Here the implied constant depends at most upon d, n and ε.},
author = {Timothy Browning and Heath-Brown, Roger},
journal = {Journal fur die Reine und Angewandte Mathematik},
number = {584},
pages = {83 -- 115},
publisher = {Walter de Gruyter and Co },
title = {{Counting rational points on hypersurfaces}},
doi = {https://doi.org/10.1515/crll.2005.2005.584.83},
year = {2005},
}
@article{214,
abstract = {Given an absolutely irreducible ternary form F, the purpose of this paper is to produce better upper bounds for the number of integer solutions to the equation F=0, that are restricted to lie in very lopsided boxes. As an application of the main result, a new paucity estimate is obtained for equal sums of two like powers.},
author = {Timothy Browning and Heath-Brown, Roger},
journal = {Mathematische Zeitschrift},
number = {2},
pages = {233 -- 247},
publisher = {Unknown},
title = {{Plane curves in boxes and equal sums of two powers}},
doi = {10.1007/s00209-004-0719-z},
volume = {251},
year = {2005},
}
@article{217,
abstract = {We show that the number of nontrivial rational points of height at most B, which lie on the cubic surface x1 x2 x3 = x4 (x1 + x2 + x3)2, has order of magnitude B (log B)6. This agrees with Manin's conjecture.},
author = {Timothy Browning},
journal = {Journal of Number Theory},
number = {2},
pages = {242 -- 283},
publisher = {Elsevier},
title = {{The density of rational points on a certain singular cubic surface}},
doi = {10.1016/j.jnt.2005.11.007},
volume = {119},
year = {2005},
}
@article{2307,
abstract = {The human norepinephrine (NE) transporter (hNET) attenuates neuronal signaling by rapid NE clearance from the synaptic cleft, and NET is a target for cocaine and amphetamines as well as therapeutics for depression, obsessive-compulsive disorder, and post-traumatic stress disorder. In spite of its central importance in the nervous system, little is known about how NET substrates, such as NE, 1-methyl-4-tetrahydropyridinium (MPP+), or amphetamine, interact with NET at the molecular level. Nor do we understand the mechanisms behind the transport rate. Previously we introduced a fluorescent substrate similar to MPP+, which allowed separate and simultaneous binding and transport measurement (Schwartz, J. W., Blakely, R. D., and DeFelice, L. J. (2003) J. Biol. Chem. 278, 9768-9777). Here we use this substrate, 4-(4-(dimethylamino)styrl)-N-methyl-pyridinium (ASP+), in combination with green fluorescent protein-tagged hNETs to measure substrate-transporter stoichiometry and substrate binding kinetics. Calibrated confocal microscopy and fluorescence correlation spectroscopy reveal that hNETs, which are homo-multimers, bind one substrate molecule per transporter subunit. Substrate residence at the transporter, obtained from rapid on-off kinetics revealed in fluorescence correlation spectroscopy, is 526 μs. Substrate residence obtained by infinite dilution is 1000 times slower. This novel examination of substrate-transporter kinetics indicates that a single ASP + molecule binds and unbinds thousands of times before being transported or ultimately dissociated from hNET. Calibrated fluorescent images combined with mass spectroscopy give a transport rate of 0.06 ASP +/hNET-protein/s, thus 36,000 on-off binding events (and 36 actual departures) occur for one transport event. Therefore binding has a low probability of resulting in transport. We interpret these data to mean that inefficient binding could contribute to slow transport rates.},
author = {Schwartz, Joel W and Gaia Novarino and Piston, David W and DeFelice, Louis J},
journal = {Journal of Biological Chemistry},
number = {19},
pages = {19177 -- 19184},
publisher = {American Society for Biochemistry and Molecular Biology},
title = {{Substrate binding stoichiometry and kinetics of the norepinephrine transporter}},
doi = {10.1074/jbc.M412923200},
volume = {280},
year = {2005},
}
@book{2335,
abstract = {This book contains a unique survey of the mathematically rigorous results about the quantum-mechanical many-body problem that have been obtained by the authors in the past seven years. It addresses a topic that is not only rich mathematically, using a large variety of techniques in mathematical analysis, but is also one with strong ties to current experiments on ultra-cold Bose gases and Bose-Einstein condensation. The book provides a pedagogical entry into an active area of ongoing research for both graduate students and researchers. It is an outgrowth of a course given by the authors for graduate students and post-doctoral researchers at the Oberwolfach Research Institute in 2004. The book also provides a coherent summary of the field and a reference for mathematicians and physicists active in research on quantum mechanics.},
author = {Lieb, Élliott H and Robert Seiringer and Solovej, Jan P and Yngvason, Jakob},
booktitle = {The mathematics of the Bose gas and its condensation},
publisher = {Birkhäuser},
title = {{The mathematics of the Bose gas and its condensation}},
volume = {34},
year = {2005},
}
@inbook{2336,
abstract = {
Now that the low temperature properties of quantum-mechanical many-body systems (bosons) at low density, ρ, can be examined experimentally it is appropriate to revisit some of the formulas deduced by many authors 4–5 decades ago, and to explore new regimes not treated before. For systems with repulsive (i.e. positive) interaction potentials the experimental low temperature state and the ground state are effectively synonymous — and this fact is used in all modeling. In such cases, the leading term in the energy/particle is 2πħ2 aρ/m where a is the scattering length of the two-body potential. Owing to the delicate and peculiar nature of bosonic correlations (such as the strange N 7/5 law for charged bosons), four decades of research failed to establish this plausible formula rigorously. The only previous lower bound for the energy was found by Dyson in 1957, but it was 14 times too small. The correct asymptotic formula has been obtained by us and this work will be presented. The reason behind the mathematical difficulties will be emphasized. A different formula, postulated as late as 1971 by Schick, holds in two dimensions and this, too, will be shown to be correct. With the aid of the methodology developed to prove the lower bound for the homogeneous gas, several other problems have been successfully addressed. One is the proof by us that the Gross-Pitaevskii equation correctly describes the ground state in the ‘traps’ actually used in the experiments. For this system it is also possible to prove complete Bose condensation and superfluidity as we have shown. On the frontier of experimental developments is the possibility that a dilute gas in an elongated trap will behave like a one-dimensional system; we have proved this mathematically. Another topic is a proof that Foldy’s 1961 theory of a high density Bose gas of charged particles correctly describes its ground state energy; using this we can also prove the N 7/5 formula for the ground state energy of the two-component charged Bose gas proposed by Dyson in 1967. All of this is quite recent work and it is hoped that the mathematical methodology might be useful, ultimately, to solve more complex problems connected with these interesting systems.},
author = {Lieb, Élliott H and Robert Seiringer and Solovej, Jan P and Yngvason, Jakob},
booktitle = {Perspectives in Analysis},
editor = {Benedicks, Michael and Jones, Peter W and Smirnov, Stanislav and Winckler, Björn},
pages = {97 -- 183},
publisher = {Springer},
title = {{The quantum-mechanical many-body problem: The Bose gas}},
doi = {10.1007/3-540-30434-7_9},
volume = {27},
year = {2005},
}
@article{2359,
abstract = {The validity of substituting a c-number z for the k = 0 mode operator a0 is established rigorously in full generality, thereby verifying one aspect of Bogoliubov's 1947 theory. This substitution not only yields the correct value of thermodynamic quantities such as the pressure or ground state energy, but also the value of |z|2 that maximizes the partition function equals the true amount of condensation in the presence of a gauge-symmetry-breaking term. This point had previously been elusive.},
author = {Lieb, Élliott H and Robert Seiringer and Yngvason, Jakob},
journal = {Physical Review Letters},
number = {8},
publisher = {American Physical Society},
title = {{Justification of c-number substitutions in bosonic hamiltonians}},
doi = {10.1103/PhysRevLett.94.080401},
volume = {94},
year = {2005},
}
@article{2361,
abstract = {The strong subadditivity of entropy plays a key role in several areas of physics and mathematics. It states that the entropy S[±]=- Tr(Ï±lnÏ±) of a density matrix Ï±123 on the product of three Hilbert spaces satisfies S[Ï±123]- S[Ï±12]≤S[Ï±23]-S[Ï±2]. We strengthen this to S[Ï±123]-S[Ï±12] ≤αnα(S[Ï±23α]-S[Ï±2α]), where the nα are weights and the Ï±23α are partitions of Ï±23. Correspondingly, there is a strengthening of the theorem that the map A|Trexp[L+lnA] is concave. As applications we prove some monotonicity and convexity properties of the Wehrl coherent state entropy and entropy inequalities for quantum gases.},
author = {Lieb, Élliott H and Robert Seiringer},
journal = {Physical Review A - Atomic, Molecular, and Optical Physics},
number = {6},
publisher = {American Physical Society},
title = {{Stronger subadditivity of entropy}},
doi = {10.1103/PhysRevA.71.062329},
volume = {71},
year = {2005},
}
@article{2362,
abstract = {Recent developments in the physics of low-density trapped gases make it worthwhile to verify old, well-known results that, while plausible, were based on perturbation theory and assumptions about pseudopotentials. We use and extend recently developed techniques to give a rigorous derivation of the asymptotic formula for the ground-state energy of a dilute gas of N fermions interacting with a short-range, positive potential of scattering length a. For spin-12 fermions, this is E∼E0+(22m)2πNa, where E0 is the energy of the noninteracting system and is the density. A similar formula holds in two dimensions (2D), with a replaced by ln(a2). Obviously this 2D energy is not the expectation value of a density-independent pseudopotential.},
author = {Lieb, Élliott H and Robert Seiringer and Solovej, Jan P},
journal = {Physical Review A - Atomic, Molecular, and Optical Physics},
number = {5},
publisher = {American Physical Society},
title = {{Ground state energy of the low density Fermi gas}},
doi = {10.1103/PhysRevA.71.053605},
volume = {71},
year = {2005},
}
@article{2427,
abstract = {Intersection graphs of disks and of line segments, respectively, have been well studied, because of both practical applications and theoretically interesting properties of these graphs. Despite partial results, the complexity status of the Clique problem for these two graph classes is still open. Here, we consider the Clique problem for intersection graphs of ellipses, which, in a sense, interpolate between disks and line segments, and show that the problem is APX-hard in that case. Moreover, this holds even if for all ellipses, the ratio of the larger over the smaller radius is some prescribed number. Furthermore, the reduction immediately carries over to intersection graphs of triangles. To our knowledge, this is the first hardness result for the Clique problem in intersection graphs of convex objects with finite description complexity. We also describe a simple approximation algorithm for the case of ellipses for which the ratio of radii is bounded.},
author = {Ambühl, Christoph and Uli Wagner},
journal = {Theory of Computing Systems},
number = {3},
pages = {279 -- 292},
publisher = {Springer},
title = {{The Clique problem in intersection graphs of ellipses and triangles}},
doi = {10.1007/s00224-005-1141-6},
volume = {38},
year = {2005},
}
@inproceedings{2428,
abstract = {We consider an online version of the conflict-free coloring of a set of points on the line, where each newly inserted point must be assigned a color upon insertion, and at all times the coloring has to be conflict-free, in the sense that in every interval I there is a color that appears exactly once in I. We present several deterministic and randomized algorithms for achieving this goal, and analyze their performance, that is, the maximum number of colors that they need to use, as a function of the number n of inserted points. We first show that a natural and simple (deterministic) approach may perform rather poorly, requiring Ω(√n) colors in the worst case. We then modify this approach, to obtain an efficient deterministic algorithm that uses a maximum of Θ(log 2 n) colors. Next, we present two randomized solutions. The first algorithm requires an expected number of at most O(log 2 n) colors, and produces a coloring which is valid with high probability, and the second one, which is a variant of our efficient deterministic algorithm, requires an expected number of at most O(log n log log n) colors but always produces a valid coloring. We also analyze the performance of the simplest proposed algorithm when the points are inserted in a random order, and present an incomplete analysis that indicates that, with high probability, it uses only O(log n) colors. Finally, we show that in the extension of this problem to two dimensions, where the relevant ranges are disks, n colors may be required in the worst case. The average-case behavior for disks, and cases involving other planar ranges, are still open.},
author = {Fiat, Amos and Levy, Meital B and Matoušek, Jiří and Pach, Elchanan M and Sharir, Micha and Smorodinsky, Shakhar and Uli Wagner and Welzl, Emo},
pages = {545 -- 554},
publisher = {SIAM},
title = {{Online conflict-free coloring for intervals}},
doi = {10.1137/S0097539704446682},
year = {2005},
}
@article{2455,
abstract = {Local accumulation of the plant growth regulator auxin mediates pattern formation in Arabidopsis roots and influences outgrowth and development of lateral root- and shoot-derived primordia. However, it has remained unclear how auxin can simultaneously regulate patterning and organ outgrowth and how its distribution is stabilized in a primordium-specif ic manner. Here we show that five PIN genes collectively control auxin distribution to regulate cell division and cell expansion in the primary root. Furthermore, the joint action of these genes has an important role in pattern formation by focusing the auxin maximum and restricting the expression domain of PLETHORA (PLT) genes, major determinants for root stem cell specification. In turn, PLT genes are required for PIN gene transcription to stabilize the auxin maximum at the distal root tip. Our data reveal an interaction network of auxin transport facilitators and root fate determinants that control patterning and growth of the root primordium.},
author = {Billou, Ikram and Xu, Jian and Wildwater, Marjolein and Willemsen, Viola and Paponov, Ivan A and Jirí Friml and Heldstra, Renze and Aida, Mitsuhiro and Palme, Klaus J and Scheres, Ben},
journal = {Nature},
number = {7021},
pages = {39 -- 44},
publisher = {Nature Publishing Group},
title = {{The PIN auxin efflux facilitator network controls growth and patterning in Arabidopsis roots}},
doi = {10.1038/nature03184},
volume = {433},
year = {2005},
}
@inbook{2463,
author = {Dubová, J and Hejátko, Jan and Jirí Friml},
booktitle = {Encyclopedia of Molecular Cell Biology and Molecular Medicine},
editor = {Meyers, Robert A},
pages = {249 -- 295},
publisher = {Wiley-Blackwell},
title = {{Reproduction, plants}},
doi = {10.1002/3527600906},
volume = {12},
year = {2005},
}
@inbook{2464,
author = {Jirí Friml and Wiśniewska, Justyna},
booktitle = {Intercellular Communication in Plants},
editor = {Fleming, Andrew J.},
publisher = {Wiley-Blackwell},
title = {{Auxin as an intercellular signal}},
volume = {16},
year = {2005},
}
@article{3915,
abstract = {In the ant Cardiocondyla obscurior, wingless males compete with nestmate males for access to female mating
partners, leading to local mate competition (LMC). Queen number varies between colonies, resulting in
variation in the strength of LMC. Cremer & Heinze (2002, Proceedings of the Royal Society of London, Series B,
269, 417–422) showed that colonies responded to increasing queen number by producing a less femalebiased
sex ratio, as predicted by LMC theory. However, the proximate mechanisms responsible for this
variation in the sex ratio could not be determined because the study was restricted to adult sex ratios.With
LMC, the primary sex ratio (proportion of haploid eggs laid by the queen) is expected to be female biased,
which lowers the conflict between queens and workers over sex allocation. We compared the primary sex
ratios laid by queens in monogynous and in polygynous experimental colonies of C. obscurior. The
proportion of haploid eggs laid by queens was significantly lower in single-queen than in multiple-queen
colonies. Furthermore, queens rapidly adjusted their primary sex ratios to changes in colony queen
number. This is the first report of an adaptive adjustment of the primary sex ratio in response to LMC by
ant queens.},
author = {De Menten, Ludivine and Cremer, Sylvia and Heinze, Jürgen and Aron, Serge},
journal = {Animal Behaviour},
number = {5},
pages = {1031 -- 1035},
publisher = {Elsevier},
title = {{Primary sex ratio adjustment by ant queens in response to local mate competition}},
doi = {10.1016/j.anbehav.2004.09.005},
volume = {69},
year = {2005},
}
@article{3916,
abstract = {Divergent reproductive interests of males and females often cause sexual conflict [1] and [2]. Males of many species manipulate females by transferring seminal fluids that boost female short-term fecundity while decreasing their life expectancy and future reproductivity [3] and [4]. The life history of ants, however, is expected to reduce sexual conflict; whereas most insect females show repeated phases of mating and reproduction, antqueens mate only during a short period early in life and undergo a lifelong commitment to their mates by storing sperm [5]. Furthermore, sexual offspring can only be reared after a sterile worker force has been built up [5]. Therefore, the males should also profit from a long female lifespan. In the antCardiocondyla obscurior, mating indeed has a positive effect on the lifetime reproductive success of queens. Queens that mated to either one fertile or one sterilized male lived considerably longer and started laying eggs earlier than virgin queens. Only queens that received viable sperm from fertile males showed increased fecundity. The lack of a trade-off between fecundity and longevity is unexpected, given evolutionary theories of aging [6]. Our data instead reveal the existence of sexual cooperation in ants.},
author = {Schrempf, Alexandra and Heinze, Jürgen and Cremer, Sylvia},
journal = {Current Biology},
number = {3},
pages = {267 -- 270},
publisher = {Cell Press},
title = {{Sexual cooperation: mating increases longevity in ant queens}},
doi = {10.1016/j.cub.2005.01.036},
volume = {15},
year = {2005},
}
@article{3933,
abstract = {Resident dendritic cells (DC) within the T cell area of the lymph node take up soluble antigens that enter via the afferent lymphatics before antigen carrying DC arrive from the periphery. The reticular network within the lymph node is a conduit system forming the infrastructure for the fast delivery of soluble substances from the afferent lymph to the lumen of high endothelial venules (HEVs). Using high-resolution light microscopy and 3D reconstruction, we show here that these conduits are unique basement membrane-like structures ensheathed by fibroblastic reticular cells with occasional resident DC embedded within this cell layer. Conduit-associated DC are capable of taking up and processing soluble antigens transported within the conduits, whereas immigrated mature DC occur remote from the reticular fibers. The conduit system is, therefore, not a closed compartment that shuttles substances through the lymph node but represents the morphological equivalent to the filtering function of the lymph node.},
author = {Sixt, Michael K and Kanazawa, Nobuo and Selg, Manuel and Samson, Thomas and Roos, Gunnel and Reinhardt, Dieter and Pabst, Reinhard and Lutz, Manfred and Sorokin, Lydia},
journal = {Immunity},
number = {1},
pages = {19 -- 29},
publisher = {Cell Press},
title = {{The conduit system transports soluble antigens from the afferent lymph to resident dendritic cells in the T cell area of the lymph node}},
doi = {10.1016/j.immuni.2004.11.013},
volume = {22},
year = {2005},
}
@inproceedings{3982,
abstract = {We present an efficient algorithm for generating a small set of coarse alignments between interacting proteins using meaningful features on their surfaces. The proteins are treated as rigid bodies, but the results are more generally useful as the produced configurations can serve as input to local improvement algorithms that allow for protein flexibility. We apply our algorithm to a diverse set of protein complexes from the Protein Data Bank, demonstrating the effectivity of our algorithm, both for bound and for unbound protein docking problems.},
author = {Wang, Yusu and Agarwal, Pankaj K and Brown, Paul and Herbert Edelsbrunner and Rudolph, Johannes},
pages = {64 -- 75},
publisher = {World Scientific Publishing},
title = {{Coarse and reliable geometric alignment for protein docking}},
doi = {10.1142/9789812702456_0007},
year = {2005},
}
@article{3983,
abstract = {Cdc25 phosphatases are key activators of the eukaryotic cell cycle and compelling anticancer targets because their overexpression has been associated with numerous cancers. However, drug discovery targeting these phosphatases has been hampered by the lack of structural information about how Cdc25s interact with their native protein substrates, the cyclin-dependent kinases. Herein, we predict a docked orientation for Cdc25B with its Cdk2-pTpY-CycA protein substrate by a rigid-body docking method and refine the docked models with full-scale molecular dynamics simulations and minimization. We validate the stable ensemble structure experimentally by a variety of in vitro and in vivo techniques. Specifically, we compare our model with a crystal structure of the substrate-trapping mutant of Cdc25B. We identify and validate in vivo a novel hot-spot residue on Cdc25B (Arg492) that plays a central role in protein substrate recognition. We identify a hot-spot residue on the Substrate Cdk2 (Asp206) and confirm its interaction with hot-spot residues on Cdc25 using hot-spot swapping and double mutant cycles to derive interaction energies. Our experimentally validated model is consistent with previous studies of Cdk2 and its interaction partners and initiates the opportunity for drug discovery of inhibitors that target the remote binding sites of this protein-protein interaction.},
author = {Sohn, Jungsan and Parks, Jerry M and Buhrman, Gregory and Brown, Paul and Kristjánsdóttir, Kolbrun and Safi, Alexias and Herbert Edelsbrunner and Yang, Weitao T and Rudolph, Johannes},
journal = {Biochemistry},
number = {50},
pages = {16563 -- 16573},
publisher = {ACS},
title = {{Experimental validation of the docking orientation of Cdc25 with its Cdk2-CycA protein substrate}},
doi = {10.1021/bi0516879},
volume = {44},
year = {2005},
}
@article{4138,
abstract = {Adaptive dynamics describes the evolution of an asexual population through the successive substitution of mutations of small effect. Waxman & Gavrilets (2005) give an excellent overview of the method and its applications. In this note, we focus on the plausibility of the key assumption that mutations have small effects, and the consequences of relaxing that assumption. We argue that: (i) successful mutations often have large effects; (ii) such mutations generate a qualitatively different evolutionary pattern, which is inherently stochastic; and (iii) in models of competition for a continuous resource, selection becomes very weak once several phenotypes are established. This makes the effects of introducing new mutations unpredictable using the methods of adaptive dynamics.
We should make clear at the outset that our criticism is of methods that rely on local analysis of fitness gradients (eqn 2 of Waxman & Gavrilets, 2005), and not of the broader idea that evolution can be understood by examining the invasion of successive mutations. We use the term ‘adaptive dynamics’ to refer to the former technique, and contrast it with a more general population genetic analysis of probabilities of invasion.},
author = {Nicholas Barton and Jitka Polechova},
journal = {Journal of Evolutionary Biology},
number = {5},
pages = {1186 -- 1190},
publisher = {Wiley-Blackwell},
title = {{The limitations of adaptive dynamics as a model of evolution}},
doi = {10.1111/j.1420-9101.2005.00943.x},
volume = {18},
year = {2005},
}
@article{4249,
abstract = {We examined causes of speciation in asexual populations in both sympatry and parapatry, providing an alternative explanation for the speciation patterns reported by Dieckmann and Doebeli (1999) and Doebeli and Dieckmann (2003). Both in sympatry and parapatry, they find that speciation occurs relatively easily. We reveal that in the sympatric clonal model, the equilibrium distribution is continuous and the disruptive selection driving evolution of discrete clusters is only transient. Hence, if discrete phenotypes are to remain stable in the sympatric sexual model, there should be some source of nontransient disruptive selection that will drive evolution of assortment. We analyze sexually reproducing populations using the Bulmer’s infinitesimal model and show that cost-free assortment alone leads to speciation and disruptive selection only arises when the optimal distribution cannot be matched—in this example, because the phenotypic range is limited. In addition, Doebeli and Dieckmann’s analyses assumed a high genetic variance and a high mutation rate. Thus, these theoretical models do not support the conclusion that sympatric speciation is a likely outcome of competition for resources. In their parapatric model (Doebeli and Dieckmann 2003), clustering into distinct phenotypes is driven by edge effects, rather than by frequency-dependent competition.},
author = {Jitka Polechova and Nicholas Barton},
journal = {Evolution; International Journal of Organic Evolution},
number = {6},
pages = {1194 -- 1210},
publisher = {Wiley-Blackwell},
title = {{Speciation through competition: A critical review}},
doi = {10.1111/j.0014-3820.2005.tb01771.x},
volume = {59},
year = {2005},
}
@article{4251,
abstract = {In finite populations subject to selection, genetic drift generates negative linkage disequilibrium, on average, even if selection acts independently (i.e. multiplicatively) upon all loci. Negative disequilibrium reduces the variance in fitness and hence, by FISHER's Fundamental Theorem (1930), slows the rate of increase in mean fitness. Modifiers that increase recombination eliminate the negative disequilibria that impede selection and consequently increase in frequency by 'hitch-hiking'. In addition, recombinant progeny are more fit on average than non-recombinant progeny when there is negative linkage disequilibrium and loci interact multiplicatively. For both these reasons, stochastic fluctuations in linkage disequilibrium in finite populations favor the evolution of increased rates of recombination, even in the absence of epistatic interactions among loci and even when disequilibrium is initially absent. The method developed within this paper quantifies the strength of selection on a modifier allele that increases recombination due to stochastically generated linkage disequilibria. The analysis indicates that, in a population subject to multiplicative selection, genetic associations generated by drift do select for increased recombination, a result that is confirmed by Monte Carlo simulations. Selection for a modifier that increases recombination is highest when linkage among all loci is tight, when beneficial alleles rise from low to high frequency, and when the population size is small.},
author = {Nicholas Barton and Otto, Sarah P},
journal = {Genetics},
number = {4},
pages = {2353 -- 2370},
publisher = {Genetics Society of America},
title = {{Evolution of recombination due to random drift}},
doi = {10.1534/genetics.104.032821},
volume = {169},
year = {2005},
}
@article{4252,
abstract = {Empirical studies of quantitative genetic variation have revealed robust patterns that are observed both across traits and across species. However, these patterns have no compelling explanation, and some of the observations even appear to be mutually incompatible. We review and extend a major class of theoretical models, ‘mutation–selection models’, that have been proposed to explain quantitative genetic variation. We also briefly review an alternative class of ‘balancing selection models’. We consider to what extent the models are compatible with the general observations, and argue that a key issue is understanding and modelling pleiotropy. We discuss some},
author = {Johnson, Toby and Nicholas Barton},
journal = {Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences},
number = {1459},
pages = {1411 -- 1425},
publisher = {Royal Society, The},
title = {{Theoretical models of selection and mutationon quantitative traits}},
doi = {10.1098/rstb.2005.1667},
volume = {360},
year = {2005},
}
@inproceedings{4367,
author = {Podelski,Andreas and Thomas Wies},
pages = {267 -- 282},
publisher = {Springer},
title = {{Boolean Heaps}},
doi = {1550},
year = {2005},
}
@inproceedings{4404,
author = {Alur, Rajeev and Pavol Cerny and Madhusudan,P. and Nam,Wonhong},
pages = {98 -- 109},
publisher = {ACM},
title = {{Synthesis of interface specifications for Java classes}},
doi = {1542},
year = {2005},
}
@inproceedings{4412,
abstract = {The periodic resource model for hierarchical, compositional scheduling abstracts task groups by resource requirements. We study this model in the presence of dataflow constraints between the tasks within a group (intragroup dependencies), and between tasks in different groups (inter-group dependencies). We consider two natural semantics for dataflow constraints, namely, RTW (real-time workshop) semantics and LET (logical execution time) semantics. We show that while RTW semantics offers better end-to-end latency on the task group level, LET semantics allows tighter resource bounds in the abstraction hierarchy and therefore provides better composability properties. This result holds both for intragroup and intergroup dependencies, as well as for shared and for distributed resources.},
author = {Matic, Slobodan and Thomas Henzinger},
pages = {99 -- 110},
publisher = {IEEE},
title = {{Trading end-to-end latency for composability}},
doi = {10.1109/RTSS.2005.43},
year = {2005},
}
@inproceedings{4418,
abstract = {We present a new software system architecture for the implementation of hard real-time applications. The core of the system is a microkernel whose reactivity (interrupt handling as in synchronous reactive programs) and proactivity (task scheduling as in traditional RTOSs) are fully programmable. The microkernel, which we implemented on a StrongARM processor, consists of two interacting domain-specific virtual machines, a reactive E (Embedded) machine and a proactive S (Scheduling) machine. The microkernel code (or microcode) that runs on the microkernel is partitioned into E and S code. E code manages the interaction of the system with the physical environment: the execution of E code is triggered by environment interrupts, which signal external events such as the arrival of a message or sensor value, and it releases application tasks to the S machine. S code manages the interaction of the system with the processor: the execution of S code is triggered by hardware interrupts, which signal internal events such as the completion of a task or time slice, and it dispatches application tasks to the CPU, possibly preempting a running task. This partition of the system orthogonalizes the two main concerns of real-time implementations: E code refers to environment time and thus defines the reactivity of the system in a hardware- and scheduler-independent fashion; S code refers to CPU time and defines a system scheduler. If both time lines can be reconciled, then the code is called time safe; violations of time safety are handled again in a programmable way, by run-time exceptions. The separation of E from S code permits the independent programming, verification, optimization, composition, dynamic adaptation, and reuse of both reaction and scheduling mechanisms. Our measurements show that the system overhead is very acceptable even for large sets of task, generally in the 0.2--0.3% range.},
author = {Kirsch, Christoph M and Sanvido, Marco A and Thomas Henzinger},
pages = {35 -- 45},
publisher = {ACM},
title = {{A programmable microkernel for real-time systems}},
doi = {10.1145/1064979.1064986},
year = {2005},
}
@article{4454,
abstract = {We define five increasingly comprehensive classes of infinite-state systems, called STS1--STS5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.STS1 These are the systems with finite bisimilarity quotients. They can be analyzed symbolically by iteratively applying predecessor and Boolean operations on state sets, starting from a finite number of observable state sets. Any such iteration is guaranteed to terminate in that only a finite number of state sets can be generated. This enables model checking of the μ-calculus.STS2 These are the systems with finite similarity quotients. They can be analyzed symbolically by iterating the predecessor and positive Boolean operations. This enables model checking of the existential and universal fragments of the μ-calculus.STS3 These are the systems with finite trace-equivalence quotients. They can be analyzed symbolically by iterating the predecessor operation and a restricted form of positive Boolean operations (intersection is restricted to intersection with observables). This enables model checking of all ω-regular properties, including linear temporal logic.STS4 These are the systems with finite distance-equivalence quotients (two states are equivalent if for every distance d, the same observables can be reached in d transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new state sets are generated. This enables model checking of the existential conjunction-free and universal disjunction-free fragments of the μ-calculus.STS5 These are the systems with finite bounded-reachability quotients (two states are equivalent if for every distance d, the same observables can be reached in d or fewer transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new states are encountered (this is a weaker termination condition than above). This enables model checking of reachability properties.},
author = {Thomas Henzinger and Majumdar, Ritankar S and Raskin, Jean-François},
journal = {ACM Transactions on Computational Logic (TOCL)},
number = {1},
pages = {1 -- 32},
publisher = {ACM},
title = {{A classification of symbolic transition systems}},
doi = {10.1145/1042038.1042039},
volume = {6},
year = {2005},
}
@inproceedings{4455,
abstract = {We define quantitative similarity functions between timed transition systems that measure the degree of closeness of two systems as a real, in contrast to the traditional boolean yes/no approach to timed simulation and language inclusion. Two systems are close if for each timed trace of one system, there exists a corresponding timed trace in the other system with the same sequence of events and closely corresponding event timings. We show that timed CTL is robust with respect to our quantitative version of bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula. We also define a discounted version of CTL over timed systems, which assigns to every CTL formula a real value that is obtained by discounting real time. We prove the robustness of discounted CTL by establishing that close states in the bisimilarity metric have close values for all discounted CTL formulas.},
author = {Thomas Henzinger and Majumdar, Ritankar S and Prabhu, Vinayak S},
pages = {226 -- 241},
publisher = {Springer},
title = {{Quantifying similarities between timed systems}},
doi = {10.1007/11603009_18},
volume = {3829},
year = {2005},
}
@inproceedings{4456,
abstract = {A modular program analysis considers components independently and provides a succinct summary for each component, which is used when checking the rest of the system. Consider a system consisting of a library and a client. A temporal summary, or interface, of the library specifies legal sequences of library calls. The interface is safe if no call sequence violates the library's internal invariants; the interface is permissive if it contains every such sequence. Modular program analysis requires full interfaces, which are both safe and permissive: the client does not cause errors in the library if and only if it makes only sequences of library calls that are allowed by the full interface of the library.Previous interface-based methods have focused on safe interfaces, which may be too restrictive and thus reject good clients. We present an algorithm for automatically synthesizing software interfaces that are both safe and permissive. The algorithm generates interfaces as graphs whose vertices are labeled with predicates over the library's internal state, and whose edges are labeled with library calls. The interface state is refined incrementally until the full interface is constructed. In other words, the algorithm automatically synthesizes a typestate system for the library, against which any client can be checked for compatibility. We present an implementation of the algorithm which is based on the BLAST model checker, and we evaluate some case studies.},
author = {Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {31 -- 40},
publisher = {ACM},
title = {{Permissive interfaces}},
doi = {10.1145/1081706.1081713},
year = {2005},
}
@inproceedings{4457,
abstract = {We present a compositional approach to the implementation of hard real-time software running on a distributed platform. We explain how several code suppliers, coordinated by a system integrator, can independently generate different parts of the distributed software. The task structure, interaction, and timing is specified as a Giotto program. Each supplier is given a part of the Giotto program and a timing interface, from which the supplier generates task and scheduling code. The integrator then checks, individually for each supplier, in pseudo-polynomial time, if the supplied code meets its timing specification. If all checks succeed, then the supplied software parts are guaranteed to work together and implement the original Giotto program. The feasibility of the approach is demonstrated by a prototype implementation.},
author = {Thomas Henzinger and Kirsch, Christoph M and Matic, Slobodan},
pages = {21 -- 30},
publisher = {ACM},
title = {{Composable code generation for distributed Giotto}},
doi = {10.1145/1065910.1065914},
year = {2005},
}
@inproceedings{4536,
abstract = {We show how to automatically construct and refine rectangular abstractions of systems of linear differential equations. From a hybrid automaton whose dynamics are given by a system of linear differential equations, our method computes automatically a sequence of rectangular hybrid automata that are increasingly precise overapproximations of the original hybrid automaton. We prove an optimality criterion for successive refinements. We also show that this method can take into account a safety property to be verified, refining only relevant parts of the state space. The practicability of the method is illustrated on a benchmark case study. },
author = {Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François},
pages = {144 -- 161},
publisher = {Springer},
title = {{Automatic rectangular refinement of affine hybrid systems}},
doi = {DOI: 10.1007/11603009_13},
volume = {3829},
year = {2005},
}
@inproceedings{4541,
abstract = {Much recent research has focused on the applications of games with ω-regular objectives in the control and verification of reactive systems. However, many of the game-based models are ill-suited for these applications, because they assume that each player has complete information about the state of the system (they are “perfect-information” games). This is because in many situations, a controller does not see the private state of the plant. Such scenarios are naturally modeled by “partial-information” games. On the other hand, these games are intractable; for example, partial-information games with simple reachability objectives are 2EXPTIME-complete.
We study the intermediate case of “semiperfect-information” games, where one player has complete knowledge of the state, while the other player has only partial knowledge. This model is appropriate in control situations where a controller must cope with plant behavior that is as adversarial as possible, i.e., the controller has partial information while the plant has perfect information. As is customary, we assume that the controller and plant take turns to make moves. We show that these semiperfect-information turn-based games are equivalent to perfect-information concurrent games, where the two players choose their moves simultaneously and independently. Since the perfect-information concurrent games are well-understood, we obtain several results of how semiperfect-information turn-based games differ from perfect-information turn-based games on one hand, and from partial-information turn-based games on the other hand. In particular, semiperfect-information turn-based games can benefit from randomized strategies while the perfect-information variety cannot, and semiperfect-information turn-based games are in NP ∩ coNP for all parity objectives.
},
author = {Krishnendu Chatterjee and Thomas Henzinger},
pages = {1 -- 18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Semiperfect-information games}},
doi = {10.1007/11590156_1},
volume = {3821},
year = {2005},
}
@inproceedings{4553,
abstract = {The theory of graph games with ω-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 (almost-sure winning); the quantitative problem asks for the maximal probability of winning (optimal winning) from each state. We show that for Rabin winning conditions, both problems are in NP. As these problems were known to be NP-hard, it follows that they are NP-complete for Rabin conditions, and dually, coNP-complete for Streett conditions. The proof proceeds by showing that pure memoryless strategies suffice for qualitatively and quantitatively winning stochastic graph games with Rabin conditions. This insight is of interest in its own right, as it implies that controllers for Rabin objectives have simple implementations. We also prove that for every ω-regular condition, optimal winning strategies are no more complex than almost-sure winning strategies.},
author = {Krishnendu Chatterjee and de Alfaro, Luca and Thomas Henzinger},
pages = {878 -- 890},
publisher = {Springer},
title = {{The complexity of stochastic Rabin and Streett games}},
doi = {10.1007/11523468_71},
volume = {3580},
year = {2005},
}
@inproceedings{4554,
abstract = {Games played on graphs may have qualitative objectives, such as the satisfaction of an ω-regular property, or quantitative objectives, such as the optimization of a real-valued reward. When games are used to model reactive systems with both fairness assumptions and quantitative (e.g., resource) constraints, then the corresponding objective combines both a qualitative and a quantitative component. In a general case of interest, the qualitative component is a parity condition and the quantitative component is a mean-payoff reward. We study and solve such mean-payoff parity games. We also prove some interesting facts about mean-payoff parity games which distinguish them both from mean-payoff and from parity games. In particular, we show that optimal strategies exist in mean-payoff parity games, but they may require infinite memory.},
author = {Krishnendu Chatterjee and Thomas Henzinger and Jurdziński, Marcin},
pages = {178 -- 187},
publisher = {IEEE},
title = {{Mean-payoff parity games}},
doi = {10.1109/LICS.2005.26},
year = {2005},
}
@inproceedings{4557,
abstract = {Planning in adversarial and uncertain environments can be modeled as the problem of devising strategies in stochastic perfect information games. These games are generalizations of Markov decision processes (MDPs): there are two (adversarial) players, and a source of randomness. The main practical obstacle to computing winning strategies in such games is the size of the state space. In practice therefore, one typically works with abstractions of the model. The diffculty is to come up with an abstraction that is neither too coarse to remove all winning strategies (plans), nor too fine to be intractable. In verification, the paradigm of counterexample-guided abstraction refinement has been successful to construct useful but parsimonious abstractions automatically. We extend this paradigm to probabilistic models (namely, perfect information games and, as a special case, MDPs). This allows us to apply the counterexample-guided abstraction paradigm to the AI planning problem. As special cases, we get planning algorithms for MDPs and deterministic systems that automatically construct system abstractions.},
author = {Krishnendu Chatterjee and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {104 -- 111},
publisher = {AUAI Press},
title = {{Counterexample-guided planning}},
year = {2005},
}
@inproceedings{4560,
abstract = {We define and study a quantitative generalization of the traditional boolean framework of model-based specification and verification. In our setting, propositions have integer values at states, and properties have integer values on traces. For example, the value of a quantitative proposition at a state may represent power consumed at the state, and the value of a quantitative property on a trace may represent energy used along the trace. The value of a quantitative property at a state, then, is the maximum (or minimum) value achievable over all possible traces from the state. In this framework, model checking can be used to compute, for example, the minimum battery capacity necessary for achieving a given objective, or the maximal achievable lifetime of a system with a given initial battery capacity. In the case of open systems, these problems require the solution of games with integer values.
Quantitative model checking and game solving is undecidable, except if bounds on the computation can be found. Indeed, many interesting quantitative properties, like minimal necessary battery capacity and maximal achievable lifetime, can be naturally specified by quantitative-bound automata, which are finite automata with integer registers whose analysis is constrained by a bound function f that maps each system K to an integer f(K). Along with the linear-time, automaton-based view of quantitative verification, we present a corresponding branching-time view based on a quantitative-bound μ-calculus, and we study the relationship, expressive power, and complexity of both views.
},
author = {Chakrabarti, Arindam and Krishnendu Chatterjee and Thomas Henzinger and Kupferman, Orna and Majumdar, Ritankar S},
pages = {50 -- 64},
publisher = {Springer},
title = {{Verifying quantitative properties using bound functions}},
doi = {10.1007/11560548_7},
volume = {3725},
year = {2005},
}
@inproceedings{4576,
abstract = {We present a language for specifying web service interfaces. A web service interface puts three kinds of constraints on the users of the service. First, the interface specifies the methods that can be called by a client, together with types of input and output parameters; these are called signature constraints. Second, the interface may specify propositional constraints on method calls and output values that may oc- cur in a web service conversation; these are called consis- tency constraints. Third, the interface may specify temporal constraints on the ordering of method calls; these are called protocol constraints. The interfaces can be used to check, first, if two or more web services are compatible, and second, if a web service A can be safely substituted for a web ser- vice B. The algorithm for compatibility checking verifies that two or more interfaces fulfill each others’ constraints. The algorithm for substitutivity checking verifies that service A demands fewer and fulfills more constraints than service B.},
author = {Beyer, Dirk and Chakrabarti, Arindam and Thomas Henzinger},
pages = {148 -- 159},
publisher = {ACM},
title = {{Web service interfaces}},
doi = {10.1145/1060745.1060770},
year = {2005},
}
@inproceedings{4579,
abstract = {BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how BLAST can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use Ccured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that BLAST can remove many of the run-time checks added by Ccured and provide useful information to the programmer about many of the remaining checks.},
author = {Beyer, Dirk and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {2 -- 18},
publisher = {Springer},
title = {{Checking memory safety with BLAST}},
doi = {10.1007/978-3-540-31984-9_2},
volume = {3442},
year = {2005},
}
@inproceedings{4624,
abstract = {Surveying results from [5] and [6], we motivate and introduce the theory behind formalizing rich interfaces for software and hardware components. Rich interfaces specify the protocol aspects of component interaction. Their formalization, called interface automata, permits a compiler to check the compatibility of component interaction protocols. Interface automata support incremental design and independent implementability. Incremental design means that the compatibility checking of interfaces can proceed for partial system descriptions, without knowing the interfaces of all components. Independent implementability means that compatible interfaces can be refined separately, while still maintaining compatibility.},
author = {de Alfaro, Luca and Thomas Henzinger},
pages = {83 -- 104},
publisher = {Springer},
title = {{Interface-based design}},
doi = {10.1007/1-4020-3532-2_3},
volume = {195},
year = {2005},
}