@inproceedings{3700, abstract = {We propose a new method to partition an unlabeled dataset, called Discriminative Context Partitioning (DCP). It is motivated by the idea of splitting the dataset based only on how well the resulting parts can be separated from a context class of disjoint data points. This is in contrast to typical clustering techniques like K-means that are based on a generative model by implicitly or explicitly searching for modes in the distribution of samples. The discriminative criterion in DCP avoids the problems that density based methods have when the a priori assumption of multimodality is violated, when the number of samples becomes small in relation to the dimensionality of the feature space, or if the cluster sizes are strongly unbalanced. We formulate DCP‘s separation property as a large-margin criterion, and show how the resulting optimization problem can be solved efficiently. Experiments on the MNIST and USPS datasets of handwritten digits and on a subset of the Caltech256 dataset show that, given a suitable context, DCP can achieve good results even in situation where density-based clustering techniques fail.}, author = {Christoph Lampert}, pages = {1 -- 8}, publisher = {IEEE}, title = {{Partitioning of image datasets using discriminative context information}}, doi = {10.1109/CVPR.2008.4587448}, year = {2008}, } @inproceedings{3716, abstract = {Most current methods for multi-class object classification and localization work as independent 1-vs-rest classifiers. They decide whether and where an object is visible in an image purely on a per-class basis. Joint learning of more than one object class would generally be preferable, since this would allow the use of contextual information such as co-occurrence between classes. However, this approach is usually not employed because of its computational cost. In this paper we propose a method to combine the efficiency of single class localization with a subsequent decision process that works jointly for all given object classes. By following a multiple kernel learning (MKL) approach, we automatically obtain a sparse dependency graph of relevant object classes on which to base the decision. Experiments on the PASCAL VOC 2006 and 2007 datasets show that the subsequent joint decision step clearly improves the accuracy compared to single class detection. }, author = {Christoph Lampert and Blaschko,Matthew B}, pages = {31 -- 40}, publisher = {Springer}, title = {{A multiple kernel learning approach to joint multi-class object detection}}, doi = {10.1007/978-3-540-69321-5_4}, volume = {5096}, year = {2008}, } @inproceedings{3714, abstract = {Most successful object recognition systems rely on binary classification, deciding only if an object is present or not, but not providing information on the actual object location. To perform localization, one can take a sliding window approach, but this strongly increases the computational cost, because the classifier function has to be evaluated over a large set of candidate subwindows. In this paper, we propose a simple yet powerful branchand- bound scheme that allows efficient maximization of a large class of classifier functions over all possible subimages. It converges to a globally optimal solution typically in sublinear time. We show how our method is applicable to different object detection and retrieval scenarios. The achieved speedup allows the use of classifiers for localization that formerly were considered too slow for this task, such as SVMs with a spatial pyramid kernel or nearest neighbor classifiers based on the 2-distance. We demonstrate state-of-the-art performance of the resulting systems on the UIUC Cars dataset, the PASCAL VOC 2006 dataset and in the PASCAL VOC 2007 competition.}, author = {Christoph Lampert and Blaschko,Matthew B and Hofmann,Thomas}, pages = {1 -- 8}, publisher = {IEEE}, title = {{Beyond sliding windows: Object localization by efficient subwindow search}}, doi = {10.1109/CVPR.2008.4587586}, year = {2008}, } @article{3734, abstract = {Gene expression levels fluctuate even under constant external conditions. Much emphasis has usually been placed on the components of this noise that are due to randomness in transcription and translation. Here we focus on the role of noise associated with the inputs to transcriptional regulation; in particular, we analyze the effects of random arrival times and binding of transcription factors to their target sites along the genome. This contribution to the total noise sets a fundamental physical limit to the reliability of genetic control, and has clear signatures, but we show that these are easily obscured by experimental limitations and even by conventional methods for plotting the variance vs. mean expression level. We argue that simple, universal models of noise dominated by transcription and translation are inconsistent with the embedding of gene expression in a network of regulatory interactions. Analysis of recent experiments on transcriptional control in the early Drosophila embryo shows that these results are quantitatively consistent with the predicted signatures of input noise, and we discuss the experiments needed to test the importance of input noise more generally.}, author = {Gasper Tkacik and Gregor, Thomas and Bialek, William S}, journal = {PLoS One}, number = {7}, publisher = {Public Library of Science}, title = {{The role of input noise in transcriptional regulation}}, doi = {10.1371/journal.pone.0002774}, volume = {3}, year = {2008}, } @article{3751, abstract = {Revealing the spectrum of combinatorial regulation of transcription at individual promoters is essential for understanding the complex structure of biological networks. However, the computations represented by the integration of various molecular signals at complex promoters are difficult to decipher in the absence of simple cis regulatory codes. Here we synthetically shuffle the regulatory architecture-operator sequences binding activators and repressors-of a canonical bacterial promoter. The resulting library of complex promoters allows for rapid exploration of promoter encoded logic regulation. Among all possible logic functions, NOR and ANDN promoter encoded logics predominate. A simple transcriptional cis regulatory code determines both logics, establishing a straightforward map between promoter structure and logic phenotype. The regulatory code is determined solely by the type of transcriptional regulation combinations: two repressors generate a NOR: NOT (a OR b) whereas a repressor and an activator generate an ANDN: a AND NOT b. Three-input versions of both logics, having an additional repressor as an input, are also present in the library. The resulting complex promoters cover a wide dynamic range of transcriptional strengths. Synthetic promoter shuffling represents a fast and efficient method for exploring the spectrum of complex regulatory functions that can be encoded by complex promoters. From an engineering point of view, synthetic promoter shuffling enables the experimental testing of the functional properties of complex promoters that cannot necessarily be inferred ab initio from the known properties of the individual genetic components. Synthetic promoter shuffling may provide a useful experimental tool for studying naturally occurring promoter shuffling.}, author = {Kinkhabwala, Ali and Guet, Calin C}, journal = {PLoS One}, number = {4}, publisher = {Public Library of Science}, title = {{Uncovering cis regulatory codes using synthetic promoter shuffling}}, doi = {10.1371/journal.pone.0002030}, volume = {3}, year = {2008}, } @article{3754, abstract = {Fluorescence correlation spectroscopy (FCS) has permitted the characterization of high concentrations of noncoding RNAs in a single living bacterium. Here, we extend the use of FCS to low concentrations of coding RNAs in single living cells. We genetically fuse a red fluorescent protein (RFP) gene and two binding sites for an RNA-binding protein, whose translated product is the RFP protein alone. Using this construct, we determine in single cells both the absolute [mRNA] concentration and the associated [RFP] expressed from an inducible plasmid. We find that the FCS method allows us to reliably monitor in real-time [mRNA] down to similar to 40 nM (i.e. approximately two transcripts per volume of detection). To validate these measurements, we show that [mRNA] is proportional to the associated expression of the RFP protein. This FCS-based technique establishes a framework for minimally invasive measurements of mRNA concentration in individual living bacteria.}, author = {Calin Guet and Bruneaux,Luke and Min,Taejin L and Siegal-Gaskins,Dan and Figueroa,Israel and Emonet,Thierry and Cluzel,Philippe}, journal = {Nucleic Acids Research}, number = {12}, publisher = {Oxford University Press}, title = {{Minimally invasive determination of mRNA concentration in single living bacteria}}, doi = {10.1093/nar/gkn329}, volume = {36}, year = {2008}, } @article{3769, abstract = {The geometrical representation of the space of phylogenetic trees implies a metric on the space of weighted trees. This metric, the geodesic distance, is the length of the shortest path through that space. We present an exact algorithm to compute this metric. For biologically reasonable trees, the implementation allows fast computations of the geodesic distance, although the running time of the algorithm is worst-case exponential. The algorithm was applied to pairs of 118 gene trees of the metazoa. The results show that a special path in tree space, the cone path, which can be computed in linear time, is a good approximation of the geodesic distance. The program GeoMeTree is a python implementation of the geodesic distance, and it is approximations and is available from www.cibiv.at/software/geometree.}, author = {Anne Kupczok and von Haeseler,Arndt and Klaere,Steffen}, journal = {Journal of Computational Biology}, number = {6}, pages = {577 -- 591}, publisher = {Mary Ann Liebert}, title = {{An Exact Algorithm for the Geodesic Distance between Phylogenetic Trees.}}, doi = {4200}, volume = {15}, year = {2008}, } @article{3826, abstract = {Gamma frequency (30-100 Hz) oscillations in the mature cortex underlie higher cognitive functions. Fast signaling in GABAergic interneuron networks plays a key role in the generation of these oscillations. During development of the rodent brain, gamma activity appears at the end of the first postnatal week, but frequency and synchrony reach adult levels only by the fourth week. However, the mechanisms underlying the maturation of gamma activity are unclear. Here we demonstrate that hippocampal basket cells (BCs), the proposed cellular substrate of gamma oscillations, undergo marked changes in their morphological, intrinsic, and synaptic properties between postnatal day 6 (P6) and P25. During maturation, action potential duration, propagation time, duration of the release period, and decay time constant of IPSCs decreases by approximately 30-60%. Thus, postnatal development converts BCs from slow into fast signaling devices. Computational analysis reveals that BC networks with young intrinsic and synaptic properties as well as reduced connectivity generate oscillations with moderate coherence in the lower gamma frequency range. In contrast, BC networks with mature properties and increased connectivity generate highly coherent activity in the upper gamma frequency band. Thus, late postnatal maturation of BCs enhances coherence in neuronal networks and will thereby contribute to the development of cognitive brain functions.}, author = {Doischer, Daniel and Hosp, Jonas Aurel and Yanagawa, Yuchio and Obata, Kunihiko and Peter Jonas and Vida, Imre and Bartos, Marlene}, journal = {Journal of Neuroscience}, number = {48}, pages = {12956 -- 68}, publisher = {Society for Neuroscience}, title = {{Postnatal differentiation of basket cells from slow to fast signaling devices}}, doi = {10.1523/JNEUROSCI.2890-08.2008}, volume = {28}, year = {2008}, } @article{3827, abstract = {Previous studies revealed that synaptotagmin 1 is the major Ca(2+) sensor for fast synchronous transmitter release at excitatory synapses. However, the molecular identity of the Ca(2+) sensor at hippocampal inhibitory synapses has not been determined. To address the functional role of synaptotagmin 1 at identified inhibitory terminals, we made paired recordings from synaptically connected basket cells (BCs) and granule cells (GCs) in the dentate gyrus in organotypic slice cultures from wild-type and synaptotagmin 1-deficient mice. As expected, genetic elimination of synaptotagmin 1 abolished synchronous transmitter release at excitatory GC-BC synapses. However, synchronous release at inhibitory BC-GC synapses was maintained. Quantitative analysis revealed that elimination of synaptotagmin 1 reduced release probability and depression but maintained the synchrony of transmitter release at BC-GC synapses. Elimination of synaptotagmin 1 also increased the frequency of both miniature excitatory postsynaptic currents (measured in BCs) and miniature inhibitory postsynaptic currents (recorded in GCs), consistent with a clamping function of synaptotagmin 1 at both excitatory and inhibitory terminals. Single-cell reverse-transcription quantitative PCR analysis revealed that single BCs coexpressed multiple synaptotagmin isoforms, including synaptotagmin 1-5, 7, and 11-13. Our results indicate that, in contrast to excitatory synapses, synaptotagmin 1 is not absolutely required for synchronous release at inhibitory BC-GC synapses. Thus, alternative fast Ca(2+) sensors contribute to synchronous release of the inhibitory transmitter GABA in cortical circuits.}, author = {Kerr, Angharad M and Reisinger, Ellen and Peter Jonas}, journal = {PNAS}, number = {40}, pages = {15581 -- 6}, publisher = {National Academy of Sciences}, title = {{Differential dependence of phasic transmitter release on synaptotagmin 1 at GABAergic and glutamatergic hippocampal synapses}}, doi = {10.1073/pnas.0800621105}, volume = {105}, year = {2008}, } @inproceedings{3504, abstract = {Simulation and bisimulation metrics for stochastic systems provide a quantitative gen- eralization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative μ-calculus and related probabilistic logics. We present algorithms for computing the metrics on Markov decision processes (MDPs), turn- based stochastic games, and concurrent games. For turn-based games and MDPs, we provide a polynomial-time algorithm based on linear programming for the computation of the one-step metric distance between states. The algorithm improves on the previously known exponential-time algo- rithm based on a reduction to the theory of reals. We then present PSPACE algorithms for both the decision problem and the problem of approximating the metric distance between two states, matching the best known bound for Markov chains. For the bisimulation kernel of the metric, which corresponds to probabilistic bisimulation, our algorithm works in time O(n4) for both turn-based games and MDPs; improving the previously best known O(n9 · log(n)) time algorithm for MDPs. For a concurrent game G, we show that computing the exact distance between states is at least as hard as computing the value of concurrent reachability games and the square-root-sum problem in computational geometry. We show that checking whether the metric distance is bounded by a rational r, can be accomplished via a reduction to the theory of real closed fields, involving a formula with three quantifier alternations, yielding O(|G|O(|G|5)) time complexity, improving the previously known reduction with O(|G|O(|G|7)) time complexity. These algorithms can be iterated to approximate the metrics using binary search.}, author = {Chatterjee, Krishnendu and De Alfaro, Luca and Majumdar, Ritankar and Raman, Vishwanath}, pages = {107 -- 118}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Algorithms for game metrics}}, doi = {10.4230/LIPIcs.FSTTCS.2008.1745}, volume = {2}, year = {2008}, } @inproceedings{3875, abstract = {We study the problem of model checking Interval-valued Discrete-time Markov Chains (IDTMC). IDTMCs are discrete-time finite Markov Chains for which the exact transition probabilities are riot known. Instead in IDTMCs, each transition is associated with an interval in which the actual transition probability must lie. We consider two semantic interpretations for the uncertainty in the transition probabilities of an IDTMC. In the first interpretation, we think of an IDTMC as representing a (possibly uncountable) family of (classical) discrete-time Markov Chains, where each member of the family is a Markov Chain whose transition probabilities lie within the interval range given in the IDTMC. We call this semantic interpretation Uncertain Markov Chains (UMC). In the second semantics for an IDTMC, which we call Interval Markov Decision Process (IMDP), we view the uncertainty as being resolved through non-determinism. In other words, each time a state is visited, we adversarially pick a transition distribution that respects the interval constraints, and take a probabilistic step according to the chosen distribution. We introduce a logic omega-PCTL that can express liveness, strong fairness, and omega-regular properties (such properties cannot be expressed in PCTL). We show that the omega-PCTL model checking problem for Uncertain Markov Chain semantics is decidable in PSPACE (same as the best known upper bound for PCTL) and for Interval Markov Decision Process semantics is decidable in coNP (improving the previous known PSPACE bound for PCTL). We also show that the qualitative fragment of the logic can lie solved in coNP for the UMC interpretation, and can be solved in polynomial time for a sub-class of UMCs. We also prove lower bounds for these model checking problems. We show that the model checking problem of IDTMCs with LTL formulas can be solved for both UMC and IMDP semantics by reduction to the model checking problem of IDTMC with omega-PcTL formulas.}, author = {Krishnendu Chatterjee and Thomas Henzinger and Sen, Koushik}, pages = {302 -- 317}, publisher = {Springer}, title = {{Model-checking omega-regular properties of interval Markov chains}}, doi = {10.1007/978-3-540-78499-9_22}, volume = {4962}, year = {2008}, } @inproceedings{3873, abstract = {We study the controller synthesis problem under budget constraints. In this problem, there is a cost associated with making an observation, and a controller can make only a limited number of observations in each round so that the total cost of the observations does not exceed a given fixed budget. The controller must ensure some omega-regular requirement subject to the budget constraint. Budget constraints arise in designing and implementing controllers for resource-constrained embedded systems, where a controller may not have enough power, time, or bandwidth to obtain data from all sensors in each round. They lead to games of imperfect information, where the unknown information is not fixed a priori, but can vary from round to round, based on the choices made by the controller how to allocate its budget. We show that the budget-constrained synthesis problem for W-regular objectives is complete for exponential time. In addition to studying synthesis under a fixed budget constraint, we study the budget optimization problem, where given a plant, an objective, and observation costs, we have to find a controller that achieves the objective with minimal average accumulated cost (or minimal peak cost). We show that this problem is reducible to a game of imperfect information where the winning objective is a conjunction of an omega-regular condition and a long-run average condition (or a least max-cost condition), and this again leads to an exponential-time algorithm. Finally, we extend our results to games over infinite state spaces, and show that the budget-constrained synthesis problem is decidable for infinite state games with stable quotients of finite index. Consequently, the discrete time budget-constrained synthesis problem is decidable for rectangular hybrid automata.}, author = {Krishnendu Chatterjee and Majumdar, Ritankar S and Thomas Henzinger}, pages = {72 -- 86}, publisher = {Springer}, title = {{Controller synthesis with budget constraints}}, doi = {DOI: 10.1007/978-3-540-78929-1_6}, volume = {4981}, year = {2008}, } @inproceedings{3876, abstract = {We consider two-player games played in real time on game structures with clocks and parity objectives. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to turn-based (i.e., nonconcurrent) finite-state (i.e., untimed) parity games. The states of the resulting game are pairs of clock regions of the original game. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust strategies. Using a limit-robust strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers.}, author = {Krishnendu Chatterjee and Thomas Henzinger and Prabhu, Vinayak S}, pages = {124 -- 140}, publisher = {Springer}, title = {{Timed parity games: complexity and robustness}}, doi = {10.1007/978-3-540-85778-5_10}, volume = {5215}, year = {2008}, } @inproceedings{3877, abstract = {The synthesis problem asks to construct a reactive finite-state system from an omega-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. A common reason for unrealizability is that assumptions on the environment of the system are incomplete. We study the problem of correcting an unrealizable specification phi by computing an environment assumption psi such that the new specification psi -> phi is realizable. Our aim is to construct an assumption psi that constrains only the environment and is as weak as possible. We present a two-step algorithm for computing assumptions. The algorithm operates on the game graph that is used to answer the realizability question. First, we compute a safety assumption that removes a minimal set of environment edges from the graph. Second, we compute a liveness assumption that puts fairness conditions on some of the remaining environment edges. We show that the problem of finding a minimal set of fair edges is computationally hard, and we use probabilistic games to compute a locally minimal fairness assumption.}, author = {Krishnendu Chatterjee and Thomas Henzinger and Jobstmann, Barbara}, pages = {147 -- 161}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Environment assumptions for synthesis}}, doi = {10.1007/978-3-540-85361-9_14}, volume = {5201}, year = {2008}, } @inproceedings{3878, abstract = {We study the problem of generating a test sequence that achieves maximal coverage for a reactive system under test. We formulate the problem as a repeated game between the tester and the system, where the system state space is partitioned according to some coverage criterion and the objective of the tester is to maximize the set of partitions (or coverage goals) visited during the game. We show the complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete, but is NP-complete for deterministic systems. For the special case of non-deterministic systems with a re-initializing “reset” action, which represent running a new test input on a re-initialized system, we show that the complexity is coNP-complete. Our proof technique for reset games uses randomized testing strategies that circumvent the exponentially large memory requirement of deterministic testing strategies.}, author = {Krishnendu Chatterjee and de Alfaro, Luca and Majumdar, Ritankar S}, pages = {91 -- 106}, publisher = {Springer}, title = {{The complexity of coverage}}, doi = {10.1007/978-3-540-89330-1_7}, volume = {5356}, year = {2008}, } @inproceedings{3874, abstract = {We consider concurrent two-player timed automaton games with omega-regular objectives specified as parity conditions. These games offer an appropriate model for the synthesis of real-time controllers. Earlier works on timed games focused on pure strategies for each player. We study, for the first time, the use of randomized strategies in such games. While pure (i.e., nonrandomized) strategies in timed games require infinite memory for winning even with respect to reachability objectives, we show that randomized strategies can win with finite memory with respect to all parity objectives. Also, the synthesized randomized real-time controllers are much simpler in structure than the corresponding pure controllers, and therefore easier to implement. For safety objectives we prove the existence of pure finite-memory winning strategies. Finally, while randomization helps in simplifying the strategies required for winning timed parity games, we prove that randomization does not help in winning at more states.}, author = {Krishnendu Chatterjee and Thomas Henzinger and Prabhu, Vinayak S}, pages = {87 -- 100}, publisher = {Springer}, title = {{Trading infinite memory for uniform randomness in timed games}}, doi = {10.1007/978-3-540-78929-1_7}, volume = {4981}, year = {2008}, } @inproceedings{3879, abstract = {Quantitative generalizations of classical languages, which assign to each word a real number instead of a boolean value, have applications in modeling resource-constrained computation. We use weighted automata (finite automata with transition weights) to define several natural classes of quantitative languages over finite and infinite words; in particular, the real value of an infinite run is computed as the maximum, limsup, liminf, limit average, or discounted sum of the transition weights. We define the classical decision problems of automata theory (emptiness, universality, language inclusion, and language equivalence) in the quantitative setting and study their computational complexity. As the decidability of language inclusion remains open for some classes of weighted automata, we introduce a notion of quantitative simulation that is decidable and implies language inclusion. We also give a complete characterization of the expressive power of the various classes of weighted automata. In particular, we show that most classes of weighted automata cannot be determinized.}, author = {Krishnendu Chatterjee and Doyen, Laurent and Thomas Henzinger}, pages = {385 -- 400}, publisher = {Springer}, title = {{Quantitative languages}}, doi = {10.1007/978-3-540-87531-4_28}, volume = {5213}, year = {2008}, } @inbook{3872, abstract = {We survey value iteration algorithms on graphs. Such algorithms can be used for determining the existence of certain paths (model checking), the existence of certain strategies (game solving), and the probabilities of certain events (performance analysis). We classify the algorithms according to the value domain (boolean, probabilistic, or quantitative); according to the graph structure (nondeterministic, probabilistic, or multi-player); according to the desired property of paths (Borel level 1, 2, or 3); and according to the alternation depth and convergence rate of fixpoint computations.}, author = {Krishnendu Chatterjee and Thomas Henzinger}, booktitle = {25 Years in Model Checking}, pages = {107 -- 138}, publisher = {Springer}, title = {{Value iteration}}, doi = {10.1007/978-3-540-69850-0_7}, volume = {5000}, year = {2008}, } @article{3945, abstract = {Langerhans cells and dermal dendritic cells migrate to the draining lymph nodes through dermal lymphatic vessels. They do so in the steady-state and under inflammatory conditions. Peripheral T cell tolerance or T cell priming, respectively, are the consequences of migration. The nature of dendritic cell-containing vessels was mostly defined by electron microscopy or by their lack of blood endothelial markers. Selective markers for murine lymph endothelium were hitherto rare or not available. Here, we utilised recently developed antibodies against the murine hyaluronan receptor, LYVE-1, to study the lymph vessel network in mouse skin in more detail. In hairless skin from the ears, lymph vessels were spread out in a horizontal plane. They formed anastomoses, and they possessed frequent blind endings that were occasionally open. Lymph vessels were wider than blood vessels, which were identified by their strong CD31 expression. In body wall skin LYVE-1 reactive vessels did not extend laterally but they dived straight down into the deeper dermis. There, they are connected to each other and formed a network similar to ear skin. The number and width of lymph vessels did not grossly change upon inflammatory stimuli such as skin explant culture or tape stripping. There were also no marked changes in caliber in response to the TLR 7/8 ligand Imiquimod. Double-labelling experiments of cultured skin showed that most of the strongly cell surface MHC II-expressing (i.e. activated) dendritic cells were confined to the lymph vessels. Langerin/CD207(+) cells within this population appeared later than dermal dendritic cells, i.e. langerin-negative cells. Comparable results were obtained after stimulating the skin in vivo with the TLR 7/8 ligand Imiquimod or by tape stripping. In untreated skin (i.e. steady state) a few MHC II(+) and Langerin/CD207(+) cells, presumably migrating skin dendritic cells including epidermal Langerhans cells, were consistently observed within the lymph vessels. The novel antibody reagents may serve as important tools to further study the dendritic cell traffic in the skin under physiological conditions as well as in conditions of adoptive dendritic cell transfer in immunotherapy.}, author = {Tripp, Christoph H and Haid, Bernhard and Flacher, Vincent and Michael Sixt and Peter, Hannes and Farkas, Julia and Gschwentner, Robert and Sorokin, Lydia and Romani, Nikolaus and Stoitzner, Patrizia}, journal = {Immunobiology}, number = {9-10}, pages = {715 -- 28}, publisher = {Elsevier}, title = {{The lymph vessel network in mouse skin visualised with antibodies against the hyaluronan receptor LYVE-1}}, doi = {10.1016/j.imbio.2008.07.025}, volume = {213}, year = {2008}, } @article{3942, abstract = {Recent in vitro studies have suggested a role for sialylation in chemokine receptor binding to its ligand (Bannert, N., S. Craig, M. Farzan, D. Sogah, N.V. Santo, H. Choe, and J. Sodroski. 2001. J. Exp. Med. 194:1661-1673). This prompted us to investigate chemokine-induced leukocyte adhesion in inflamed cremaster muscle venules of alpha2,3 sialyltransferase (ST3Gal-IV)-deficient mice. We found a marked reduction in leukocyte adhesion to inflamed microvessels upon injection of the CXCR2 ligands CXCL1 (keratinocyte-derived chemokine) or CXCL8 (interleukin 8). In addition, extravasation of ST3Gal-IV(-/-) neutrophils into thioglycollate-pretreated peritoneal cavities was significantly decreased. In vitro assays revealed that CXCL8 binding to isolated ST3Gal-IV(-/-) neutrophils was markedly impaired. Furthermore, CXCL1-mediated adhesion of ST3Gal-IV(-/-) leukocytes at physiological flow conditions, as well as transendothelial migration of ST3Gal-IV(-/-) leukocytes in response to CXCL1, was significantly reduced. In human neutrophils, enzymatic desialylation decreased binding of CXCR2 ligands to the neutrophil surface and diminished neutrophil degranulation in response to these chemokines. In addition, binding of alpha2,3-linked sialic acid-specific Maackia amurensis lectin II to purified CXCR2 from neuraminidase-treated CXCR2-transfected HEK293 cells was markedly impaired. Collectively, we provide substantial evidence that sialylation by ST3Gal-IV significantly contributes to CXCR2-mediated leukocyte adhesion during inflammation in vivo.}, author = {Frommhold, David and Ludwig, Andreas and Bixel, M Gabriele and Zarbock, Alexander and Babushkina, Inna and Weissinger, Melitta and Cauwenberghs, Sandra and Ellies, Lesley G and Marth, Jamey D and Beck-Sickinger, Annette G and Michael Sixt and Lange-Sperandio, Bärbel and Zernecke, Alma and Brandt, Ernst and Weber, Christian and Vestweber, Dietmar and Ley, Klaus and Sperandio, Markus}, journal = {The Journal of Experimental Medicine}, number = {6}, pages = {1435 -- 1446}, publisher = {Rockefeller University Press}, title = {{Sialyltransferase ST3Gal-IV controls CXCR2-mediated firm leukocyte arrest during inflammation}}, doi = {10.1084/jem.20070846}, volume = {205}, year = {2008}, } @article{3943, abstract = {Neutrophil granulocytes form the body's first line of antibacterial defense, but they also contribute to tissue injury and noninfectious, chronic inflammation. Proteinase 3 (PR3) and neutrophil elastase (NE) are 2 abundant neutrophil serine proteases implicated in antimicrobial defense with overlapping and potentially redundant substrate specificity. Here, we unraveled a cooperative role for PR3 and NE in neutrophil activation and noninfectious inflammation in vivo, which we believe to be novel. Mice lacking both PR3 and NE demonstrated strongly diminished immune complex-mediated (IC-mediated) neutrophil infiltration in vivo as well as reduced activation of isolated neutrophils by ICs in vitro. In contrast, in mice lacking just NE, neutrophil recruitment to ICs was only marginally impaired. The defects in mice lacking both PR3 and NE were directly linked to the accumulation of antiinflammatory progranulin (PGRN). Both PR3 and NE cleaved PGRN in vitro and during neutrophil activation and inflammation in vivo. Local administration of recombinant PGRN potently inhibited neutrophilic inflammation in vivo, demonstrating that PGRN represents a crucial inflammation-suppressing mediator. We conclude that PR3 and NE enhance neutrophil-dependent inflammation by eliminating the local antiinflammatory activity of PGRN. Our results support the use of serine protease inhibitors as antiinflammatory agents.}, author = {Kessenbrock, Kai and Fröhlich, Leopold and Michael Sixt and Lämmermann, Tim and Pfister, Heiko and Bateman, Andrew and Belaaouaj, Azzaq and Ring, Johannes and Ollert, Markus and Fässler, Reinhard and Jenne, Dieter E}, journal = {The Journal of Clinical Investigation}, number = {7}, pages = {2438 -- 2447}, publisher = {American Society for Clinical Investigation}, title = {{Proteinase 3 and neutrophil elastase enhance inflammation in mice by inactivating antiinflammatory progranulin}}, doi = {10.1172/JCI34694}, volume = {118}, year = {2008}, } @article{3941, abstract = {All metazoan cells carry transmembrane receptors of the integrin family, which couple the contractile force of the actomyosin cytoskeleton to the extracellular environment. In agreement with this principle, rapidly migrating leukocytes use integrin-mediated adhesion when moving over two-dimensional surfaces. As migration on two-dimensional substrates naturally overemphasizes the role of adhesion, the contribution of integrins during three-dimensional movement of leukocytes within tissues has remained controversial. We studied the interplay between adhesive, contractile and protrusive forces during interstitial leukocyte chemotaxis in vivo and in vitro. We ablated all integrin heterodimers from murine leukocytes, and show here that functional integrins do not contribute to migration in three-dimensional environments. Instead, these cells migrate by the sole force of actin-network expansion, which promotes protrusive flowing of the leading edge. Myosin II-dependent contraction is only required on passage through narrow gaps, where a squeezing contraction of the trailing edge propels the rigid nucleus.}, author = {Lämmermann, Tim and Bader, Bernhard L and Monkley, Susan J and Worbs, Tim and Wedlich-Söldner, Roland and Hirsch, Karin and Keller, Markus and Förster, Reinhold and Critchley, David R and Fässler, Reinhard and Michael Sixt}, journal = {Nature}, number = {7191}, pages = {51 -- 55}, publisher = {Nature Publishing Group}, title = {{Rapid leukocyte migration by integrin-independent flowing and squeezing}}, doi = {10.1038/nature06887}, volume = {453}, year = {2008}, } @article{3944, abstract = {Live imaging of the actin cytoskeleton is crucial for the study of many fundamental biological processes, but current approaches to visualize actin have several limitations. Here we describe Lifeact, a 17-amino-acid peptide, which stained filamentous actin (F-actin) structures in eukaryotic cells and tissues. Lifeact did not interfere with actin dynamics in vitro and in vivo and in its chemically modified peptide form allowed visualization of actin dynamics in nontransfectable cells.}, author = {Riedl, Julia and Crevenna, Alvaro H and Kessenbrock, Kai and Yu, Jerry Haochen and Neukirchen, Dorothee and Bista, Michal and Bradke, Frank and Jenne, Dieter and Holak, Tad A and Werb, Zena and Michael Sixt and Wedlich-Soldner, Roland}, journal = {Nature Methods}, number = {7}, pages = {605 -- 607}, publisher = {Nature Publishing Group}, title = {{Lifeact: a versatile marker to visualize F-actin}}, doi = {10.1038/nmeth.1220}, volume = {5}, year = {2008}, } @inproceedings{3974, abstract = {Generalizing the concept of a Reeb graph, the Reeb space of a multivariate continuous mapping identifies points of the domain that belong to a common component of the preimage of a point in the range. We study the local and global structure of this space for generic, piecewise linear mappings on a combinatorial manifold.}, author = {Herbert Edelsbrunner and Harer, John and Amit Patel}, pages = {242 -- 250}, publisher = {ACM}, title = {{Reeb spaces of piecewise linear mappings}}, doi = {10.1145/1377676.1377720}, year = {2008}, } @article{4135, author = {Storch,D. and Šizling,A. L and Reif,J. and Jitka Polechova and Šizlingová,E. and Gaston,K. J}, journal = {Ecology Letters}, number = {8}, pages = {771 -- 784}, publisher = {Wiley-Blackwell}, title = {{The quest for a null model for macroecological patterns: geometry of species distributions at multiple spatial scales}}, doi = {3817}, volume = {11}, year = {2008}, } @inbook{4137, author = {Bridle, Jon R and Jitka Polechova and Vines, Timothy H}, booktitle = {Evolution and Speciation}, editor = {R. K. Butlin,J.R. Bridle and Schluter,D.}, pages = {77 -- 101}, publisher = {Cambridge University Press}, title = {{Patterns of biodiversity and limits to adaptation in time and space}}, doi = {3816}, year = {2008}, } @article{4150, abstract = {This study provides direct functional evidence that differential adhesion, measurable as quantitative differences in tissue surface tension, influences spatial positioning between zebrafish germ layer tissues. We show that embryonic ectodermal and mesendodermal tissues generated by mRNA-overexpression behave on long-time scales like immiscible fluids. When mixed in hanging drop culture, their cells segregate into discrete phases with ectoderm adopting an internal position relative to the mesendoderm. The position adopted directly correlates with differences in tissue surface tension. We also show that germ layer tissues from untreated embryos, when extirpated and placed in culture, adopt a configuration similar to those of their mRNA-overexpressing counterparts. Down-regulating E-cadherin expression in the ectoderm leads to reduced surface tension and results in phase reversal with E-cadherin-depleted ectoderm cells now adopting an external position relative to the mesendoderm. These results show that in vitro cell sorting of zebrafish mesendoderm and ectoderm tissues is specified by tissue interfacial tensions. We perform a mathematical analysis indicating that tissue interfacial tension between actively motile cells contributes to the spatial organization and dynamics of these zebrafish germ layers in vivo.}, author = {Schötz, Eva and Burdine, Rebecca and Julicher, Frank and Steinberg, Malcolm and Heisenberg, Carl-Philipp J and Foty, Ramsey}, journal = {HFSP Journal}, number = {1}, pages = {42 -- 56}, publisher = {HFSP Publishing}, title = {{Quantitative differences in tissue surface tension influence zebrafish germ layer positioning}}, doi = {10.2976/1.2834817}, volume = {2}, year = {2008}, } @article{4181, abstract = {Understanding the factors that direct tissue organization during development is one of the most fundamental goals in developmental biology. Various hypotheses explain cell sorting and tissue organization on the basis of the adhesive and mechanical properties of the constituent cells(1). However, validating these hypotheses has been difficult due to the lack of appropriate tools to measure these parameters. Here we use atomic force microscopy ( AFM) to quantify the adhesive and mechanical properties of individual ectoderm, mesoderm and endoderm progenitor cells from gastrulating zebrafish embryos. Combining these data with tissue self-assembly in vitro and the sorting behaviour of progenitors in vivo, we have shown that differential actomyosin-dependent cell-cortex tension, regulated by Nodal/ TGF beta-signalling ( transforming growth factor beta), constitutes a key factor that directs progenitor-cell sorting. These results demonstrate a previously unrecognized role for Nodal-controlled cell-cortex tension in germ-layer organization during gastrulation.}, author = {Krieg, Michael and Arboleda Estudillo, Yohanna and Puech, Pierre and Käfer, Jos and Graner, François and Mueller, Daniel and Heisenberg, Carl-Philipp J}, journal = {Nature Cell Biology}, number = {4}, pages = {429 -- 436}, publisher = {Nature Publishing Group}, title = {{Tensile forces govern germ-layer organization in zebrafish}}, doi = {10.1038/ncb1705}, volume = {10}, year = {2008}, } @article{4180, abstract = {(Figure Presented) The name's Bond: Separated cells form membranous nanotubes whose tips are tethered by adhesive bonds (see picture). The lifetime of receptor-ligand interactions can be measured by using membrane nanotubes of living cells as constant force actuators. Because the nanotubes are extruded from living cells at conditions approaching the physiological, cellular processes can be both studied and utilized. }, author = {Krieg, Michael and Helenius, Jonne and Heisenberg, Carl-Philipp J and Mueller, Daniel}, journal = {Angewandte Chemie - International Edition}, number = {50}, pages = {9775 -- 9777}, publisher = {Wiley-Blackwell}, title = {{A Bond for a Lifetime: Employing Membrane Nanotubes from Living Cells to Determine Receptor-Ligand Kinetics}}, doi = {10.1002/anie.200803552}, volume = {47}, year = {2008}, } @article{4193, abstract = {The controlled adhesion of cells to each other and to the extracellular matrix is crucial for tissue development and maintenance. Numerous assays have been developed to quantify cell adhesion. Among these, the use of atomic force microscopy (AFM) for single-cell force spectroscopy (SCFS) has recently been established. This assay permits the adhesion of living cells to be studied in near-physiological conditions. This implementation of AFM allows unrivaled spatial and temporal control of cells, as well as highly quantitative force actuation and force measurement that is sufficiently sensitive to characterize the interaction of single molecules. Therefore, not only overall cell adhesion but also the properties of single adhesion-receptor-ligand interactions can be studied. Here we describe current implementations and applications of SCFS, as well as potential pitfalls, and outline how developments will provide insight into the forces, energetics and kinetics of cell-adhesion processes.}, author = {Helenius, Jonne and Heisenberg, Carl-Philipp J and Gaub, Hermann and Mueller, Daniel}, journal = {Journal of Cell Science}, number = {11}, pages = {1785 -- 1791}, publisher = {Company of Biologists}, title = {{Single-cell force spectroscopy}}, doi = {10.1242/​jcs.030999}, volume = {121}, year = {2008}, } @article{4198, abstract = {Animal body plan arises during gastrulation and organogenesis by the coordination of inductive events and cell movements. Several signaling pathways, such as BMP, FGF, Hedgehog, Nodal, and Wnt have well-recognized instructive roles in cell fate specification during vertebrate embryogenesis. Growing evidence indicates that BMP, Nodal, and FGF signaling also regulate cell movements, and that they do so through mechanisms distinct from those that specify cell fates. Moreover, pathways controlling cell movements can also indirectly influence cell fate specification by regulating dimensions and relative positions of interacting tissues. The current challenge is to delineate the molecular mechanisms via which the major signaling pathways regulate cell fate specification and movements, and how these two processes are coordinated to ensure normal development.}, author = {Heisenberg, Carl-Philipp J and Solnica Krezel, Lilianna}, journal = {Current Opinion in Genetics & Development}, number = {4}, pages = {311 -- 316}, publisher = {Elsevier}, title = {{Back and forth between cell fate specification and movement during vertebrate gastrulation}}, doi = {10.1016/j.gde.2008.07.011}, volume = {18}, year = {2008}, } @article{4227, abstract = {Morphogen concentration gradients provide positional information by activating target genes in a concentration-dependent manner. Recent reports show that the gradient of the syncytial morphogen Bicoid seems to provide precise positional information to determine target gene domains. For secreted morphogenetic ligands, the precision of the gradients, the signal transduction and the reliability of target gene expression domains have not been studied. Here we investigate these issues for the TGF-beta-type morphogen Dpp. We first studied theoretically how cell-to-cell variability in the source, the target tissue, or both, contribute to the variations of the gradient. Fluctuations in the source and target generate a local maximum of precision at a finite distance to the source. We then determined experimentally in the wing epithelium: (1) the precision of the Dpp concentration gradient; (2) the precision of the Dpp signaling activity profile; and (3) the precision of activation of the Dpp target gene spalt. As captured by our theoretical description, the Dpp gradient provides positional information with a maximal precision a few cells away from the source. This maximal precision corresponds to a positional uncertainly of about a single cell diameter. The precision of the Dpp gradient accounts for the precision of the spalt expression range, implying that Dpp can act as a morphogen to coarsely determine the expression pattern of target genes.}, author = {Bollenbach, Tobias and Pantazis, Periklis and Anna Kicheva and Bokel, Christian and González-Gaitán, Marcos and Julicher, Frank}, journal = {Development}, number = {6}, pages = {1137 -- 1146}, publisher = {Company of Biologists}, title = {{Precision of the Dpp gradient}}, doi = {10.1242/dev.012062}, volume = {135}, year = {2008}, } @article{4245, abstract = {Sex allocation theory has proved extremely successful at predicting when individuals should adjust the sex of their offspring in response to environmental conditions. However, we know rather little about the underlying genetics of sex ratio or how genetic architecture might constrain adaptive sex-ratio behavior. We examined how mutation influenced genetic variation in the sex ratios produced by the parasitoid wasp Nasonia vitripennis. In a mutation accumulation experiment, we determined the mutability of sex ratio, and compared this with the amount of genetic variation observed in natural populations. We found that the mutability (h2m) ranges from 0.001 to 0.002, similar to estimates for life-history traits in other organisms. These estimates suggest one mutation every 5–60 generations, which shift the sex ratio by approximately 0.01 (proportion males). In this and other studies, the genetic variation in N. vitripennis sex ratio ranged from 0.02 to 0.17 (broad-sense heritability, H2). If sex ratio is maintained by mutation–selection balance, a higher genetic variance would be expected given our mutational parameters. Instead, the observed genetic variance perhaps suggests additional selection against sex-ratio mutations with deleterious effects on other fitness traits as well as sex ratio (i.e., pleiotropy), as has been argued to be the case more generally.}, author = {Pannebakker, Bart A and Halligan, Daniel and Reynolds, K Tracy and Ballantyne, Gavin A and Shuker, David M and Nicholas Barton and West, Stuart A}, journal = {Evolution; International Journal of Organic Evolution}, number = {8}, pages = {1921 -- 1935}, publisher = {Wiley-Blackwell}, title = {{Effects of spontaneous mutation accumulation on sex ratio traits}}, doi = {10.1111/j.1558-5646.2008.00434.x}, volume = {62}, year = {2008}, } @inproceedings{4244, abstract = {This paper presents a new approach to optimization of an energy-constrained modulation scheme for wireless sensor networks by taking advantage of a novel bio-inspired optimization algorithm. The algorithm is inspired by Wrightpsilas shifting balance theory (SBT) of evolution in population genetics. The total energy consumption of an energy-constrained modulation scheme is minimized by using the new SBT-based optimization algorithm. The results obtained by this new algorithm are compared with other popular optimization algorithms. Numerical experiments are performed to demonstrate that the SBT-based algorithm could be used as an efficient optimizer for solving the optimization problems arising from currently emerging energy-efficient wireless sensor networks.}, author = {Yang, Erfu and Nicholas Barton and Arslan, Tughrul and Erdogan, Ahmet T}, pages = {2749 -- 2756}, publisher = {IEEE}, title = {{A novel shifting balance theory-based approach to optimization of an energy-constrained modulation scheme for wireless sensor networks}}, doi = {10.1109/CEC.2008.4631167}, year = {2008}, } @inbook{4371, abstract = {We survey some of the problems associated with checking whether a given behavior (a sequence, a Boolean signal or a continuous signal) satisfies a property specified in an appropriate temporal logic and describe two such monitoring algorithms for the real-time logic MITL.}, author = {Maler, Oded and Nickovic, Dejan and Pnueli, Amir}, booktitle = {Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday}, isbn = {9783540781264}, pages = {475 -- 505}, publisher = {Springer}, title = {{Checking Temporal Properties of Discrete, Timed and Continuous Behaviors}}, doi = {10.1007/978-3-540-78127-1_26}, year = {2008}, } @inproceedings{4366, abstract = {Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique interplay between counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential.}, author = {Podelski,Andreas and Rybalchenko, Andrey and Thomas Wies}, pages = {314 -- 327}, publisher = {Springer}, title = {{Heap Assumptions on Demand}}, doi = {10.1007/978-3-540-70545-1_31}, volume = {5123}, year = {2008}, } @article{3038, abstract = {Lateral roots originate deep within the parental root from a small number of founder cells at the periphery of vascular tissues and must emerge through intervening layers of tissues. We describe how the hormone auxin, which originates from the developing lateral root, acts as a local inductive signal which re-programmes adjacent cells. Auxin induces the expression of a previously uncharacterized auxin influx carrier LAX3 in cortical and epidermal cells directly overlaying new primordia. Increased LAX3 activity reinforces the auxin-dependent induction of a selection of cell-wall-remodelling enzymes, which are likely to promote cell separation in advance of developing lateral root primordia.}, author = {Swarup, Kamal and Eva Benková and Swarup, Ranjan and Casimiro, Ilda and Péret, Benjamin and Yang, Yaodong and Parry, Geraint and Nielsen, Erik and De Smet, Ive and Vanneste, Steffen and Levesque, Mitchell P and Carrier, David and James, Nicholas and Calvo, Vanessa and Ljung, Karin and Kramer, Eric and Roberts, Rebecca and Graham, Neil and Marillonnet, Sylvestre and Patel, Kanu and Jones, Jonathan D and Taylor, Christopher G and Schachtman, Daniel P and May, Sean and Sandberg, Göran and Benfey, Philip N and Jirí Friml and Kerr, Ian and Beeckman, Tom and Laplaze, Laurent and Bennett, Malcolm J}, journal = {Nature Cell Biology}, number = {8}, pages = {946 -- 954}, publisher = {Nature Publishing Group}, title = {{The auxin influx carrier LAX3 promotes lateral root emergence}}, doi = {10.1038/ncb1754}, volume = {10}, year = {2008}, } @article{3036, abstract = {Plants exhibit an exceptional adaptability to different environmental conditions. To a large extent, this adaptability depends on their ability to initiate and form new organs throughout their entire postembryonic life. Plant shoot and root systems unceasingly branch and form axillary shoots or lateral roots, respectively. The first event in the formation of a new organ is specification of founder cells. Several plant hormones, prominent among them auxin, have been implicated in the acquisition of founder cell identity by differentiated cells, but the mechanisms underlying this process are largely elusive. Here, we show that auxin and its local accumulation in root pericycle cells is a necessary and sufficient signal to respecify these cells into lateral root founder cells. Analysis of the alf4-1 mutant suggests that specification of founder cells and the subsequent activation of cell division leading to primordium formation represent two genetically separable events. Time-lapse experiments show that the activation of an auxin response is the earliest detectable event in founder cell specification. Accordingly, local activation of auxin response correlates absolutely with the acquisition of founder cell identity and precedes the actual formation of a lateral root primordium through patterned cell division. Local production and subsequent accumulation of auxin in single pericycle cells induced by Cre-Lox-based activation of auxin synthesis converts them into founder cells. Thus, auxin is the local instructive signal that is sufficient for acquisition of founder cell identity and can be considered a morphogenetic trigger in postembryonic plant organogenesis.}, author = {Dubrovsky, Joseph G and Sauer, Michael and Napsucialy-Mendivil, Selene and Ivanchenko, Maria G and Jirí Friml and Shishkova, Svetlana and Celenza, John and Eva Benková}, journal = {PNAS}, number = {25}, pages = {8790 -- 8794}, publisher = {National Academy of Sciences}, title = {{Auxin acts as a local morphogenetic trigger to specify lateral root founder cells}}, doi = {10.1073/pnas.0712307105}, volume = {105}, year = {2008}, } @article{3030, abstract = {Telomeres in many eukaryotes are maintained by telomerase in whose absence telomere shortening occurs. However, telomerase-deficient Arabidopsis thaliana mutants (Attert -/-) show extremely low rates of telomere shortening per plant generation (250-500 bp), which does not correspond to the expected outcome of replicative telomere shortening resulting from ca. 1,000 meristem cell divisions per seed-to-seed generation. To investigate the influence of the number of cell divisions per seed-to-seed generation, Attert -/- mutant plants were propagated from seeds coming either from the lower-most or the upper-most siliques (L- and U-plants) and the length of their telomeres were followed over several generations. The rate of telomere shortening was faster in U-plants, than in L-plants, as would be expected from their higher number of cell divisions per generation. However, this trend was observed only in telomeres whose initial length is relatively high and the differences decreased with progressive general telomere shortening over generations. But in generation 4, the L-plants frequently show a net telomere elongation, while the U-plants fail to do so. We propose that this is due to the activation of alternative telomere lengthening (ALT), a process which is activated in early embryonic development in both U- and L-plants, but is overridden in U-plants due to their higher number of cell divisions per generation. These data demonstrate what so far has only been speculated, that in the absence of telomerase, the number of cell divisions within one generation influences the control of telomere lengths. These results also reveal a fast and efficient activation of ALT mechanism(s) in response to the loss of telomerase activity and imply that ALT is probably involved also in normal plant development.}, author = {Růčková, Eva and Jirí Friml and Procházková Schrumpfová, Petra and Fajkus, Jiří}, journal = {Plant Molecular Biology}, number = {6}, pages = {637 -- 646}, publisher = {Springer}, title = {{Role of alternative telomere lengthening unmasked in telomerase knock-out mutant plants}}, doi = {10.1007/s11103-008-9295-7}, volume = {66}, year = {2008}, } @article{3032, abstract = { Cell polarity manifested by the polar cargo delivery to different plasma-membrane domains is a fundamental feature of multicellular organisms. Pathways for polar delivery have been identified in animals; prominent among them is transcytosis, which involves cargo movement between different sides of the cell [1]. PIN transporters are prominent polar cargoes in plants, whose polar subcellular localization determines the directional flow of the signaling molecule auxin [2, 3]. In this study, we address the cellular mechanisms of PIN polar targeting and dynamic polarity changes. We show that apical and basal PIN targeting pathways are interconnected but molecularly distinct by means of ARF GEF vesicle-trafficking regulators. Pharmacological or genetic interference with the Arabidopsis ARF GEF GNOM leads specifically to apicalization of basal cargoes such as PIN1. We visualize the translocation of PIN proteins between the opposite sides of polarized cells in vivo and show that this PIN transcytosis occurs by endocytic recycling and alternative recruitment of the same cargo molecules by apical and basal targeting machineries. Our data suggest that an ARF GEF-dependent transcytosis-like mechanism is operational in plants and provides a plausible mechanism to trigger changes in PIN polarity and hence auxin fluxes during embryogenesis and organogenesis.}, author = {Kleine-Vehn, Jürgen and Dhonukshe, Pankaj and Sauer, Michael and Brewer, Philip B and Wiśniewska, Justyna and Paciorek, Tomasz and Eva Benková and Jirí Friml}, journal = {Current Biology}, number = {7}, pages = {526 -- 531}, publisher = {Cell Press}, title = {{ARF GEF dependent transcytosis and polar delivery of PIN auxin carriers in Arabidopsis}}, doi = {10.1016/j.cub.2008.03.021}, volume = {18}, year = {2008}, } @inbook{3035, abstract = {Embryogenesis of Arabidopsis thaliana follows a nearly invariant cell division pattern and provides an ideal system for studies of early plant development. However, experimental manipulation with embryogenesis is difficult, as the embryo develops deeply inside maternal tissues. Here, we present a method to culture zygotic Arabidopsis embryos in vitro. It enables culturing for prolonged periods of time from the first developmental stages on. The technique omits excision of the embryo by culturing the entire ovule, which facilitates the manual procedure. It allows pharmacological manipulation of embryo development and does not interfere with standard techniques for localizing gene expression and protein localization in the cultivated embryos.}, author = {Sauer, Michael and Jirí Friml}, booktitle = {Plant Embryogenesis}, editor = {Suárez, María F and Bozhkov, Peter V}, pages = {71 -- 76}, publisher = {Humana Press}, title = {{In vitro culture of Arabidopsis embryos }}, doi = {10.1007/978-1-59745-273-1_5}, volume = {427}, year = {2008}, } @inbook{3033, abstract = { Embryogenesis in Arabidopsis thaliana depends on the proper establishment and maintenance of local auxin accumulation. In the course of elucidating the connections between developmental progress and auxin distribution, several techniques have been developed to investigate spatial and temporal distribution of auxin response or accumulation in Arabidopsis embryos. This chapter reviews and describes two independent methods, the detection of the activity of auxin responsive transgenes and immunolocalization of auxin itself.}, author = {Sauer, Michael and Jirí Friml}, booktitle = {Plant Embryogenesis}, editor = {Suárez, María F and Bozhkov, Peter V}, pages = {137 -- 144}, publisher = {Humana Press}, title = {{Visualization of auxin gradients in embryogenesis }}, doi = {10.1007/978-1-59745-273-1_11}, volume = {427}, year = {2008}, } @article{3037, author = {Feraru, Elena and Friml, Jirí}, journal = {Plant Physiology}, number = {4}, pages = {1553 -- 1559}, publisher = {American Society of Plant Biologists}, title = {{PIN polar targeting}}, doi = {10.1104/pp.108.121756}, volume = {147}, year = {2008}, } @article{3034, abstract = {They can't move away from shade, so plants resort to a molecular solution to find a place in the sun. The action they take is quite radical, and involves a reprogramming of their development. }, author = {Friml, Jirí and Sauer, Michael}, journal = {Nature}, number = {7193}, pages = {298 -- 299}, publisher = {Nature Publishing Group}, title = {{Plant biology: In their neighbour's shadow}}, doi = {10.1038/453298a}, volume = {453}, year = {2008}, } @article{3196, abstract = {Among the most exciting advances in early vision has been the development of efficient energy minimization algorithms for pixel-labeling tasks such as depth or texture computation. It has been known for decades that such problems can be elegantly expressed as Markov random fields, yet the resulting energy minimization problems have been widely viewed as intractable. Algorithms such as graph cuts and loopy belief propagation (LBP) have proven to be very powerful: For example, such methods form the basis for almost all the top-performing stereo methods. However, the trade-offs among different energy minimization algorithms are still not well understood. In this paper, we describe a set of energy minimization benchmarks and use them to compare the solution quality and runtime of several common energy minimization algorithms. We investigate three promising methods-graph cuts, LBP, and tree-reweighted message passing-in addition to the well-known older iterated conditional mode (ICM) algorithm. Our benchmark problems are drawn from published energy functions used for stereo, image stitching, interactive segmentation, and denoising. We also provide a general-purpose software interface that allows vision researchers to easily switch between optimization methods. The benchmarks, code, images, and results are available at http://vision.middlebury.edu/MRF/.}, author = {Szeliski, Richard S and Zabih, Ramin and Scharstein, Daniel and Veksler, Olga and Vladimir Kolmogorov and Agarwala, Aseem and Tappen, Marshall F and Rother, Carsten}, journal = {IEEE Transactions on Pattern Analysis and Machine Intelligence}, number = {6}, pages = {1068 -- 1080}, publisher = {IEEE}, title = {{A comparative study of energy minimization methods for Markov random fields with smoothness-based priors}}, doi = {10.1109/TPAMI.2007.70844}, volume = {30}, year = {2008}, } @inproceedings{3198, abstract = {In this paper we present a new approach for establishing correspondences between sparse image features related by an unknown non-rigid mapping and corrupted by clutter and occlusion, such as points extracted from a pair of images containing a human figure in distinct poses. We formulate this matching task as an energy minimization problem by defining a complex objective function of the appearance and the spatial arrangement of the features. Optimization of this energy is an instance of graph matching, which is in general a NP-hard problem. We describe a novel graph matching optimization technique, which we refer to as dual decomposition (DD), and demonstrate on a variety of examples that this method outperforms existing graph matching algorithms. In the majority of our examples DD is able to find the global minimum within a minute. The ability to globally optimize the objective allows us to accurately learn the parameters of our matching model from training examples. We show on several matching tasks that our learned model yields results superior to those of state-of-the-art methods. }, author = {Torresani, Lorenzo and Vladimir Kolmogorov and Rother, Carsten}, pages = {596 -- 609}, publisher = {Springer}, title = {{Feature correspondence via graph matching: Models and global optimization}}, doi = {10.1007/978-3-540-88688-4_44}, volume = {5303}, year = {2008}, } @inproceedings{3195, abstract = {Graph cut is a popular technique for interactive image segmentation. However, it has certain shortcomings. In particular, graph cut has problems with segmenting thin elongated objects due to the ldquoshrinking biasrdquo. To overcome this problem, we propose to impose an additional connectivity prior, which is a very natural assumption about objects. We formulate several versions of the connectivity constraint and show that the corresponding optimization problems are all NP-hard. For some of these versions we propose two optimization algorithms: (i) a practical heuristic technique which we call DijkstraGC, and (ii) a slow method based on problem decomposition which provides a lower bound on the problem. We use the second technique to verify that for some practical examples DijkstraGC is able to find the global minimum.}, author = {Vicente, Sara and Vladimir Kolmogorov and Rother, Carsten}, publisher = {IEEE}, title = {{Graph cut based image segmentation with connectivity priors}}, doi = {10.1109/CVPR.2008.4587440}, year = {2008}, } @inproceedings{3224, abstract = {We propose a new mode of operation, enciphered CBC, for domain extension of length-preserving functions (like block ciphers), which is a variation on the popular CBC mode of operation. Our new mode is twice slower than CBC, but has many (property-preserving) properties not enjoyed by CBC and other known modes. Most notably, it yields the first constant-rate Variable Input Length (VIL) MAC from any length preserving Fixed Input Length (FIL) MAC. This answers the question of Dodis and Puniya from Eurocrypt 2007. Further, our mode is a secure domain extender for PRFs (with basically the same security as encrypted CBC). This provides a hedge against the security of the block cipher: if the block cipher is pseudorandom, one gets a VIL-PRF, while if it is "only" unpredictable, one "at least" gets a VIL-MAC. Additionally, our mode yields a VIL random oracle (and, hence, a collision-resistant hash function) when instantiated with length-preserving random functions, or even random permutations (which can be queried from both sides). This means that one does not have to re-key the block cipher during the computation, which was critically used in most previous constructions (analyzed in the ideal cipher model). }, author = {Dodis, Yevgeniy and Krzysztof Pietrzak and Puniya, Prashant}, pages = {198 -- 219}, publisher = {Springer}, title = {{A new mode of operation for block ciphers and length preserving MACs}}, doi = {10.1007/978-3-540-78967-3_12}, volume = {4965}, year = {2008}, } @inproceedings{3225, abstract = {A robust multi-property combiner for a set of security properties merges two hash functions such that the resulting function satisfies each of the properties which at least one of the two starting functions has. Fischlin and Lehmann (TCC 2008) recently constructed a combiner which simultaneously preserves collision-resistance, target collision-resistance, message authentication, pseudorandomness and indifferentiability from a random oracle (IRO). Their combiner produces outputs of 5n bits, where n denotes the output length of the underlying hash functions. In this paper we propose improved combiners with shorter outputs. By sacrificing the indifferentiability from random oracles we obtain a combiner which preserves all of the other aforementioned properties but with output length 2n only. This matches a lower bound for black-box combiners for collision-resistance as the only property, showing that the other properties can be achieved without penalizing the length of the hash values. We then propose a combiner which also preserves the IRO property, slightly increasing the output length to 2n + ω(logn). Finally, we show that a twist on our combiners also makes them robust for one-wayness (but at the price of a fixed input length). }, author = {Fischlin, Marc and Lehmann, Anja and Krzysztof Pietrzak}, number = {PART 2}, pages = {655 -- 666}, publisher = {Springer}, title = {{Robust multi property combiners for hash functions revisited}}, doi = {10.1007/978-3-540-70583-3_53}, volume = {5126}, year = {2008}, } @article{3291, abstract = {The filamentous fungus Aspergillus fumigatus is responsible for a lethal disease called Invasive Aspergillosis that affects immunocompromised patients. This disease, like other human fungal diseases, is generally treated by compounds targeting the primary fungal cell membrane sterol. Recently, glucan synthesis inhibitors were added to the limited antifungal arsenal and encouraged the search for novel targets in cell wall biosynthesis. Although galactomannan is a major component of the A. fumigatus cell wall and extracellular matrix, the biosynthesis and role of galactomannan are currently unknown. By a targeted gene deletion approach, we demonstrate that UDP-galactopyranose mutase, a key enzyme of galactofuranose metabolism, controls the biosynthesis of galactomannan and galactofuranose containing glycoconjugates. The glfA deletion mutant generated in this study is devoid of galactofuranose and displays attenuated virulence in a low-dose mouse model of invasive aspergillosis that likely reflects the impaired growth of the mutant at mammalian body temperature. Furthermore, the absence of galactofuranose results in a thinner cell wall that correlates with an increased susceptibility to several antifungal agents. The UDP-galactopyranose mutase thus appears to be an appealing adjunct therapeutic target in combination with other drugs against A. fumigatus. Its absence from mammalian cells indeed offers a considerable advantage to achieve therapeutic selectivity. }, author = {Philipp Schmalhorst and Krappmann, Sven and Vervecken, Wouter and Rohde, Manfred and Müller, Meike and Braus, Gerhard H. and Contreras, Roland and Braun, Armin and Bakker, Hans and Routier, Françoise H}, journal = {Eukaryotic Cell}, number = {8}, pages = {1268 -- 1277}, publisher = {American Society for Microbiology}, title = {{Contribution of galactofuranose to the virulence of the opportunistic pathogen Aspergillus fumigatus}}, doi = {10.1128/EC.00065-08}, volume = {7}, year = {2008}, } @article{3307, abstract = {A complete mitochondrial (mt) genome sequence was reconstructed from a 38,000 year-old Neandertal individual with 8341 mtDNA sequences identified among 4.8 Gb of DNA generated from ∼0.3 g of bone. Analysis of the assembled sequence unequivocally establishes that the Neandertal mtDNA falls outside the variation of extant human mtDNAs, and allows an estimate of the divergence date between the two mtDNA lineages of 660,000 ± 140,000 years. Of the 13 proteins encoded in the mtDNA, subunit 2 of cytochrome c oxidase of the mitochondrial electron transport chain has experienced the largest number of amino acid substitutions in human ancestors since the separation from Neandertals. There is evidence that purifying selection in the Neandertal mtDNA was reduced compared with other primate lineages, suggesting that the effective population size of Neandertals was small.}, author = {Green, Richard E and Malaspinas, Anna-Sapfo and Krause, Johannes and Briggs, Adrian W and Johnson, Philip L and Caroline Uhler and Meyer, Matthias and Good, Jeffrey M and Maricic, Tomislav and Stenzel, Udo and Prüfer, Kay and Siebauer, Michael F and Burbano, Hernän A and Ronan, Michael T and Rothberg, Jonathan M and Egholm, Michael and Rudan, Pavao and Brajković, Dejana and Kućan, Željko and Gušić, Ivan and Wikström, Mårten K and Laakkonen, Liisa J and Kelso, Janet F and Slatkin, Montgomery and Pääbo, Svante H}, journal = {Cell}, pages = {416 -- 426}, publisher = {Cell Press}, title = {{A complete neandertal mitochondrial genome sequence determined by highhhroughput sequencing}}, doi = {10.1016/j.cell.2008.06.021}, volume = {134}, year = {2008}, } @article{3435, abstract = {We develop a new method for estimating effective population sizes, Ne, and selection coefficients, s, from time-series data of allele frequencies sampled from a single diallelic locus. The method is based on calculating transition probabilities, using a numerical solution of the diffusion process, and assuming independent binomial sampling from this diffusion process at each time point. We apply the method in two example applications. First, we estimate selection coefficients acting on the CCR5-Δ32 mutation on the basis of published samples of contemporary and ancient human DNA. We show that the data are compatible with the assumption of s = 0, although moderate amounts of selection acting on this mutation cannot be excluded. In our second example, we estimate the selection coefficient acting on a mutation segregating in an experimental phage population. We show that the selection coefficient acting on this mutation is ~0.43.}, author = {Jonathan Bollback and York, Thomas L and Nielsen, Rasmus}, journal = {Genetics}, number = {1}, pages = {497 -- 502}, publisher = {Genetics Society of America}, title = {{Estimation of 2Nes From Temporal Allele Frequency Data}}, doi = {10.1534/genetics.107.085019}, volume = {179}, year = {2008}, } @article{3516, abstract = {Temporal coding is a means of representing information by the time, as opposed to the rate, at which neurons fire. Evidence of temporal coding in the hippocampus comes from place cells, whose spike times relative to theta oscillations reflect a rat's position while running along stereotyped trajectories. This arises from the backwards shift in cell firing relative to local theta oscillations (phase precession). Here we demonstrate phase precession during place-field crossings in an open-field foraging task. This produced spike sequences in each theta cycle that disambiguate the rat's trajectory through two-dimensional space and can be used to predict movement direction. Furthermore, position and movement direction were maximally predicted from firing in the early and late portions of the theta cycle, respectively. This represents the first direct evidence of a combined representation of position, trajectory and heading in the hippocampus, organized on a fine temporal scale by theta oscillations.}, author = {Huxter,John R and Senior,Timothy J and Allen, Kevin and Jozsef Csicsvari}, journal = {Nature Neuroscience}, number = {5}, pages = {587 -- 594}, publisher = {Nature Publishing Group}, title = {{Theta phase-specific codes for two-dimensional position, trajectory and heading in the hippocampus}}, doi = {10.1038/nn.2106}, volume = {11}, year = {2008}, } @article{3530, abstract = {In the cerebral cortex, GABAergic interneurons are often regarded as fast-spiking cells. We have identified a type of slow-spiking interneuron that offers distinct contributions to network activity. “Ivy” cells, named after their dense and fine axons innervating mostly basal and oblique pyramidal cell dendrites, are more numerous than the parvalbumin-expressing basket, bistratified, or axo-axonic cells. Ivy cells express nitric oxide synthase, neuropeptide Y, and high levels of GABA(A) receptor alpha 1 subunit; they discharge at a low frequency with wide spikes in vivo, yet are distinctively phase-locked to behaviorally relevant network rhythms including theta, gamma, and ripple oscillations. Paired recordings in vitro showed that Ivy cells receive depressing EPSPs from pyramidal cells, which in turn receive slowly rising and decaying inhibitory input from Ivy cells. In contrast to fast-spiking interneurons operating with millisecond precision, the highly abundant Ivy cells express presynaptically acting neuromodulators and regulate the excitability of pyramidal cell dendrites through slowly rising and decaying GABAergic inputs.}, author = {Fuentealba,Pablo and Begum,Rahima and Capogna,Marco and Jinno,Shozo and Marton,Laszlo F and Jozsef Csicsvari and Thomson,Alex and Somogyi, Péter and Klausberger,Thomas}, journal = {Neuron}, number = {6}, pages = {917 -- 929}, publisher = {Elsevier}, title = {{Ivy cells: A population of nitric-oxide-producing, slow-spiking GABAergic neurons and their involvement in hippocampal network activity}}, doi = {10.1016/j.neuron.2008.01.034}, volume = {57}, year = {2008}, } @article{3544, abstract = {In the subthalamic nucleus (STN) of Parkinson's disease (PD) patients, a pronounced synchronization of oscillatory activity at beta frequencies (15-30 Hz) accompanies movement difficulties. Abnormal beta oscillations and motor symptoms are concomitantly and acutely suppressed by dopaminergic therapies, suggesting that these inappropriate rhythms might also emerge acutely from disrupted dopamine transmission. The neural basis of these abnormal beta oscillations is unclear, and how they might compromise information processing, or how they arise, is unknown. Using a 6-hydroxydopamine-lesioned rodent model of PD, we demonstrate that beta oscillations are inappropriately exaggerated, compared with controls, in a brain-state-dependent manner after chronic dopamine loss. Exaggerated beta oscillations are expressed at the levels of single neurons and small neuronal ensembles, and are focally present and spatially distributed within STN. They are also expressed in synchronous population activities, as evinced by oscillatory local field potentials, in STN and cortex. Excessively synchronized beta oscillations reduce the information coding capacity of STN neuronal ensembles, which may contribute to parkinsonian motor impairment. Acute disruption of dopamine transmission in control animals with antagonists of D-1/D-2 receptors did not exaggerate STN or cortical beta oscillations. Moreover, beta oscillations were not exaggerated until several days after 6-hydroxydopamine injections. Thus, contrary to predictions, abnormally amplified beta oscillations in cortico-STN circuits do not result simply from an acute absence of dopamine receptor stimulation, but are instead delayed sequelae of chronic dopamine depletion. Targeting the plastic processes underlying the delayed emergence of pathological beta oscillations after continuing dopaminergic dysfunction may offer considerable therapeutic promise.}, author = {Mallet,Nicolas and Pogosyan,Alek and Sharott,Andrew and Jozsef Csicsvari and Bolam, John Paul and Brown,Peter and Magill,Peter J}, journal = {Journal of Neuroscience}, number = {18}, pages = {4795 -- 4806}, publisher = {Society for Neuroscience}, title = {{Disrupted dopamine transmission and the emergence of exaggerated beta oscillations in subthalamic nucleus and cerebral cortex}}, doi = {10.1523/JNEUROSCI.0123-08.2008}, volume = {28}, year = {2008}, } @inbook{3577, author = {Biasotti, Silvia and Attali, Dominique and Boissonnat, Jean-Daniel and Herbert Edelsbrunner and Elber, Gershon and Mortara, Michela and Sanniti di Baja, Gabriella and Spagnuolo, Michela and Tanase, Mirela and Veltkam, Remco}, booktitle = {Shape Analysis and Structuring}, pages = {145 -- 183}, publisher = {Springer}, title = {{Skeletal structures}}, doi = {10.1007/978-3-540-33265-7_5}, year = {2008}, } @article{3591, abstract = {The controlled internalization of membrane receptors and lipids is crucial for cells to control signaling pathways and interact with their environment. During clathrin-mediated endocytosis, membrane constituents are transported via endocytic vesicles into early endosomes, from which they are further distributed within the cell. The small guanosine triphosphatase (GTPase) Rab5 is both required and sufficient for the formation of these early endosomes and can be used to experimentally address endocytic processes. Recent evidence shows that endocytic turnover of E-cadherin regulates the migration of mesendodermal cells during zebrafish gastrulation by modulating their adhesive interactions with neighboring cells. This in turn leads to effective and synchronized movement within the embryo. In this review, we discuss techniques to manipulate E-cadherin endocytosis by morpholino-mediated knockdown of rab5 during zebrafish gastrulation. We describe the use of antibodies specifically directed against zebrafish E-cadherin to detect its intracellular localization and of in situ hybridization and primary cell culture to reveal patterns of cell migration and adhesion, respectively}, author = {Ulrich, Florian and Heisenberg, Carl-Philipp J}, journal = {Methods in Molecular Biology}, pages = {371 -- 387}, publisher = {Springer}, title = {{Probing E-cadherin endocytosis by morpholino-mediated Rab5 knock-down in zebrafish.}}, doi = {10.1007/978-1-59745-178-9_27}, volume = {440}, year = {2008}, } @inproceedings{3599, abstract = {In this paper, adaptive formation control and bio-inspired optimization are jointly addressed for a cluster-based satellite wireless sensor network in which there are multiple satellites flying in formation (MSFF) in the presence of unknown disturbances. The full nonlinear dynamics model describing the relative positioning of the MSFF system is used to develop an adaptive formation controller. First, the original nonlinear system is transformed into a linear controllable system with aperturbation term by invoking the input-output feedback linearization technique. Second, by using the integral feedback design scheme, the adaptive formation controller is presented for improving the steady-state performance of the MSFF system in the presence of unknown disturbances. Third, as a currently popular bio-inspired algorithm, PSO (particle swarm optimizer) is employed to minimize the total energy consumption under the required quality of service by jointly optimizing the transmission power and rate for each satellite. Simulation results are provided to demonstrate the effectiveness of the adaptive formation controller and the PSO-based optimization for saving the total communication energy.}, author = {Yang, Erfu and Erdogan, Ahmet T and Arslan, Tughrul and Nicholas Barton}, pages = {432 -- 439}, publisher = {IEEE}, title = {{Adaptive formation control and bio-inspired optimization of a cluster-based satellite wireless sensor network }}, doi = {10.1109/AHS.2008.60}, year = {2008}, } @inproceedings{3698, abstract = {Kernel canonical correlation analysis (KCCA) is a dimensionality reduction technique for paired data. By finding directions that maximize correlation, KCCA learns representations that are more closely tied to the underlying semantics of the data rather than noise. However, meaningful directions are not only those that have high correlation to another modality, but also those that capture the manifold structure of the data. We propose a method that is simultaneously able to find highly correlated directions that are also located on high variance directions along the data manifold. This is achieved by the use of semi-supervised Laplacian regularization of KCCA. We show experimentally that Laplacian regularized training improves class separation over KCCA with only Tikhonov regularization, while causing no degradation in the correlation between modalities. We propose a model selection criterion based on the Hilbert-Schmidt norm of the semi-supervised Laplacian regularized cross-covariance operator, which we compute in closed form.}, author = {Blaschko,Matthew B and Christoph Lampert and Gretton,Arthur}, number = {Part 1}, pages = {133 -- 145}, publisher = {Springer}, title = {{Semi-supervised Laplacian regularization of kernel canonical correlation analysis}}, doi = {10.1007/978-3-540-87479-9_27}, volume = {5211}, year = {2008}, } @inproceedings{3694, abstract = {Distributed Denial of Service (DDoS) attacks are today the most destabilizing factor in the global internet and there is a strong need for sophisticated solutions. We introduce a formal statistical framework and derive a Bayes optimal packet classifier from it. Our proposed practical algorithm "Adaptive History-Based IP Filtering" (AHIF) mitigates DDoS attacks near the victim and outperforms existing methods by at least 32% in terms of collateral damage. Furthermore, it adjusts to the strength of an ongoing attack and ensures availability of the attacked server. In contrast to other adaptive solutions, firewall rulesets used to resist an attack can be precalculated before an attack takes place. This ensures an immediate response in a DDoS emergency. For evaluation, simulated DDoS attacks and two real-world user traffic datasets are used.}, author = {Goldstein,Markus and Christoph Lampert and Reif,Matthias and Stahl,Armin and Breuel,Thomas M}, pages = {174 -- 179}, publisher = {IEEE}, title = {{Bayes optimal DDoS mitigation by adaptive history-based IP filtering}}, doi = {10.1109/ICN.2008.64}, year = {2008}, } @inproceedings{3706, abstract = {We present a new technique for structured prediction that works in a hybrid generative/discriminative way, using a one-class support vector machine to model the joint probability of (input, output)-pairs in a joint reproducing kernel Hilbert space. Compared to discriminative techniques, like conditional random fields or structured output SVMs?, the proposed method has the advantage that its training time depends only on the number of training examples, not on the size of the label space. Due to its generative aspect, it is also very tolerant against ambiguous, incomplete or incorrect labels. Experiments on realistic data show that our method works efficiently and robustly in situations that discriminative techniques have problems with or that are computationally infeasible for them.}, author = {Christoph Lampert and Blaschko,Matthew B}, pages = {1 -- 4}, publisher = {Curran Associates, Inc.}, title = {{Joint kernel support estimation for structured prediction}}, year = {2008}, } @inproceedings{3712, abstract = {We present a new method for spectral clustering with paired data based on kernel canonical correlation analysis, called correlational spectral clustering. Paired data are common in real world data sources, such as images with text captions. Traditional spectral clustering algorithms either assume that data can be represented by a single similarity measure, or by co-occurrence matrices that are then used in biclustering. In contrast, the proposed method uses separate similarity measures for each data representation, and allows for projection of previously unseen data that are only observed in one representation (e.g. images but not text). We show that this algorithm generalizes traditional spectral clustering algorithms and show consistent empirical improvement over spectral clustering on a variety of datasets of images with associated text.}, author = {Blaschko,Matthew B and Christoph Lampert}, pages = {1 -- 8}, publisher = {IEEE}, title = {{Correlational spectral clustering}}, doi = {10.1109/CVPR.2008.4587353}, year = {2008}, } @inbook{3726, abstract = {Single-molecule atomic force microscopy (AFM) provides novel ways to characterize the structure-function relationship of native membrane proteins. High-resolution AFM topographs allow observing the structure of single proteins at sub-nanometer resolution as well as their conformational changes, oligomeric state, molecular dynamics and assembly. We will review these feasibilities illustrating examples of membrane proteins in native and reconstituted membranes. Classification of individual topographs of single proteins allows understanding the principles of motions of their extrinsic domains, to learn about their local structural flexibilities and to find the entropy minima of certain conformations. Combined with the visualization of functionally related conformational changes these insights allow understanding why certain flexibilities are required for the protein to function and how structurally flexible regions allow certain conformational changes. Complementary to AFM imaging, single-molecule force spectroscopy (SMFS) experiments detect molecular interactions established within and between membrane proteins. The sensitivity of this method makes it possible to measure interactions that stabilize secondary structures such as transmembrane α-helices, polypeptide loops and segments within. Changes in temperature or protein-protein assembly do not change the locations of stable structural segments, but influence their stability established by collective molecular interactions. Such changes alter the probability of proteins to choose a certain unfolding pathway. Recent examples have elucidated unfolding and refolding pathways of membrane proteins as well as their energy landscapes.}, author = {Engel, Andreas and Harald Janovjak and Fotiadis, Dimtrios and Kedrov, Alexej and Cisneros, David and Mueller, Daniel J}, booktitle = {Single Molecules and Nanotechnology}, pages = {279 -- 311}, publisher = {Springer}, title = {{Single-molecule microscopy and force spectroscopy of membrane proteins}}, doi = {10.1007/978-3-540-73924-1_11}, volume = {12}, year = {2008}, } @article{3739, abstract = {Changes in a cell's external or internal conditions are usually reflected in the concentrations of the relevant transcription factors. These proteins in turn modulate the expression levels of the genes under their control and sometimes need to perform nontrivial computations that integrate several inputs and affect multiple genes. At the same time, the activities of the regulated genes would fluctuate even if the inputs were held fixed, as a consequence of the intrinsic noise in the system, and such noise must fundamentally limit the reliability of any genetic computation. Here we use information theory to formalize the notion of information transmission in simple genetic regulatory elements in the presence of physically realistic noise sources. The dependence of this "channel capacity" on noise parameters, cooperativity and cost of making signaling molecules is explored systematically. We find that, in the range of parameters probed by recent in vivo measurements, capacities higher than one bit should be achievable. It is of course generally accepted that gene regulatory elements must, in order to function properly, have a capacity of at least one bit. The central point of our analysis is the demonstration that simple physical models of noisy gene transcription, with realistic parameters, can indeed achieve this capacity: it was not self-evident that this should be so. We also demonstrate that capacities significantly greater than one bit are possible, so that transcriptional regulation need not be limited to simple "on-off" components. The question whether real systems actually exploit this richer possibility is beyond the scope of this investigation.}, author = {Gasper Tkacik and Callan,Curtis G and Bialek, William S}, journal = {Physical Review E Statistical Nonlinear and Soft Matter Physics}, number = {1}, publisher = {American Institute of Physics}, title = {{Information capacity of genetic regulatory elements}}, doi = {10.1103/PhysRevE.78.011910}, volume = {78}, year = {2008}, } @article{3740, abstract = {In the simplest view of transcriptional regulation, the expression of a gene is turned on or off by changes in the concentration of a transcription factor (TF). We use recent data on noise levels in gene expression to show that it should be possible to transmit much more than just one regulatory bit. Realizing this optimal information capacity would require that the dynamic range of TF concentrations used by the cell, the input/output relation of the regulatory module, and the noise in gene expression satisfy certain matching relations, which we derive. These results provide parameter-free, quantitative predictions connecting independently measurable quantities. Although we have considered only the simplified problem of a single gene responding to a single TF, we find that these predictions are in surprisingly good agreement with recent experiments on the Bicoid/Hunchback system in the early Drosophila embryo and that this system achieves approximately 90% of its theoretical maximum information transmission.}, author = {Gasper Tkacik and Callan,Curtis G and Bialek, William S}, journal = {PNAS}, number = {34}, pages = {12265 -- 12270}, publisher = {National Academy of Sciences}, title = {{Information flow and optimization in transcriptional regulation}}, doi = {10.1073/pnas.0806077105}, volume = {105}, year = {2008}, } @article{3744, abstract = {It is widely acknowledged that detailed timing of action potentials is used to encode information, for example, in auditory pathways; however, the computational tools required to analyze encoding through timing are still in their infancy. We present a simple example of encoding, based on a recent model of time-frequency analysis, in which units fire action potentials when a certain condition is met, but the timing of the action potential depends also on other features of the stimulus. We show that, as a result, spike-triggered averages are smoothed so much that they do not represent the true features of the encoding. Inspired by this example, we present a simple method, differential reverse correlations, that can separate an analysis of what causes a neuron to spike, and what controls its timing. We analyze with this method the leaky integrate-and-fire neuron and show the method accurately reconstructs the model's kernel.}, author = {Gasper Tkacik and Magnasco, Marcelo O}, journal = {Biosystems}, number = {1-2}, pages = {90 -- 100}, publisher = {Elsevier}, title = {{Decoding spike timing: The differential reverse-correlation method}}, doi = {10.1016/j.biosystems.2008.04.011}, volume = {93}, year = {2008}, } @article{3760, abstract = {We introduce a method for efficiently animating a wide range of deformable materials. We combine a high resolution surface mesh with a tetrahedral finite element simulator that makes use of frequent re-meshing. This combination allows for fast and detailed simulations of complex elastic and plastic behavior. We significantly expand the range of physical parameters that can be simulated with a single technique, and the results are free from common artifacts such as volume-loss, smoothing, popping, and the absence of thin features like strands and sheets. Our decision to couple a high resolution surface with low-resolution physics leads to efficient simulation and detailed surface features, and our approach to creating the tetrahedral mesh leads to an order-of-magnitude speedup over previous techniques in the time spent re-meshing. We compute masses, collisions, and surface tension forces on the scale of the fine mesh, which helps avoid visual artifacts due to the differing mesh resolutions. The result is a method that can simulate a large array of different material behaviors with high resolution features in a short amount of time.}, author = {Wojtan, Christopher J and Turk, Greg}, journal = {ACM Transactions on Graphics}, number = {3}, publisher = {ACM}, title = {{Fast viscoelastic behavior with thin features}}, doi = {10.1145/1360612.1360646}, volume = {27}, year = {2008}, } @article{3825, abstract = {Fast-spiking parvalbumin-expressing basket cells (BCs) represent a major type of inhibitory interneuron in the hippocampus. These cells inhibit principal cells in a temporally precise manner and are involved in the generation of network oscillations. Although BCs show a unique expression profile of Ca(2+)-permeable receptors, Ca(2+)-binding proteins and Ca(2+)-dependent signalling molecules, physiological Ca(2+) signalling in these interneurons has not been investigated. To study action potential (AP)-induced dendritic Ca(2+) influx and buffering, we combined whole-cell patch-clamp recordings with ratiometric Ca(2+) imaging from the proximal apical dendrites of rigorously identified BCs in acute slices, using the high-affinity Ca(2+) indicator fura-2 or the low-affinity dye fura-FF. Single APs evoked dendritic Ca(2+) transients with small amplitude. Bursts of APs evoked Ca(2+) transients with amplitudes that increased linearly with AP number. Analysis of Ca(2+) transients under steady-state conditions with different fura-2 concentrations and during loading with 200 microm fura-2 indicated that the endogenous Ca(2+)-binding ratio was approximately 200 (kappa(S) = 202 +/- 26 for the loading experiments). The peak amplitude of the Ca(2+) transients measured directly with 100 microm fura-FF was 39 nm AP(-1). At approximately 23 degrees C, the decay time constant of the Ca(2+) transients was 390 ms, corresponding to an extrusion rate of approximately 600 s(-1). At 34 degrees C, the decay time constant was 203 ms and the corresponding extrusion rate was approximately 1100 s(-1). At both temperatures, continuous theta-burst activity with three to five APs per theta cycle, as occurs in vivo during exploration, led to a moderate increase in the global Ca(2+) concentration that was proportional to AP number, whereas more intense stimulation was required to reach micromolar Ca(2+) concentrations and to shift Ca(2+) signalling into a non-linear regime. In conclusion, dentate gyrus BCs show a high endogenous Ca(2+)-binding ratio, a small AP-induced dendritic Ca(2+) influx, and a relatively slow Ca(2+) extrusion. These specific buffering properties of BCs will sharpen the time course of local Ca(2+) signals, while prolonging the decay of global Ca(2+) signals.}, author = {Aponte, Yexica and Bischofberger, Josef and Peter Jonas}, journal = {Journal of Physiology}, number = {8}, pages = {2061 -- 75}, publisher = {Wiley-Blackwell}, title = {{Efficient Ca(2+) buffering in fast-spiking basket cells of rat hippocampus}}, doi = {10.1113/jphysiol.2007.147298}, volume = {586}, year = {2008}, } @article{3822, abstract = {Dentate gyrus granule cells transmit action potentials (APs) along their unmyelinated mossy fibre axons to the CA3 region. Although the initiation and propagation of APs are fundamental steps during neural computation, little is known about the site of AP initiation and the speed of propagation in mossy fibre axons. To address these questions, we performed simultaneous somatic and axonal whole-cell recordings from granule cells in acute hippocampal slices of adult mice at approximately 23 degrees C. Injection of short current pulses or synaptic stimulation evoked axonal and somatic APs with similar amplitudes. By contrast, the time course was significantly different, as axonal APs had a higher maximal rate of rise (464 +/- 30 V s(-1) in the axon versus 297 +/- 12 V s(-1) in the soma, mean +/- s.e.m.). Furthermore, analysis of latencies between the axonal and somatic signals showed that APs were initiated in the proximal axon at approximately 20-30 mum distance from the soma, and propagated orthodromically with a velocity of 0.24 m s(-1). Qualitatively similar results were obtained at a recording temperature of approximately 34 degrees C. Modelling of AP propagation in detailed cable models of granule cells suggested that a approximately 4 times higher Na(+) channel density ( approximately 1000 pS mum(-2)) in the axon might account for both the higher rate of rise of axonal APs and the robust AP initiation in the proximal mossy fibre axon. This may be of critical importance to separate dendritic integration of thousands of synaptic inputs from the generation and transmission of a common AP output.}, author = {Schmidt-Hieber, Christoph and Peter Jonas and Bischofberger, Josef}, journal = {Journal of Physiology}, number = {7}, pages = {1849 -- 57}, publisher = {Wiley-Blackwell}, title = {{Action potential initiation and propagation in hippocampal mossy fibre axons}}, doi = {10.1113/jphysiol.2007.150151 }, volume = {586}, year = {2008}, } @article{3824, abstract = {It is generally thought that transmitter release at mammalian central synapses is triggered by Ca2+ microdomains, implying loose coupling between presynaptic Ca2+ channels and Ca2+ sensors of exocytosis. Here we show that Ca2+ channel subunit immunoreactivity is highly concentrated in the active zone of GABAergic presynaptic terminals of putative parvalbumin-containing basket cells in the hippocampus. Paired recording combined with presynaptic patch pipette perfusion revealed that GABA release at basket cell-granule cell synapses is sensitive to millimolar concentrations of the fast Ca2+ chelator BAPTA but insensitive to the slow Ca2+ chelator EGTA. These results show that Ca2+ source and Ca2+ sensor are tightly coupled at this synapse, with distances in the range of 10-20 nm. Models of Ca2+ inflow-exocytosis coupling further reveal that the tightness of coupling increases efficacy, speed, and temporal precision of transmitter release. Thus, tight coupling contributes to fast feedforward and feedback inhibition in the hippocampal network.}, author = {Bucurenciu, Iancu and Kulik, Ákos and Schwaller, Beat and Frotscher, Michael and Peter Jonas}, journal = {Neuron}, number = {4}, pages = {536 -- 45}, publisher = {Elsevier}, title = {{Nanodomain coupling between Ca(2+) channels and Ca2+ sensors promotes fast and efficient transmitter release at a cortical GABAergic synapse}}, doi = {10.1016/j.neuron.2007.12.026}, volume = {57}, year = {2008}, } @article{3823, abstract = {Two studies in this issue of Neuron (Kwon and Castillo and Rebola et al.) show that the mossy fiber-CA3 pyramidal neuron synapse, a hippocampal synapse well known for its presynaptic plasticity, exhibits a novel form of long-term potentiation of NMDAR-mediated currents, which is induced and expressed postsynaptically.}, author = {Kerr, Angharad M and Peter Jonas}, journal = {Neuron}, number = {1}, pages = {5 -- 7}, publisher = {Elsevier}, title = {{The two sides of hippocampal mossy fiber plasticity (Review)}}, doi = {10.1016/j.neuron.2007.12.015}, volume = {57}, year = {2008}, } @inproceedings{3880, abstract = {We consider imperfect-information parity games in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games, i.e., to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent perfect-information game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies. In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. We have implemented this algorithm as a prototype. To our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.}, author = {Berwanger, Dietmar and Krishnendu Chatterjee and Doyen, Laurent and Thomas Henzinger and Raje, Sangram}, pages = {325 -- 339}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Strategy construction for parity games with imperfect information}}, doi = {10.1007/978-3-540-85361-9}, volume = {5201}, year = {2008}, } @article{3903, abstract = {Background The invasive garden ant, Lasius neglectus, is the most recently detected pest ant and the first known invasive ant able to become established and thrive in the temperate regions of Eurasia. In this study, we aim to reconstruct the invasion history of this ant in Europe analysing 14 populations with three complementary approaches: genetic microsatellite analysis, chemical analysis of cuticular hydrocarbon profiles and behavioural observations of aggression behaviour. We evaluate the relative informative power of the three methodological approaches and estimate both the number of independent introduction events from a yet unknown native range somewhere in the Black Sea area, and the invasive potential of the existing introduced populations. Results Three clusters of genetically similar populations were detected, and all but one population had a similar chemical profile. Aggression between populations could be predicted from their genetic and chemical distance, and two major clusters of non-aggressive groups of populations were found. However, populations of L. neglectus did not separate into clear supercolonial associations, as is typical for other invasive ants. Conclusion The three methodological approaches gave consistent and complementary results. All joint evidence supports the inference that the 14 introduced populations of L. neglectus in Europe likely arose from only very few independent introductions from the native range, and that new infestations were typically started through introductions from other invasive populations. This indicates that existing introduced populations have a very high invasive potential when the ants are inadvertently spread by human transport. }, author = {Ugelvig, Line V and Drijfhout, Falko and Kronauer, Daniel and Boomsma, Jacobus and Pedersen, Jes and Cremer, Sylvia}, journal = {BMC Biology}, number = {11}, publisher = {BioMed Central}, title = {{The introduction history of invasive garden ants in Europe: integrating genetic, chemical and behavioural approaches}}, doi = {10.1186/1741-7007-6-11}, volume = {6}, year = {2008}, } @article{3905, abstract = {Winged and wingless males coexist in the ant Cardiocondyla obscurior. Wingless (“ergatoid”) males never leave their maternal colony and fight remorselessly among each other for the access to emerging females. The peaceful winged males disperse after about 10 days, but beforehand also mate in the nest. In the first 5 days of their life, winged males perform a chemical female mimicry that protects them against attack and even makes them sexually attractive to ergatoid males. When older, the chemical profile of winged males no longer matches that of virgin females; nevertheless, they are still tolerated, which so far has been puzzling. Contrasting this general pattern, we have identified a single aberrant colony in which all winged males were attacked and killed by the ergatoid males. A comparative analysis of the morphology and chemical profile of these untypical attacked winged males and the tolerated males from several normal colonies revealed that normal old males are still performing some chemical mimicry to the virgin queens, though less perfect than in their young ages. The anomalous attacked winged males, on the other hand, had a very different odour to the females. Our study thus exemplifies that the analysis of rare malfunctioning can add valuable insight on functioning under normal conditions and allows the conclusion that older winged males from normal colonies of the ant C. obscurior are guarded through an imperfect chemical female mimicry, still close enough to protect against attacks by the wingless fighters yet dissimilar enough not to elicit their sexual interest.}, author = {Cremer, Sylvia and D'Ettorre, Patrizia and Drijfhout, Falko and Sledge, Matthew and Turillazzi, Stefano and Heinze, Jürgen}, journal = {Naturwissenschaften}, number = {11}, pages = {1101 -- 1105}, publisher = {Springer}, title = {{Imperfect chemical female mimicry in males of the ant Cardiocondyla obscurior}}, doi = {10.1007/s00114-008-0430-8}, volume = {95}, year = {2008}, } @article{3907, abstract = {Wingless males of the ant genus Cardiocondyla engage in fatal fighting for access to female sexual nestmates. Older, heavily sclerotized males are usually capable of eliminating all younger rivals, whose cuticle is still soft. In Cardiocondyla sp. A, this type of local mate competition (LMC) has turned the standard pattern of brood production of social insects upside down, in that mother queens in multi-queen colonies produce extremely long-lived sons very early in the life cycle of the colony. Here, we investigated the emergence pattern of sexuals in two species with LMC, in which males are much less long-lived. Queens of Cardiocondyla obscurior and Cardiocondyla minutior reared their first sons significantly earlier in multi-queen than in single-queen societies. In addition, first female sexuals also emerged earlier in multi-queen colonies, so that early males had mating opportunities. Hence, the timing of sexual production appears to be well predicted by evolutionary theory, in particular by local mate and queen–queen competition. }, author = {Suefuji, Masaki and Cremer, Sylvia and Oettler, Jan and Heinze, Jürgen}, journal = {Biology Letters}, number = {6}, pages = {670 -- 673}, publisher = {Royal Society, The}, title = {{Queen number influences the timing of the sexual production in colonies of Cardiocondyla ants}}, doi = {10.1098/rsbl.2008.0355}, volume = {4}, year = {2008}, } @article{3906, author = {Cremer, Sylvia and Ugelvig, Line V and Drijfhout, Falko and Schlick Steiner, Birgit and Steiner, Florian and Seifert, Bernhard and Hughes, David and Schulz, Andreas and Petersen, Klaus and Konrad, Heino and Stauffer, Christian and Kiran, Kadri and Espadaler, Xavier and D'Ettorre, Patrizia and Aktaç, Nihat and Eilenberg, Jørgen and Jones, Graeme and Nash, David and Pedersen, Jes and Boomsma, Jacobus}, journal = {PLoS One}, number = {12}, publisher = {Public Library of Science}, title = {{The evolution of invasiveness in garden ants}}, doi = {10.1371/journal.pone.0003838}, volume = {3}, year = {2008}, } @article{3939, abstract = {The priming of a T cell results from its physical interaction with a dendritic cell (DC) that presents the cognate antigenic peptide. The success rate of such interactions is extremely low, because the precursor frequency of a naive T cell recognizing a specific antigen is in the range of 1:10(5)-10(6). To make this principle practicable, encounter frequencies between DCs and T cells are maximized within lymph nodes (LNs) that are compact immunological projections of the peripheral tissue they drain. But LNs are more than passive meeting places for DCs that immigrated from the tissue and lymphocytes that recirculated via the blood. The microanatomy of the LN stroma actively organizes the cellular encounters by providing preformed migration tracks that create dynamic but highly ordered movement patterns. LN architecture further acts as a sophisticated filtration system that sieves the incoming interstitial fluid at different levels and guarantees that immunologically relevant antigens are loaded on DCs or B cells while inert substances are channeled back into the blood circulation. This review focuses on the non-hematopoietic infrastructure of the lymph node. We describe the association between fibroblastic reticular cell, conduit, DC, and T cell as the essential functional unit of the T-cell cortex.}, author = {Lämmermann, Tim and Sixt, Michael K}, journal = {Immunological Reviews}, number = {1}, pages = {26 -- 43}, publisher = {Wiley-Blackwell}, title = {{The microanatomy of T-cell responses}}, doi = {10.1111/j.1600-065X.2008.00592.x}, volume = {221}, year = {2008}, } @article{3940, abstract = {Until recently little information was available on the molecular details of the extracellular matrix (ECM) of secondary lymphoid tissues. There is now growing evidence that these ECMs are unique structures, combining characteristics of basement membranes and interstitial or fibrillar matrices, resulting in scaffolds that are strong and highly flexible and, in certain secondary lymphoid compartments, also forming conduit networks for rapid fluid transport. This review will address the structural characteristics of the ECM of the murine spleen and its potential role as an organizer of immune cell compartments, with reference to the lymph node where relevant.}, author = {Lokmic, Zerina and Lämmermann, Tim and Michael Sixt and Cardell, Susanna and Hallmann, Rupert and Sorokin, Lydia}, journal = {Seminars in Immunology}, number = {1}, pages = {4 -- 13}, publisher = {Academic Press}, title = {{The extracellular matrix of the spleen as a potential organizer of immune cell compartments}}, doi = {10.1016/j.smim.2007.12.009}, volume = {20}, year = {2008}, } @article{3970, abstract = {While genome-wide gene expression data are generated at an increasing rate, the repertoire of approaches for pattern discovery in these data is still limited. Identifying subtle patterns of interest in large amounts of data (tens of thousands of profiles) associated with a certain level of noise remains a challenge. A microarray time series was recently generated to study the transcriptional program of the mouse segmentation clock, a biological oscillator associated with the periodic formation of the segments of the body axis. A method related to Fourier analysis, the Lomb-Scargle periodogram, was used to detect periodic profiles in the dataset, leading to the identification of a novel set of cyclic genes associated with the segmentation clock. Here, we applied to the same microarray time series dataset four distinct mathematical methods to identify significant patterns in gene expression profiles. These methods are called: Phase consistency, Address reduction, Cyclohedron test and Stable persistence, and are based on different conceptual frameworks that are either hypothesis- or data-driven. Some of the methods, unlike Fourier transforms, are not dependent on the assumption of periodicity of the pattern of interest. Remarkably, these methods identified blindly the expression profiles of known cyclic genes as the most significant patterns in the dataset. Many candidate genes predicted by more than one approach appeared to be true positive cyclic genes and will be of particular interest for future research. In addition, these methods predicted novel candidate cyclic genes that were consistent with previous biological knowledge and experimental validation in mouse embryos. Our results demonstrate the utility of these novel pattern detection strategies, notably for detection of periodic profiles, and suggest that combining several distinct mathematical approaches to analyze microarray datasets is a valuable strategy for identifying genes that exhibit novel, interesting transcriptional patterns.}, author = {Dequéant, Mary-Lee and Ahnert, Sebastian and Herbert Edelsbrunner and Fink, Thomas M and Glynn, Earl F and Hattem, Gaye and Kudlicki, Andrzej and Mileyko, Yuriy and Morton, Jason and Mushegian, Arcady R and Pachter, Lior and Rowicka, Maga and Shiu, Anne and Sturmfels, Bernd and Pourquie, Olivier}, journal = {PLoS One}, number = {8}, publisher = {Public Library of Science}, title = {{Comparison of pattern detection methods in microarray time series of the segmentation clock}}, doi = {10.1371/journal.pone.0002856}, volume = {3}, year = {2008}, } @article{3971, abstract = {The Reeb graph is a useful tool in visualizing real-valued data obtained from computational simulations of physical processes. We characterize the evolution of the Reeb graph of a time-varying continuous function defined in three-dimensional space. We show how to maintain the Reeb graph over time and compress the entire sequence of Reeb graphs into a single, partially persistent data structure, and augment this data structure with Betti numbers to describe the topology of level sets and with path seeds to assist in the fast extraction of level sets for visualization.}, author = {Herbert Edelsbrunner and Harer, John and Mascarenhas, Ajith and Pascucci, Valerio and Snoeyink, Jack}, journal = {Computational Geometry: Theory and Applications}, number = {3}, pages = {149 -- 166}, publisher = {Elsevier}, title = {{Time-varying Reeb graphs for continuous space-time data}}, doi = {10.1016/j.comgeo.2007.11.001}, volume = {41}, year = {2008}, } @inbook{3969, abstract = {Persistent homology is an algebraic tool for measuring topological features of shapes and functions. It casts the multi-scale organization we frequently observe in nature into a mathematical formalism. Here we give a record of the short history of persistent homology and present its basic concepts. Besides the mathematics we focus on algorithms and mention the various connections to applications, including to biomolecules, biological networks, data analysis, and geometric modeling.}, author = {Herbert Edelsbrunner and Harer, John}, booktitle = {Surveys on Discrete and Computational Geometry: Twenty Years Later}, pages = {257 -- 282}, publisher = {American Mathematical Society}, title = {{Persistent homology - a survey}}, year = {2008}, } @article{4141, abstract = {The zyxin-related LPP protein is localized at focal adhesions and cell-cell contacts and is involved in the regulation of smooth muscle cell migration. A known interaction partner of LPP in human is the tumor suppressor protein SCRIB. Knocking down scrib expression c uring zebrafish embryonic development results in defects of convergence and extension (C&E) movements, which occur during gastrulation and mediate elongation of the anterior-posterior body axis. Mediolateral cell polarization underlying C&E is regulated by a noncanonical Writ signaling pathway constituting the vertebrate planar cell polarity (PCP) pathway. Here, we investigated the role of Lpp during early zebrafish development. We show that morpholino knockdown of Ipp results in defects of C&E, phenocopying noncanonical Wnt signaling mutants. Time-lapse analysis associates the defective dorsal convergence movements with a reduced ability to migrate along straight paths. In addition, expression of Lpp is significantly reduced in Wnt11 morphants and in embryos overexpressing Wnt11 or a dominant-negative form of Rho kinase 2, which is a downstream effector of Wnt11, Suggesting that Lpp expression is dependent on noncanonical Wnt signaling. Finally, we demonstrate that Lpp interacts with the PCP protein Scrib in zebrafish, and that Lpp and Scrib cooperate for the mediation of C&E. (C) 2008 Elsevier Inc. All rights reserved.}, author = {Vervenne, Hilke and Crombez, Koen and Lambaerts, Kathleen and Carvalho, Lara and Köppen, Mathias and Heisenberg, Carl-Philipp J and Van De Ven, Wim and Petit, Marleen}, journal = {Developmental Biology}, number = {1}, pages = {267 -- 277}, publisher = {Elsevier}, title = {{Lpp is involved in Wnt/PCP signaling and acts together with Scrib to mediate convergence and extension movements during zebrafish gastrulation}}, doi = {10.1016/j.ydbio.2008.05.529}, volume = {320}, year = {2008}, } @article{4161, abstract = {Handedness of the vertebrate body plan critically depends on transient embryonic structures/ organs that generate cilia-dependent leftward fluid flow within constrained extracellular environments. Although the function of ciliated organs in laterality determination has been extensively studied, how they are formed during embryogenesis is still poorly understood. Here we show that Kupffer's vesicle (KV), the zebrafish organ of laterality, arises from a surface epithelium previously thought to adopt exclusively extra-embryonic fates. Live multi-photon confocal imaging reveals that surface epithelial cells undergo Nodal/TGF beta signalling-dependent ingression at the dorsal germ ring margin prior to gastrulation, to give rise to dorsal forerunner cells (DFCs), the precursors of KV. DFCs then migrate attached to the overlying surface epithelium and rearrange into rosette-like epithelial structures at the end of gastrulation. During early somitogenesis, these epithelial rosettes coalesce into a single rosette that differentiates into the KV with a ciliated lumen at its apical centre. Our results provide novel insights into the morphogenetic transformations that shape the laterality organ in zebrafish and suggest a conserved progenitor role of the surface epithelium during laterality organ formation in vertebrates.}, author = {Oteíza, Pablo and Köppen, Mathias and Concha, Miguel and Heisenberg, Carl-Philipp J}, journal = {Development}, number = {16}, pages = {2807 -- 2813}, publisher = {Company of Biologists}, title = {{Origin and shaping of the laterality organ in zebrafish}}, doi = {10.1242/dev.022228}, volume = {135}, year = {2008}, } @article{4190, abstract = {During vertebrate gastrulation, cells forming the prechordal plate undergo directed migration as a cohesive cluster. Recent studies revealed that E-cadherin-mediated coherence between these cells plays an important role in effective anterior migration, and that platelet-derived growth factor (Pdgf) appears to act as a guidance cue in this process. However, the mechanisms underlying this process at the individual cell level remain poorly understood. We have identified miles apart (mil) as a suppressor of defective anterior migration of the prospective prechordal plate in silberblick (slb)/wnt11 mutant embryos, in which E-cadherin-mediated coherence of cell movement is reduced. mil encodes Edg5, a sphingosine-1-phosphate (S1P) receptor belonging to a family of five G-protein-coupled receptors (S1PRs). S1P is a lipid signalling molecule that has been implicated in regulating cytoskeletal rearrangements, cell motility and cell adhesion in a variety of cell types. We examined the roles of Mil in anterior migration of prechordal plate progenitor cells and found that, in slb embryos injected with mil-MO, cells migrate with increased motility but decreased directionality, without restoring the coherence of cell migration. This indicates that prechordal plate progenitor cells can migrate effectively as individuals, as well as in a coherent cluster of cells. Moreover, we demonstrate that Mil regulates cell motility and polarisation through Pdgf and its intracellular effecter PI3K, but modulates cell coherence independently of the Pdgf/PI3K pathway, thus co-ordinating cell motility and coherence. These results suggest that the net migration of prechordal plate progenitors is determined by different parameters, including motility, persistence and coherence.}, author = {Kai, Masatake and Heisenberg, Carl-Philipp J and Tada, Masazumi}, journal = {Development}, number = {18}, pages = {3043 -- 3051}, publisher = {Company of Biologists}, title = {{Sphingosine-1-phosphate receptors regulate individual cell behaviours underlying the directed migration of prechordal plate progenitor cells during zebrafish gastrulation}}, doi = {10.1242/dev.020396}, volume = {135}, year = {2008}, } @inproceedings{4384, abstract = {Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom. Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.}, author = {Guerraoui, Rachid and Thomas Henzinger and Jobstmann, Barbara and Vasu Singh}, pages = {372 -- 382}, publisher = {ACM}, title = {{Model checking transactional memories}}, doi = {10.1145/1375581.1375626}, year = {2008}, } @inproceedings{4386, abstract = {We introduce the notion of permissiveness in transactional memories (TM). Intuitively, a TM is permissive if it never aborts a transaction when it need not. More specifically, a TM is permissive with respect to a safety property p if the TM accepts every history that satisfies p. Permissiveness, like safety and liveness, can be used as a metric to compare TMs. We illustrate that it is impractical to achieve permissiveness deterministically, and then show how randomization can be used to achieve permissiveness efficiently. We introduce Adaptive Validation STM (AVSTM), which is probabilistically permissive with respect to opacity; that is, every opaque history is accepted by AVSTM with positive probability. Moreover, AVSTM guarantees lock freedom. Owing to its permissiveness, AVSTM outperforms other STMs by up to 40% in read dominated workloads in high contention scenarios. But, in low contention scenarios, the book-keeping done by AVSTM to achieve permissiveness makes AVSTM, on average, 20-30% worse than existing STMs.}, author = {Guerraoui, Rachid and Thomas Henzinger and Vasu Singh}, pages = {305 -- 319}, publisher = {Springer}, title = {{Permissiveness in transactional memories}}, doi = {10.1007/978-3-540-87779-0_21}, volume = {5218}, year = {2008}, } @inproceedings{4387, abstract = {Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first deterministic specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a complete verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is nondeterministic and establishes correctness for all possible contention management schemes.}, author = {Guerraoui, Rachid and Thomas Henzinger and Vasu Singh}, pages = {21 -- 35}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Completeness and nondeterminism in model checking transactional memories}}, doi = {10.1007/978-3-540-85361-9_6}, volume = {5201}, year = {2008}, } @inproceedings{4397, author = {Beyer, Dirk and Damien Zufferey and Majumdar, Ritankar S}, pages = {304 -- 308}, publisher = {Springer}, title = {{CSIsat: Interpolation for LA+EUF}}, year = {2008}, } @inproceedings{4400, author = {Aviv,Adam J. and Pavol Cerny and Clark,Sandy and Cronin,Eric and Shah,Gaurav and Sherr,Micah and Blaze,Matt}, publisher = {USENIX}, title = {{Security Evaluation of ES&S Voting Machines and Election Management System}}, doi = {1545}, year = {2008}, } @phdthesis{4409, abstract = {Models of timed systems must incorporate not only the sequence of system events, but the timings of these events as well to capture the real-time aspects of physical systems. Timed automata are models of real-time systems in which states consist of discrete locations and values for real-time clocks. The presence of real-time clocks leads to an uncountable state space. This thesis studies verification problems on timed automata in a game theoretic framework. For untimed systems, two systems are close if every sequence of events of one system is also observable in the second system. For timed systems, the difference in timings of the two corresponding sequences is also of importance. We propose the notion of bisimulation distance which quantifies timing differences; if the bisimulation distance between two systems is epsilon, then (a) every sequence of events of one system has a corresponding matching sequence in the other, and (b) the timings of matching events in between the two corresponding traces do not differ by more than epsilon. We show that we can compute the bisimulation distance between two timed automata to within any desired degree of accuracy. We also show that the timed verification logic TCTL is robust with respect to our notion of quantitative bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula. Timed games are used for distinguishing between the actions of several agents, typically a controller and an environment. The controller must achieve its objective against all possible choices of the environment. The modeling of the passage of time leads to the presence of zeno executions, and corresponding unrealizable strategies of the controller which may achieve objectives by blocking time. We disallow such unreasonable strategies by restricting all agents to use only receptive strategies --strategies which while not being required to ensure time divergence by any agent, are such that no agent is responsible for blocking time. Time divergence is guaranteed when all players use receptive strategies. We show that timed automaton games with receptive strategies can be solved by a reduction to finite state turn based game graphs. We define the logic timed alternating-time temporal logic for verification of timed automaton games and show that the logic can be model checked in EXPTIME. We also show that the minimum time required by an agent to reach a desired location, and the maximum time an agent can stay safe within a set of locations, against all possible actions of its adversaries are both computable. We next study the memory requirements of winning strategies for timed automaton games. We prove that finite memory strategies suffice for safety objectives, and that winning strategies for reachability objectives may require infinite memory in general. We introduce randomized strategies in which an agent can propose a probabilistic distribution of moves and show that finite memory randomized strategies suffice for all omega-regular objectives. We also show that while randomization helps in simplifying winning strategies, and thus allows the construction of simpler controllers, it does not help a player in winning at more states, and thus does not allow the construction of more powerful controllers. Finally we study robust winning strategies in timed games. In a physical system, a controller may propose an action together with a time delay, but the action cannot be assumed to be executed at the exact proposed time delay. We present robust strategies which incorporate such jitters and show that the set of states from which an agent can win robustly is computable.}, author = {Prabhu, Vinayak}, pages = {1 -- 137}, publisher = {University of California, Berkeley}, title = {{Games for the verification of timed systems}}, year = {2008}, } @phdthesis{4415, abstract = {Many computing applications, especially those in safety critical embedded systems, require highly predictable timing properties. However, time is often not present in the prevailing computing and networking abstractions. In fact, most advances in computer architecture, software, and networking favor average-case performance over timing predictability. This thesis studies several methods for the design of concurrent and/or distributed embedded systems with precise timing guarantees. The focus is on flexible and compositional methods for programming and verification of the timing properties. The presented methods together with related formalisms cover two levels of design: (1) Programming language/model level. We propose the distributed variant of Giotto, a coordination programming language with an explicit temporal semantics—the logical execution time (LET) semantics. The LET of a task is an interval of time that specifies the time instants at which task inputs and outputs become available (task release and termination instants). The LET of a task is always non-zero. This allows us to communicate values across the network without changing the timing information of the task, and without introducing nondeterminism. We show how this methodology supports distributed code generation for distributed real-time systems. The method gives up some performance in favor of composability and predictability. We characterize the tradeoff by comparing the LET semantics with the semantics used in Simulink. (2) Abstract task graph level. We study interface-based design and verification of applications represented with task graphs. We consider task sequence graphs with general event models, and cyclic graphs with periodic event models with jitter and phase. Here an interface of a component exposes time and resource constraints of the component. Together with interfaces we formally define interface composition operations and the refinement relation. For efficient and flexible composability checking two properties are important: incremental design and independent refinement. According to the incremental design property the composition of interfaces can be performed in any order, even if interfaces for some components are not known. The refinement relation is defined such that in a design we can always substitute a refined interface for an abstract one. We show that the framework supports independent refinement, i.e., the refinement relation is preserved under composition operations.}, author = {Matic, Slobodan}, pages = {1 -- 148}, publisher = {University of California, Berkeley}, title = {{Compositionality in deterministic real-time embedded systems}}, year = {2008}, } @inproceedings{4452, abstract = {We describe Valigator, a software tool for imperative program verification that efficiently combines symbolic computation and automated reasoning in a uniform framework. The system offers support for automatically generating and proving verification conditions and, most importantly, for automatically inferring loop invariants and bound assertions by means of symbolic summation, Gröbner basis computation, and quantifier elimination. We present general principles of the implementation and illustrate them on examples.}, author = {Thomas Henzinger and Hottelier, Thibaud and Kovács, Laura}, pages = {333 -- 342}, publisher = {Springer}, title = {{Valigator: A verification tool with bound and invariant generation}}, doi = {10.1007/978-3-540-89439-1_24}, volume = {5330}, year = {2008}, } @article{4509, abstract = {I discuss two main challenges in embedded systems design: the challenge to build predictable systems, and that to build robust systems. I suggest how predictability can be formalized as a form of determinism, and robustness as a form of continuity.}, author = {Thomas Henzinger}, journal = {Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences}, number = {1881}, pages = {3727 -- 3736}, publisher = {Royal Society of London}, title = {{Two challenges in embedded systems design: Predictability and robustness}}, doi = {10.1098/rsta.2008.0141}, volume = {366}, year = {2008}, } @phdthesis{4524, abstract = {Complex requirements, time-to-market pressure and regulatory constraints have made the designing of embedded systems extremely challenging. This is evident by the increase in effort and expenditure for design of safety-driven real-time control-dominated applications like automotive and avionic controllers. Design processes are often challenged by lack of proper programming tools for specifying and verifying critical requirements (e.g. timing and reliability) of such applications. Platform based design, an approach for designing embedded systems, addresses the above concerns by separating requirement from architecture. The requirement specifies the intended behavior of an application while the architecture specifies the guarantees (e.g. execution speed, failure rate etc). An implementation, a mapping of the requirement on the architecture, is then analyzed for correctness. The orthogonalization of concerns makes the specification and analyses simpler. An effective use of such design methodology has been proposed in Logical Execution Time (LET) model of real-time tasks. The model separates the timing requirements (specified by release and termination instances of a task) from the architecture guarantees (specified by worst-case execution time of the task). This dissertation proposes a coordination language, Hierarchical Timing Language (HTL), that captures the timing and reliability requirements of real-time applications. An implementation of the program on an architecture is then analyzed to check whether desired timing and reliability requirements are met or not. The core framework extends the LET model by accounting for reliability and refinement. The reliability model separates the reliability requirements of tasks from the reliability guarantees of the architecture. The requirement expresses the desired long-term reliability while the architecture provides a short-term reliability guarantee (e.g. failure rate for each iteration). The analysis checks if the short-term guarantee ensures the desired long-term reliability. The refinement model allows replacing a task by another task during program execution. Refinement preserves schedulability and reliability, i.e., if a refined task is schedulable and reliable for an implementation, then the refining task is also schedulable and reliable for the implementation. Refinement helps in concise specification without overloading analysis. The work presents the formal model, the analyses (both with and without refinement), and a compiler for HTL programs. The compiler checks composition and refinement constraints, performs schedulability and reliability analyses, and generates code for implementation of an HTL program on a virtual machine. Three real-time controllers, one each from automatic control, automotive control and avionic control, are used to illustrate the steps in modeling and analyzing HTL programs.}, author = {Ghosal, Arkadeb}, pages = {1 -- 210}, publisher = {University of California, Berkeley}, title = {{A hierarchical coordination language for reliable real-time tasks}}, year = {2008}, } @inproceedings{4521, abstract = {The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, the current focus of liveness verification has been almost exclusively on the search for termination proofs. A counterexample to termination is an infinite programexecution. In this paper, we propose a method to search for such counterexamples. The search proceeds in two phases. We first dynamically enumerate lasso-shaped candidate paths for counterexamples, and then statically prove their feasibility. We illustrate the utility of our nontermination prover, called TNT, on several nontrivial examples, some of which require bit-level reasoning about integer representations.}, author = {Ashutosh Gupta and Thomas Henzinger and Majumdar, Ritankar S and Rybalchenko, Andrey and Xu, Ru-Gang}, pages = {147 -- 158}, publisher = {ACM}, title = {{Proving non-termination}}, doi = {10.1145/1328438.1328459}, year = {2008}, } @inproceedings{4527, abstract = {We introduce bounded asynchrony, a notion of concurrency tailored to the modeling of biological cell-cell interactions. Bounded asynchrony is the result of a scheduler that bounds the number of steps that one process gets ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the experimental observations made about certain cell-cell interactions: its constrained nondeterminism captures the variability observed in cells that, although equally potent, assume distinct fates. Real-life cells are not “scheduled”, but we show that distributed real-time behavior can lead to component interactions that are observationally equivalent to bounded asynchrony; this provides a possible mechanistic explanation for the phenomena observed during cell fate specification. We use model checking to determine cell fates. The nondeterminism of bounded asynchrony causes state explosion during model checking, but partial-order methods are not directly applicable. We present a new algorithm that reduces the number of states that need to be explored: our optimization takes advantage of the bounded-asynchronous progress and the spatially local interactions of components that model cells. We compare our own communication-based reduction with partial-order reduction (on a restricted form of bounded asynchrony) and experiments illustrate that our algorithm leads to significant savings.}, author = {Fisher, Jasmin and Thomas Henzinger and Maria Mateescu and Piterman, Nir}, pages = {17 -- 32}, publisher = {Springer}, title = {{Bounded asynchrony: Concurrency for modeling cell-cell interactions}}, doi = {10.1007/978-3-540-68413-8_2}, volume = {5054}, year = {2008}, } @article{4532, abstract = {We consider the equivalence problem for labeled Markov chains (LMCs), where each state is labeled with an observation. Two LMCs are equivalent if every finite sequence of observations has the same probability of occurrence in the two LMCs. We show that equivalence can be decided in polynomial time, using a reduction to the equivalence problem for probabilistic automata, which is known to be solvable in polynomial time. We provide an alternative algorithm to solve the equivalence problem, which is based on a new definition of bisimulation for probabilistic automata. We also extend the technique to decide the equivalence of weighted probabilistic automata.}, author = {Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François}, journal = {International Journal of Foundations of Computer Science}, number = {3}, pages = {549 -- 563}, publisher = {World Scientific Publishing}, title = {{Equivalence of labeled Markov chains}}, doi = {10.1142/S0129054108005814 }, volume = {19}, year = {2008}, } @inproceedings{4533, abstract = {Interface theories have been proposed to 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, maintaining compatibility. We show that these interface theories provide no formal support for component reuse, meaning that the same component cannot be used to implement several different interfaces in a design. We add a new operation to interface theories in order to support such reuse. For example, different interfaces for the same component may refer to different aspects such as functionality, timing, and power consumption. We give both stateless and stateful examples for interface theories with component reuse. To illustrate component reuse in interface-based design, we show how the stateful theory provides a natural framework for specifying and refining PCI bus clients.}, author = {Doyen, Laurent and Thomas Henzinger and Jobstmann, Barbara and Tatjana Petrov}, pages = {79 -- 88}, publisher = {ACM}, title = {{Interface theories with component reuse}}, doi = {10.1145/1450058.1450070}, year = {2008}, } @article{4534, abstract = {A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives, and mean-payoff (or limit-average) objectives. These games lie in NP ∩ coNP. We present a polynomial-time Turing reduction of stochastic parity games to stochastic mean-payoff games.}, author = {Krishnendu Chatterjee and Thomas Henzinger}, journal = {Information Processing Letters}, number = {1}, pages = {1 -- 7}, publisher = {Elsevier}, title = {{Reduction of stochastic parity to stochastic mean-payoff games}}, doi = {10.1016/j.ipl.2007.08.035}, volume = {106}, year = {2008}, } @inproceedings{4546, abstract = {We propose the notion of logical reliability for real-time program tasks that interact through periodically updated program variables. We describe a reliability analysis that checks if the given short-term (e.g., single-period) reliability of a program variable update in an implementation is sufficient to meet the logical reliability requirement (of the program variable) in the long run. We then present a notion of design by refinement where a task can be refined by another task that writes to program variables with less logical reliability. The resulting analysis can be combined with an incremental schedulability analysis for interacting real-time tasks proposed earlier for the Hierarchical Timing Language (HTL), a coordination language for distributed real-time systems. We implemented a logical-reliability-enhanced prototype of the compiler and runtime infrastructure for HTL.}, author = {Krishnendu Chatterjee and Ghosal, Arkadeb and Thomas Henzinger and Iercan, Daniel and Kirsch, Christoph M and Pinello, Claudio and Sangiovanni-Vincentelli, Alberto}, pages = {909 -- 914}, publisher = {IEEE}, title = {{Logical reliability of interacting real-time tasks}}, doi = {10.1145/1403375.1403595}, year = {2008}, }