@inproceedings{3361, abstract = {In this paper, we investigate the computational complexity of quantitative information flow (QIF) problems. Information-theoretic quantitative relaxations of noninterference (based on Shannon entropy)have been introduced to enable more fine-grained reasoning about programs in situations where limited information flow is acceptable. The QIF bounding problem asks whether the information flow in a given program is bounded by a constant $d$. Our first result is that the QIF bounding problem is PSPACE-complete. The QIF memoryless synthesis problem asks whether it is possible to resolve nondeterministic choices in a given partial program in such a way that in the resulting deterministic program, the quantitative information flow is bounded by a given constant $d$. Our second result is that the QIF memoryless synthesis problem is also EXPTIME-complete. The QIF memoryless synthesis problem generalizes to QIF general synthesis problem which does not impose the memoryless requirement (that is, by allowing the synthesized program to have more variables then the original partial program). Our third result is that the QIF general synthesis problem is EXPTIME-hard.}, author = {Cerny, Pavol and Chatterjee, Krishnendu and Henzinger, Thomas A}, location = {Cernay-la-Ville, France}, pages = {205 -- 217}, publisher = {IEEE}, title = {{The complexity of quantitative information flow problems}}, doi = {10.1109/CSF.2011.21}, year = {2011}, } @inproceedings{3358, abstract = {The static scheduling problem often arises as a fundamental problem in real-time systems and grid computing. We consider the problem of statically scheduling a large job expressed as a task graph on a large number of computing nodes, such as a data center. This paper solves the large-scale static scheduling problem using abstraction refinement, a technique commonly used in formal verification to efficiently solve computationally hard problems. A scheduler based on abstraction refinement first attempts to solve the scheduling problem with abstract representations of the job and the computing resources. As abstract representations are generally small, the scheduling can be done reasonably fast. If the obtained schedule does not meet specified quality conditions (like data center utilization or schedule makespan) then the scheduler refines the job and data center abstractions and, again solves the scheduling problem. We develop different schedulers based on abstraction refinement. We implemented these schedulers and used them to schedule task graphs from various computing domains on simulated data centers with realistic topologies. We compared the speed of scheduling and the quality of the produced schedules with our abstraction refinement schedulers against a baseline scheduler that does not use any abstraction. We conclude that abstraction refinement techniques give a significant speed-up compared to traditional static scheduling heuristics, at a reasonable cost in the quality of the produced schedules. We further used our static schedulers in an actual system that we deployed on Amazon EC2 and compared it against the Hadoop dynamic scheduler for large MapReduce jobs. Our experiments indicate that there is great potential for static scheduling techniques.}, author = {Henzinger, Thomas A and Singh, Vasu and Wies, Thomas and Zufferey, Damien}, location = {Salzburg, Austria}, pages = {329 -- 342}, publisher = {ACM}, title = {{Scheduling large jobs by abstraction refinement}}, doi = {10.1145/1966445.1966476}, year = {2011}, } @inproceedings{3359, abstract = {Motivated by improvements in constraint-solving technology and by the increase of routinely available computational power, partial-program synthesis is emerging as an effective approach for increasing programmer productivity. The goal of the approach is to allow the programmer to specify a part of her intent imperatively (that is, give a partial program) and a part of her intent declaratively, by specifying which conditions need to be achieved or maintained. The task of the synthesizer is to construct a program that satisfies the specification. As an example, consider a partial program where threads access shared data without using any synchronization mechanism, and a declarative specification that excludes data races and deadlocks. The task of the synthesizer is then to place locks into the program code in order for the program to meet the specification. In this paper, we argue that quantitative objectives are needed in partial-program synthesis in order to produce higher-quality programs, while enabling simpler specifications. Returning to the example, the synthesizer could construct a naive solution that uses one global lock for shared data. This can be prevented either by constraining the solution space further (which is error-prone and partly defeats the point of synthesis), or by optimizing a quantitative objective that models performance. Other quantitative notions useful in synthesis include fault tolerance, robustness, resource (memory, power) consumption, and information flow.}, author = {Cerny, Pavol and Henzinger, Thomas A}, location = {Taipei; Taiwan}, pages = {149 -- 154}, publisher = {ACM}, title = {{From boolean to quantitative synthesis}}, doi = {10.1145/2038642.2038666}, year = {2011}, } @inproceedings{3357, abstract = {We consider two-player graph games whose objectives are request-response condition, i.e conjunctions of conditions of the form "if a state with property Rq is visited, then later a state with property Rp is visited". The winner of such games can be decided in EXPTIME and the problem is known to be NP-hard. In this paper, we close this gap by showing that this problem is, in fact, EXPTIME-complete. We show that the problem becomes PSPACE-complete if we only consider games played on DAGs, and NP-complete or PTIME-complete if there is only one player (depending on whether he wants to enforce or spoil the request-response condition). We also present near-optimal bounds on the memory needed to design winning strategies for each player, in each case.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Horn, Florian}, editor = {Dediu, Adrian-Horia and Inenaga, Shunsuke and Martín-Vide, Carlos}, location = {Tarragona, Spain}, pages = {227 -- 237}, publisher = {Springer}, title = {{The complexity of request-response games}}, doi = {10.1007/978-3-642-21254-3_17}, volume = {6638}, year = {2011}, } @article{336, abstract = {The growth kinetics of colloidal Bi2S3 nanorods was investigated. After nucleation, the length distribution of the growing Bi 2S3 nanorods narrows with the reaction time until a bimodal length distribution appears. From this critical reaction time on, the smallest nanorods of the ensemble dissolve, feeding with monomer the growth of the largest ones. A comprehensive characterization of the size-distribution evolution of Bi2S3 nanorods is used here to illustrate the dependences of the anisotropic growth rates of cylindrical nanoparticles on the nanoparticle dimensions and the monomer concentration in solution. With this goal in mind, a diffusion-reaction model is presented to explain the origin of the experimentally obtained length distribution focusing mechanism. The model is able to reproduce the decrease of the growth rate in the nanorod axial direction with both its thickness and length. On the other hand, low lateral reaction rates prevent the nanorod thickness distribution to be focused. In both crystallographic growth directions, a concentration-dependent critical thickness exists, which discriminates between nanorods with positive growth rates and those dissolving in the reaction solution. }, author = {Ibáñez, Maria and Guardia, Pablo and Shavel, Alexey and Cadavid, Doris and Arbiol, Jordi and Morante, Joan and Cabot, Andreu}, journal = {Journal of Physical Chemistry C}, number = {16}, pages = {7947 -- 7955}, publisher = {American Chemical Society}, title = {{Growth kinetics of asymmetric Bi2S3 nanocrystals: Size distribution focusing in nanorods}}, doi = {10.1021/jp2002904}, volume = {115}, year = {2011}, } @article{3379, abstract = {The process of gastrulation is highly conserved across vertebrates on both the genetic and morphological levels, despite great variety in embryonic shape and speed of development. This mechanism spatially separates the germ layers and establishes the organizational foundation for future development. Mesodermal identity is specified in a superficial layer of cells, the epiblast, where cells maintain an epithelioid morphology. These cells involute to join the deeper hypoblast layer where they adopt a migratory, mesenchymal morphology. Expression of a cascade of related transcription factors orchestrates the parallel genetic transition from primitive to mature mesoderm. Although the early and late stages of this process are increasingly well understood, the transition between them has remained largely mysterious. We present here the first high resolution in vivo observations of the blebby transitional morphology of involuting mesodermal cells in a vertebrate embryo. We further demonstrate that the zebrafish spadetail mutation creates a reversible block in the maturation program, stalling cells in the transition state. This mutation creates an ideal system for dissecting the specific properties of cells undergoing the morphological transition of maturing mesoderm, as we demonstrate with a direct measurement of cell–cell adhesion.}, author = {Row, Richard and Maître, Jean-Léon and Martin, Benjamin and Stockinger, Petra and Heisenberg, Carl-Philipp J and Kimelman, David}, journal = {Developmental Biology}, number = {1}, pages = {102 -- 110}, publisher = {Elsevier}, title = {{Completion of the epithelial to mesenchymal transition in zebrafish mesoderm requires Spadetail}}, doi = {10.1016/j.ydbio.2011.03.025}, volume = {354}, year = {2011}, } @article{3376, abstract = {Regulatory conflicts occur when two signals that individually trigger opposite cellular responses are present simultaneously. Here, we investigate regulatory conflicts in the bacterial response to antibiotic combinations. We use an Escherichia coli promoter-GFP library to study the transcriptional response of many promoters to either additive or antagonistic drug pairs at fine two-dimensional (2D) resolution of drug concentration. Surprisingly, we find that this data set can be characterized as a linear sum of only two principal components. Component one, accounting for over 70% of the response, represents the response to growth inhibition by the drugs. Component two describes how regulatory conflicts are resolved. For the additive drug pair, conflicts are resolved by linearly interpolating the single drug responses, while for the antagonistic drug pair, the growth-limiting drug dominates the response. Importantly, for a given drug pair, the same conflict resolution strategy applies to almost all genes. These results provide a recipe for predicting gene expression responses to antibiotic combinations.}, author = {Bollenbach, Mark Tobias and Kishony, Roy}, journal = {Molecular Cell}, number = {4}, pages = {413 -- 425}, publisher = {Cell Press}, title = {{Resolution of gene regulatory conflicts caused by combinations of antibiotics}}, doi = {10.1016/j.molcel.2011.04.016}, volume = {42}, year = {2011}, } @article{3380, abstract = {Linkage between markers and genes that affect a phenotype of interest may be determined by examining differences in marker allele frequency in the extreme progeny of a cross between two inbred lines. This strategy is usually employed when pooling is used to reduce genotyping costs. When the cross progeny are asexual, the extreme progeny may be selected by multiple generations of asexual reproduction and selection. We analyse this method of measuring phenotype in asexual progeny and examine the changes in marker allele frequency due to selection over many generations. Stochasticity in marker frequency in the selected population arises due to the finite initial population size. We derive the distribution of marker frequency as a result of selection at a single major locus, and show that in order to avoid spurious changes in marker allele frequency in the selected population, the initial population size should be in the low to mid hundreds.}, author = {Logeswaran, Sayanthan and Barton, Nicholas H}, journal = {Genetical Research}, number = {3}, pages = {221 -- 232}, publisher = {Cambridge University Press}, title = {{Mapping Mendelian traits in asexual progeny using changes in marker allele frequency}}, doi = {10.1017/S0016672311000115}, volume = {93}, year = {2011}, } @article{3377, abstract = {By definition, transverse intersections are stable under in- finitesimal perturbations. Using persistent homology, we ex- tend this notion to sizeable perturbations. Specifically, we assign to each homology class of the intersection its robust- ness, the magnitude of a perturbation necessary to kill it, and prove that robustness is stable. Among the applications of this result is a stable notion of robustness for fixed points of continuous mappings and a statement of stability for con- tours of smooth mappings.}, author = {Edelsbrunner, Herbert and Morozov, Dmitriy and Patel, Amit}, journal = {Foundations of Computational Mathematics}, number = {3}, pages = {345 -- 361}, publisher = {Springer}, title = {{Quantifying transversality by measuring the robustness of intersections}}, doi = {10.1007/s10208-011-9090-8}, volume = {11}, year = {2011}, } @article{3378, abstract = {The theory of intersection homology was developed to study the singularities of a topologically stratified space. This paper in- corporates this theory into the already developed framework of persistent homology. We demonstrate that persistent intersec- tion homology gives useful information about the relationship between an embedded stratified space and its singularities. We give, and prove the correctness of, an algorithm for the computa- tion of the persistent intersection homology groups of a filtered simplicial complex equipped with a stratification by subcom- plexes. We also derive, from Poincare ́ Duality, some structural results about persistent intersection homology.}, author = {Bendich, Paul and Harer, John}, journal = {Foundations of Computational Mathematics}, number = {3}, pages = {305 -- 336}, publisher = {Springer}, title = {{Persistent intersection homology}}, doi = {10.1007/s10208-010-9081-1}, volume = {11}, year = {2011}, } @article{3388, abstract = {Background: Fragmentation of terrestrial ecosystems has had detrimental effects on metapopulations of habitat specialists. Maculinea butterflies have been particularly affected because of their specialized lifecycles, requiring both specific food-plants and host-ants. However, the interaction between dispersal, effective population size, and long-term genetic erosion of these endangered butterflies remains unknown. Using non-destructive sampling, we investigated the genetic diversity of the last extant population of M. arion in Denmark, which experienced critically low numbers in the 1980s. Results: Using nine microsatellite markers, we show that the population is genetically impoverished compared to nearby populations in Sweden, but less so than monitoring programs suggested. Ten additional short repeat microsatellites were used to reconstruct changes in genetic diversity and population structure over the last 77 years from museum specimens. We also tested amplification efficiency in such historical samples as a function of repeat length and sample age. Low population numbers in the 1980s did not affect genetic diversity, but considerable turnover of alleles has characterized this population throughout the time-span of our analysis. Conclusions: Our results suggest that M. arion is less sensitive to genetic erosion via population bottlenecks than previously thought, and that managing clusters of high quality habitat may be key for long-term conservation.}, author = {Ugelvig, Line V and Nielsen, Per and Boomsma, Jacobus and Nash, David}, journal = {BMC Evolutionary Biology}, number = {201}, publisher = {BioMed Central}, title = {{Reconstructing eight decades of genetic variation in an isolated Danish population of the large blue butterfly Maculinea arion}}, doi = {10.1186/1471-2148-11-201}, volume = {11}, year = {2011}, } @article{3384, abstract = {Here we introduce a database of calibrated natural images publicly available through an easy-to-use web interface. Using a Nikon D70 digital SLR camera, we acquired about six-megapixel images of Okavango Delta of Botswana, a tropical savanna habitat similar to where the human eye is thought to have evolved. Some sequences of images were captured unsystematically while following a baboon troop, while others were designed to vary a single parameter such as aperture, object distance, time of day or position on the horizon. Images are available in the raw RGB format and in grayscale. Images are also available in units relevant to the physiology of human cone photoreceptors, where pixel values represent the expected number of photoisomerizations per second for cones sensitive to long (L), medium (M) and short (S) wavelengths. This database is distributed under a Creative Commons Attribution-Noncommercial Unported license to facilitate research in computer vision, psychophysics of perception, and visual neuroscience.}, author = {Tkacik, Gasper and Garrigan, Patrick and Ratliff, Charles and Milcinski, Grega and Klein, Jennifer and Seyfarth, Lucia and Sterling, Peter and Brainard, David and Balasubramanian, Vijay}, journal = {PLoS One}, number = {6}, publisher = {Public Library of Science}, title = {{Natural images from the birthplace of the human eye}}, doi = {10.1371/journal.pone.0020409}, volume = {6}, year = {2011}, } @article{3387, abstract = {Background: Supertree methods combine overlapping input trees into a larger supertree. Here, I consider split-based supertree methods that first extract the split information of the input trees and subsequently combine this split information into a phylogeny. Well known split-based supertree methods are matrix representation with parsimony and matrix representation with compatibility. Combining input trees on the same taxon set, as in the consensus setting, is a well-studied task and it is thus desirable to generalize consensus methods to supertree methods. Results: Here, three variants of majority-rule (MR) supertrees that generalize majority-rule consensus trees are investigated. I provide simple formulas for computing the respective score for bifurcating input- and supertrees. These score computations, together with a heuristic tree search minmizing the scores, were implemented in the python program PluMiST (Plus- and Minus SuperTrees) available from http://www.cibiv.at/software/ plumist. The different MR methods were tested by simulation and on real data sets. The search heuristic was successful in combining compatible input trees. When combining incompatible input trees, especially one variant, MR(-) supertrees, performed well. Conclusions: The presented framework allows for an efficient score computation of three majority-rule supertree variants and input trees. I combined the score computation with a heuristic search over the supertree space. The implementation was tested by simulation and on real data sets and showed promising results. Especially the MR(-) variant seems to be a reasonable score for supertree reconstruction. Generalizing these computations to multifurcating trees is an open problem, which may be tackled using this framework.}, author = {Kupczok, Anne}, journal = {BMC Evolutionary Biology}, number = {205}, publisher = {BioMed Central}, title = {{Split based computation of majority rule supertrees}}, doi = {10.1186/1471-2148-11-205}, volume = {11}, year = {2011}, } @article{3389, abstract = {Kernel canonical correlation analysis (KCCA) is a general technique for subspace learning that incorporates principal components analysis (PCA) and Fisher linear discriminant analysis (LDA) as special cases. By finding directions that maximize correlation, KCCA learns representations that are more closely tied to the underlying process that generates the data and can ignore high-variance noise directions. However, for data where acquisition in one or more modalities is expensive or otherwise limited, KCCA may suffer from small sample effects. We propose to use semi-supervised Laplacian regularization to utilize data that are present in only one modality. This approach is able to find highly correlated directions that also lie along the data manifold, resulting in a more robust estimate of correlated subspaces. Functional magnetic resonance imaging (fMRI) acquired data are naturally amenable to subspace techniques as data are well aligned. fMRI data of the human brain are a particularly interesting candidate. In this study we implemented various supervised and semi-supervised versions of KCCA on human fMRI data, with regression to single and multi-variate labels (corresponding to video content subjects viewed during the image acquisition). In each variate condition, the semi-supervised variants of KCCA performed better than the supervised variants, including a supervised variant with Laplacian regularization. We additionally analyze the weights learned by the regression in order to infer brain regions that are important to different types of visual processing.}, author = {Blaschko, Matthew and Shelton, Jacquelyn and Bartels, Andreas and Lampert, Christoph and Gretton, Arthur}, journal = {Pattern Recognition Letters}, number = {11}, pages = {1572 -- 1583}, publisher = {Elsevier}, title = {{Semi supervised kernel canonical correlation analysis with application to human fMRI}}, doi = {10.1016/j.patrec.2011.02.011}, volume = {32}, year = {2011}, } @article{3382, abstract = {Dynamic tactile sensing is a fundamental ability to recognize materials and objects. However, while humans are born with partially developed dynamic tactile sensing and quickly master this skill, today's robots remain in their infancy. The development of such a sense requires not only better sensors but the right algorithms to deal with these sensors' data as well. For example, when classifying a material based on touch, the data are noisy, high-dimensional, and contain irrelevant signals as well as essential ones. Few classification methods from machine learning can deal with such problems. In this paper, we propose an efficient approach to infer suitable lower dimensional representations of the tactile data. In order to classify materials based on only the sense of touch, these representations are autonomously discovered using visual information of the surfaces during training. However, accurately pairing vision and tactile samples in real-robot applications is a difficult problem. The proposed approach, therefore, works with weak pairings between the modalities. Experiments show that the resulting approach is very robust and yields significantly higher classification performance based on only dynamic tactile sensing.}, author = {Kroemer, Oliver and Lampert, Christoph and Peters, Jan}, journal = {IEEE Transactions on Robotics}, number = {3}, pages = {545 -- 557}, publisher = {IEEE}, title = {{Learning dynamic tactile sensing with robust vision based training}}, doi = {10.1109/TRO.2011.2121130}, volume = {27}, year = {2011}, } @article{3386, abstract = {Evolutionary theories of ageing predict that life span increases with decreasing extrinsic mortality, and life span variation among queens in ant species seems to corroborate this prediction: queens, which are the only reproductive in a colony, live much longer than queens in multi-queen colonies. The latter often inhabit ephemeral nest sites and accordingly are assumed to experience a higher mortality risk. Yet, all prior studies compared queens from different single- and multi-queen species. Here, we demonstrate an effect of queen number on longevity and fecundity within a single, socially plastic species, where queens experience the similar level of extrinsic mortality. Queens from single- and two-queen colonies had significantly longer lifespan and higher fecundity than queens living in associations of eight queens. As queens also differ neither in morphology nor the mode of colony foundation, our study shows that the social environment itself strongly affects ageing rate.}, author = {Schrempf, Alexandra and Cremer, Sylvia and Heinze, Jürgen}, journal = {Journal of Evolutionary Biology}, number = {7}, pages = {1455 -- 1461}, publisher = {Wiley-Blackwell}, title = {{Social influence on age and reproduction reduced lifespan and fecundity in multi queen ant colonies}}, doi = {10.1111/j.1420-9101.2011.02278.x}, volume = {24}, year = {2011}, } @article{3385, author = {Sixt, Michael K}, journal = {Immunology Letters}, number = {1}, pages = {32 -- 34}, publisher = {Elsevier}, title = {{Interstitial locomotion of leukocytes}}, doi = {10.1016/j.imlet.2011.02.013}, volume = {138}, year = {2011}, } @article{3383, author = {Heisenberg, Carl-Philipp J}, journal = {FEBS Journal}, number = {S1}, pages = {24 -- 24}, publisher = {Wiley-Blackwell}, title = {{Invited Lectures ‐ Symposia Area}}, doi = {10.1111/j.1742-4658.2011.08136.x}, volume = {278}, year = {2011}, } @article{3399, abstract = {Context-dependent adjustment of mating tactics can drastically increase the mating success of behaviourally flexible animals. We used the ant Cardiocondyla obscurior as a model system to study adaptive adjustment of male mating tactics. This species shows a male diphenism of wingless fighter males and peaceful winged males. Whereas the wingless males stay and exclusively mate in the maternal colony, the mating behaviour of winged males is plastic. They copulate with female sexuals in their natal nests early in life but later disperse in search for sexuals outside. In this study, we observed the nest-leaving behaviour of winged males under different conditions and found that they adaptively adjust the timing of their dispersal to the availability of mating partners, as well as the presence, and even the type of competitors in their natal nests. In colonies with virgin female queens winged males stayed longest when they were the only male in the nest. They left earlier when mating partners were not available or when other males were present. In the presence of wingless, locally mating fighter males, winged males dispersed earlier than in the presence of docile, winged competitors. This suggests that C. obscurior males are capable of estimating their local breeding chances and adaptively adjust their dispersal behaviour in both an opportunistic and a risk-sensitive way, thus showing hitherto unknown behavioural plasticity in social insect males.}, author = {Cremer, Sylvia and Schrempf, Alexandra and Heinze, Jürgen}, journal = {PLoS One}, number = {3}, publisher = {Public Library of Science}, title = {{Competition and opportunity shape the reproductive tactics of males in the ant Cardiocondyla obscurior}}, doi = {10.1371/journal.pone.0017323}, volume = {6}, year = {2011}, } @article{3401, abstract = {The Bicoid morphogen gradient directs the patterning of cell fates along the anterior-posterior axis of the syncytial Drosophila embryo and serves as a paradigm of morphogen-mediated patterning. The simplest models of gradient formation rely on constant protein synthesis and diffusion from anteriorly localized source mRNA, coupled with uniform protein degradation. However, currently such models cannot account for all known gradient characteristics. Recent work has proposed that bicoid mRNA spatial distribution is sufficient to produce the observed protein gradient, minimizing the role of protein transport. Here, we adapt a novel method of fluorescent in situ hybridization to quantify the global spatio-temporal dynamics of bicoid mRNA particles. We determine that >90% of all bicoid mRNA is continuously present within the anterior 20% of the embryo. bicoid mRNA distribution along the body axis remains nearly unchanged despite dynamic mRNA translocation from the embryo core to the cortex. To evaluate the impact of mRNA distribution on protein gradient dynamics, we provide detailed quantitative measurements of nuclear Bicoid levels during the formation of the protein gradient. We find that gradient establishment begins 45 minutes after fertilization and that the gradient requires about 50 minutes to reach peak levels. In numerical simulations of gradient formation, we find that incorporating the actual bicoid mRNA distribution yields a closer prediction of the observed protein dynamics compared to modeling protein production from a point source at the anterior pole. We conclude that the spatial distribution of bicoid mRNA contributes to, but cannot account for, protein gradient formation, and therefore that protein movement, either active or passive, is required for gradient formation.}, author = {Little, Shawn and Tkacik, Gasper and Kneeland, Thomas and Wieschaus, Eric and Gregor, Thomas}, journal = {PLoS Biology}, number = {3}, publisher = {Public Library of Science}, title = {{The formation of the Bicoid morphogen gradient requires protein movement from anteriorly localized source}}, doi = {10.1371/journal.pbio.1000596}, volume = {9}, year = {2011}, } @inbook{3724, abstract = {Small photochromic molecules are widespread in nature and serve as switches for a plethora of light-controlled processes. In a typical photoreceptor, the different geometries and polarities of the photochrome isomers are tightly coupled to functionally relevant conformational changes in the proteins. The past decade has seen extensive efforts to mimic nature and create proteins controlled by synthetic photochromes in the laboratory. Here, we discuss the role of molecular modeling to gain a structural understanding of photochromes and to design light-controlled peptides and proteins. We address several fundamental questions: What are the molecular structures of photochromes, particularly for metastable isomers that cannot be addressed experimentally? How are the structures of bistable photoisomers coupled to the conformational states of peptides and proteins? Can we design light-controlled proteins rapidly and reliably? After an introduction to the principles of molecular modeling, we answer these questions by examining systems that range from the size of isolated photochromes, to that of peptides and large cell surface receptors, each from its unique computational perspective.}, author = {Harald Janovjak and Isacoff, Ehud Y}, booktitle = {Photosensitive Molecules for the Control of Biological Function}, pages = {233 -- 266}, publisher = {Springer}, title = {{Structure-based design of light-controlled proteins}}, doi = {10.1007/978-1-61779-031-7_13}, volume = {55}, year = {2011}, } @article{3770, abstract = {The pink dolphin (Inia geoffrensis) is widely distributed along the Amazon and Orinoco basins, covering an area of approximately 7 million km2. Previous morphological and genetic studies have proposed the existence of at least two evolutionary significant units: one distributed across the Orinoco and Amazon basins and another confined to the Bolivian Amazon. The presence of barriers in the riverine environment has been suggested to play a significant role in shaping present-day patterns of ecological and genetic structure for this species. In the present study, we examined the phylogeographic structure, lineage divergence time and historical demography using mitochondrial (mt)DNA sequences in different pink dolphin populations distributed in large and small spatial scales, including two neighbouring Brazilian Amazon populations. mtDNA control region (CR) analysis revealed that the Brazilian haplotypes occupy an intermediate position compared to three previously studied geographic locations: the Colombian Amazon, the Colombian Orinoco, and the Bolivian Amazon. On a local scale, we have identified a pattern of maternal isolation between two neighbouring populations from Brazil. Six mtDNA CR haplotypes were identified in Brazil with no sharing between the two populations, as well as specific cytochrome b (cyt b) haplotypes identified in each locality. In addition, we analyzed autosomal microsatellites to investigate male-mediated gene flow and demographic changes within the study area in Brazil. Data analysis of 14 microsatellite loci failed to detect significant population subdivision, suggesting that male-mediated gene flow may maintain homogeneity between these two locations. Moreover, both mtDNA and microsatellite data indicate a major demographic collapse within Brazil in the late Pleistocene. Bayesian skyline plots (BSP) of mtDNA data revealed a stable population for Colombian and Brazilian Amazon lineages through time, whereas a population decline was demonstrated in the Colombian Orinoco lineage. Moreover, BSP and Tajima's D and Fu's Fs tests revealed a recent population expansion exclusively in the Bolivian sample. Finally, we estimated that the diversification of the Inia sp. lineage began in the Late Pliocene (approximately 3.1 Mya) and continued throughout the Pleistocene.}, author = {Hollatz, Claudia and Vilaça, Sibelle and Fernandes Redondo, Rodrigo A and Marmontel, Míriam and Baker, Cyndi and Santos, Fabrício}, journal = {Biological Journal of the Linnean Society}, number = {4}, pages = {812 -- 827}, publisher = {Wiley}, title = {{The Amazon River system as an ecological barrier driving genetic differentiation of the pink dolphin (Inia geoffrensis)}}, doi = {10.1111/j.1095-8312.2011.01616.x}, volume = {102}, year = {2011}, } @article{3771, abstract = {The small-sized frugivorous bat Carollia perspicillata is an understory specialist and occurs in a wide range of lowland habitats, tending to be more common in tropical dry or moist forests of South and Central America. Its sister species, Carollia brevicauda, occurs almost exclusively in the Amazon rainforest. A recent phylogeographic study proposed a hypothesis of origin and subsequent diversification for C. perspicillata along the Atlantic coastal forest of Brazil. Additionally, it also found two allopatric clades for C. brevicauda separated by the Amazon Basin. We used cytochrome b gene sequences and a more extensive sampling to test hypotheses related to the origin and diversification of C. perspicillata plus C. brevicauda clade in South America. The results obtained indicate that there are two sympatric evolutionary lineages within each species. In C. perspicillata, one lineage is limited to the Southern Atlantic Forest, whereas the other is widely distributed. Coalescent analysis points to a simultaneous origin for C. perspicillata and C. brevicauda, although no place for the diversification of each species can be firmly suggested. The phylogeographic pattern shown by C. perspicillata is also congruent with the Pleistocene refugia hypothesis as a likely vicariant phenomenon shaping the present distribution of its intraspecific lineages.}, author = {Pavan, Ana and Martins, Felipe and Santos, Fabrício and Ditchfield, Albert and Fernandes Redondo, Rodrigo A}, journal = {Biological Journal of the Linnean Society}, number = {3}, pages = {527 -- 539}, publisher = {Wiley-Blackwell}, title = {{Patterns of diversification in two species of short-tailed bats (Carollia Gray, 1838): the effects of historical fragmentation of Brazilian rainforests.}}, doi = {10.1111/j.1095-8312.2010.01601.x}, volume = {102}, year = {2011}, } @article{3778, author = {Barton, Nicholas H}, journal = {Heredity}, number = {2}, pages = {205 -- 206}, publisher = {Nature Publishing Group}, title = {{Estimating linkage disequilibria}}, doi = {10.1038/hdy.2010.67}, volume = {106}, year = {2011}, } @inbook{3791, abstract = {During the development of multicellular organisms, cell fate specification is followed by the sorting of different cell types into distinct domains from where the different tissues and organs are formed. Cell sorting involves both the segregation of a mixed population of cells with different fates and properties into distinct domains, and the active maintenance of their segregated state. Because of its biological importance and apparent resemblance to fluid segregation in physics, cell sorting was extensively studied by both biologists and physicists over the last decades. Different theories were developed that try to explain cell sorting on the basis of the physical properties of the constituent cells. However, only recently the molecular and cellular mechanisms that control the physical properties driving cell sorting, have begun to be unraveled. In this review, we will provide an overview of different cell-sorting processes in development and discuss how these processes can be explained by the different sorting theories, and how these theories in turn can be connected to the molecular and cellular mechanisms driving these processes.}, author = {Krens, Gabriel and Heisenberg, Carl-Philipp J}, booktitle = {Forces and Tension in Development}, editor = {Labouesse, Michel}, pages = {189 -- 213}, publisher = {Elsevier}, title = {{Cell sorting in development}}, doi = {10.1016/B978-0-12-385065-2.00006-2}, volume = {95}, year = {2011}, } @article{3364, abstract = {Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete-state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required.}, author = {Didier, Frédéric and Henzinger, Thomas A and Mateescu, Maria and Wolf, Verena}, journal = {Theoretical Computer Science}, number = {21}, pages = {2128 -- 2141}, publisher = {Elsevier}, title = {{Approximation of event probabilities in noisy cellular processes}}, doi = {10.1016/j.tcs.2010.10.022}, volume = {412}, year = {2011}, } @article{469, abstract = {Spontaneous release of glutamate is important for maintaining synaptic strength and controlling spike timing in the brain. Mechanisms regulating spontaneous exocytosis remain poorly understood. Extracellular calcium concentration ([Ca2+]o) regulates Ca2+ entry through voltage-activated calcium channels (VACCs) and consequently is a pivotal determinant of action potential-evoked vesicle fusion. Extracellular Ca 2+ also enhances spontaneous release, but via unknown mechanisms. Here we report that external Ca2+ triggers spontaneous glutamate release more weakly than evoked release in mouse neocortical neurons. Blockade of VACCs has no effect on the spontaneous release rate or its dependence on [Ca2+]o. Intracellular [Ca2+] slowly increases in a minority of neurons following increases in [Ca2+]o. Furthermore, the enhancement of spontaneous release by extracellular calcium is insensitive to chelation of intracellular calcium by BAPTA. Activation of the calcium-sensing receptor (CaSR), a G-protein-coupled receptor present in nerve terminals, by several specific agonists increased spontaneous glutamate release. The frequency of spontaneous synaptic transmission was decreased in CaSR mutant neurons. The concentration-effect relationship for extracellular calcium regulation of spontaneous release was well described by a combination of CaSR-dependent and CaSR-independent mechanisms. Overall these results indicate that extracellular Ca2+ does not trigger spontaneous glutamate release by simply increasing calcium influx but stimulates CaSR and thereby promotes resting spontaneous glutamate release. }, author = {Vyleta, Nicholas and Smith, Stephen}, journal = {European Journal of Neuroscience}, number = {12}, pages = {4593 -- 4606}, publisher = {Wiley-Blackwell}, title = {{Spontaneous glutamate release is independent of calcium influx and tonically activated by the calcium-sensing receptor}}, doi = {10.1523/JNEUROSCI.6398-10.2011}, volume = {31}, year = {2011}, } @article{490, abstract = {BioSig is an open source software library for biomedical signal processing. The aim of the BioSig project is to foster research in biomedical signal processing by providing free and open source software tools for many different application areas. Some of the areas where BioSig can be employed are neuroinformatics, brain-computer interfaces, neurophysiology, psychology, cardiovascular systems, and sleep research. Moreover, the analysis of biosignals such as the electroencephalogram (EEG), electrocorticogram (ECoG), electrocardiogram (ECG), electrooculogram (EOG), electromyogram (EMG), or respiration signals is a very relevant element of the BioSig project. Specifically, BioSig provides solutions for data acquisition, artifact processing, quality control, feature extraction, classification, modeling, and data visualization, to name a few. In this paper, we highlight several methods to help students and researchers to work more efficiently with biomedical signals. }, author = {Schlögl, Alois and Vidaurre, Carmen and Sander, Tilmann}, journal = {Computational Intelligence and Neuroscience}, publisher = {Hindawi Publishing Corporation}, title = {{BioSig: The free and open source software library for biomedical signal processing}}, doi = {10.1155/2011/935364}, volume = {2011}, year = {2011}, } @article{491, abstract = {In their search for antigens, lymphocytes continuously shuttle among blood vessels, lymph vessels, and lymphatic tissues. Chemokines mediate entry of lymphocytes into lymphatic tissues, and sphingosine 1-phosphate (S1P) promotes localization of lymphocytes to the vasculature. Both signals are sensed through G protein-coupled receptors (GPCRs). Most GPCRs undergo ligand-dependent homologous receptor desensitization, a process that decreases their signaling output after previous exposure to high ligand concentration. Such desensitization can explain why lymphocytes do not take an intermediate position between two signals but rather oscillate between them. The desensitization of S1P receptor 1 (S1PR1) is mediated by GPCR kinase 2 (GRK2). Deletion of GRK2 in lymphocytes compromises desensitization by high vascular S1P concentrations, thereby reducing responsiveness to the chemokine signal and trapping the cells in the vascular compartment. The desensitization kinetics of S1PR1 allows lymphocytes to dynamically shuttle between vasculature and lymphatic tissue, although the positional information in both compartments is static.}, author = {Eichner, Alexander and Sixt, Michael K}, journal = {Science Signaling}, number = {198}, publisher = {American Association for the Advancement of Science}, title = {{Setting the clock for recirculating lymphocytes}}, doi = {10.1126/scisignal.2002617}, volume = {4}, year = {2011}, } @article{518, abstract = {Cancer stem cells or cancer initiating cells are believed to contribute to cancer recurrence after therapy. MicroRNAs (miRNAs) are short RNA molecules with fundamental roles in gene regulation. The role of miRNAs in cancer stem cells is only poorly understood. Here, we report miRNA expression profiles of glioblastoma stem cell-containing CD133 + cell populations. We find that miR-9, miR-9 * (referred to as miR-9/9 *), miR-17 and miR-106b are highly abundant in CD133 + cells. Furthermore, inhibition of miR-9/9 * or miR-17 leads to reduced neurosphere formation and stimulates cell differentiation. Calmodulin-binding transcription activator 1 (CAMTA1) is a putative transcription factor, which induces the expression of the anti-proliferative cardiac hormone natriuretic peptide A (NPPA). We identify CAMTA1 as an miR-9/9 * and miR-17 target. CAMTA1 expression leads to reduced neurosphere formation and tumour growth in nude mice, suggesting that CAMTA1 can function as tumour suppressor. Consistently, CAMTA1 and NPPA expression correlate with patient survival. Our findings could provide a basis for novel strategies of glioblastoma therapy.}, author = {Schraivogel, Daniel and Weinmann, Lasse and Beier, Dagmar and Tabatabai, Ghazaleh and Eichner, Alexander and Zhu, Jia and Anton, Martina and Sixt, Michael K and Weller, Michael and Beier, Christoph and Meister, Gunter}, journal = {EMBO Journal}, number = {20}, pages = {4309 -- 4322}, publisher = {Wiley-Blackwell}, title = {{CAMTA1 is a novel tumour suppressor regulated by miR-9/9 * in glioblastoma stem cells}}, doi = {10.1038/emboj.2011.301}, volume = {30}, year = {2011}, } @article{531, abstract = {Software transactional memories (STM) are described in the literature with assumptions of sequentially consistent program execution and atomicity of high level operations like read, write, and abort. However, in a realistic setting, processors use relaxed memory models to optimize hardware performance. Moreover, the atomicity of operations depends on the underlying hardware. This paper presents the first approach to verify STMs under relaxed memory models with atomicity of 32 bit loads and stores, and read-modify-write operations. We describe RML, a simple language for expressing concurrent programs. We develop a semantics of RML parametrized by a relaxed memory model. We then present our tool, FOIL, which takes as input the RML description of an STM algorithm restricted to two threads and two variables, and the description of a memory model, and automatically determines the locations of fences, which if inserted, ensure the correctness of the restricted STM algorithm under the given memory model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of sequential consistency, total store order, partial store order, and relaxed memory order for two threads and two variables. Finally, we extend the verification results for DSTM and TL2 to an arbitrary number of threads and variables by manually proving that the structural properties of STMs are satisfied at the hardware level of atomicity under the considered relaxed memory models.}, author = {Guerraoui, Rachid and Henzinger, Thomas A and Singh, Vasu}, journal = {Formal Methods in System Design}, number = {3}, pages = {297 -- 331}, publisher = {Springer}, title = {{Verification of STM on relaxed memory models}}, doi = {10.1007/s10703-011-0131-3}, volume = {39}, year = {2011}, } @misc{5379, abstract = {Computing the winning set for Büchi objectives in alternating games on graphs is a central problem in computer aided verification with a large number of applications. The long standing best known upper bound for solving the problem is ̃O(n·m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the ̃O(n·m) boundary by presenting a new technique that reduces the running time to O(n2). This bound also leads to O(n2) time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of O(n·m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n3)), and (3) in Markov decision processes (improving for m > n4/3 an earlier bound of O(min(m1.5, m·n2/3)). We also show that the same technique can be used to compute the maximal end-component decomposition of a graph in time O(n2), which is an improvement over earlier bounds for m > n4/3. Finally, we show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. This is the first dynamic algorithm for this problem.}, author = {Chatterjee, Krishnendu and Henzinger, Monika H}, issn = {2664-1690}, pages = {20}, publisher = {IST Austria}, title = {{An O(n2) time algorithm for alternating Büchi games}}, doi = {10.15479/AT:IST-2011-0009}, year = {2011}, } @misc{5381, abstract = {In two-player finite-state stochastic games of partial obser- vation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distri- bution over the successor states. The game is played for infinitely many rounds and thus the players construct an infinite path in the graph. We consider reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1) or pos- itively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two- sided with (c) both players having partial observation. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Our main results for pure strategies are as follows: (1) For one-sided games with player 2 perfect observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strate- gies are not sufficient, and present an exponential upper bound on mem- ory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete and present symbolic algo- rithms that avoid the explicit exponential construction. (2) For one-sided games with player 1 perfect observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and posi- tive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence re- sult exhibit serious flaws in previous results in the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, issn = {2664-1690}, pages = {43}, publisher = {IST Austria}, title = {{Partial-observation stochastic games: How to win when belief fails}}, doi = {10.15479/AT:IST-2011-0007}, year = {2011}, } @misc{5380, abstract = {We consider 2-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. We study concurrent games with ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). We study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision or infinite-precision; and in terms of memory, strategies can be memoryless, finite-memory or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in O(n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms,that are obtained by characterization of the winning sets as μ-calculus formulas, are considerably more involved than those for turn-based games.}, author = {Chatterjee, Krishnendu}, issn = {2664-1690}, pages = {53}, publisher = {IST Austria}, title = {{Bounded rationality in concurrent parity games}}, doi = {10.15479/AT:IST-2011-0008}, year = {2011}, } @misc{5382, abstract = {We consider two-player stochastic games played on a finite state space for an infinite num- ber of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine a probability distribution over the successor states. We also consider the important special case of turn-based stochastic games where players make moves in turns, rather than concurrently. We study concurrent games with ω-regular winning conditions specified as parity objectives. The value for player 1 for a parity objective is the maximal probability with which the player can guarantee the satisfaction of the objective against all strategies of the opponent. We study the problem of continuity and robustness of the value function in concurrent and turn-based stochastic parity games with respect to imprecision in the transition probabilities. We present quantitative bounds on the difference of the value function (in terms of the imprecision of the transition probabilities) and show the value continuity for structurally equivalent concurrent games (two games are structurally equivalent if the support of the transition func- tion is same and the probabilities differ). We also show robustness of optimal strategies for structurally equivalent turn-based stochastic parity games. Finally we show that the value continuity property breaks without the structurally equivalent assumption (even for Markov chains) and show that our quantitative bound is asymptotically optimal. Hence our results are tight (the assumption is both necessary and sufficient) and optimal (our quantitative bound is asymptotically optimal).}, author = {Chatterjee, Krishnendu}, issn = {2664-1690}, pages = {18}, publisher = {IST Austria}, title = {{Robustness of structurally equivalent concurrent parity games}}, doi = {10.15479/AT:IST-2011-0006}, year = {2011}, } @unpublished{3338, abstract = {We consider 2-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves inde- pendently and simultaneously; the current state and the two moves determine the successor state. We study concurrent games with ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respec- tively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). We study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision or infinite- precision; and in terms of memory, strategies can be memoryless, finite-memory or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as power- ful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in O(n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms, that are obtained by characterization of the winning sets as μ-calculus formulas, are considerably more involved than those for turn-based games.}, author = {Chatterjee, Krishnendu}, booktitle = {arXiv}, pages = {1 -- 51}, publisher = {ArXiv}, title = {{Bounded rationality in concurrent parity games}}, year = {2011}, } @inproceedings{3356, abstract = {There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with "controlled-accumulation", allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable.}, author = {Boker, Udi and Chatterjee, Krishnendu and Henzinger, Thomas A and Kupferman, Orna}, location = {Toronto, Canada}, publisher = {IEEE}, title = {{Temporal specifications with accumulative values}}, doi = {10.1109/LICS.2011.33}, year = {2011}, } @misc{5385, abstract = {There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with “controlled-accumulation”, allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable.}, author = {Boker, Udi and Chatterjee, Krishnendu and Henzinger, Thomas A and Kupferman, Orna}, issn = {2664-1690}, pages = {14}, publisher = {IST Austria}, title = {{Temporal specifications with accumulative values}}, doi = {10.15479/AT:IST-2011-0003}, year = {2011}, } @misc{5386, abstract = {We introduce TopoCut: a new way to integrate knowledge about topological properties (TPs) into random field image segmentation model. Instead of including TPs as additional constraints during minimization of the energy function, we devise an efficient algorithm for modifying the unary potentials such that the resulting segmentation is guaranteed with the desired properties. Our method is more flexible in the sense that it handles more topology constraints than previous methods, which were only able to enforce pairwise or global connectivity. In particular, our method is very fast, making it for the first time possible to enforce global topological properties in practical image segmentation tasks.}, author = {Chen, Chao and Freedman, Daniel and Lampert, Christoph}, issn = {2664-1690}, pages = {69}, publisher = {IST Austria}, title = {{Enforcing topological constraints in random field image segmentation}}, doi = {10.15479/AT:IST-2011-0002}, year = {2011}, } @misc{5383, abstract = {We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures.}, author = {Wies, Thomas and Muñiz, Marco and Kuncak, Viktor}, issn = {2664-1690}, pages = {25}, publisher = {IST Austria}, title = {{On an efficient decision procedure for imperative tree data structures}}, doi = {10.15479/AT:IST-2011-0005}, year = {2011}, } @misc{5384, abstract = {We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether for every ε > 0 there is a word that is accepted with probability at least 1 − ε. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions.}, author = {Chatterjee, Krishnendu and Tracol, Mathieu}, issn = {2664-1690}, pages = {30}, publisher = {IST Austria}, title = {{Decidable problems for probabilistic automata on infinite words}}, doi = {10.15479/AT:IST-2011-0004}, year = {2011}, } @inproceedings{3336, abstract = {We introduce TopoCut: a new way to integrate knowledge about topological properties (TPs) into random field image segmentation model. Instead of including TPs as additional constraints during minimization of the energy function, we devise an efficient algorithm for modifying the unary potentials such that the resulting segmentation is guaranteed with the desired properties. Our method is more flexible in the sense that it handles more topology constraints than previous methods, which were only able to enforce pairwise or global connectivity. In particular, our method is very fast, making it for the first time possible to enforce global topological properties in practical image segmentation tasks.}, author = {Chen, Chao and Freedman, Daniel and Lampert, Christoph}, booktitle = {CVPR: Computer Vision and Pattern Recognition}, isbn = {978-1-4577-0394-2}, location = {Colorado Springs, CO, United States}, pages = {2089 -- 2096}, publisher = {IEEE}, title = {{Enforcing topological constraints in random field image segmentation}}, doi = {10.1109/CVPR.2011.5995503}, year = {2011}, } @inproceedings{3323, abstract = {We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures.}, author = {Wies, Thomas and Muñiz, Marco and Kuncak, Viktor}, location = {Wrocław, Poland}, pages = {476 -- 491}, publisher = {Springer}, title = {{An efficient decision procedure for imperative tree data structures}}, doi = {10.1007/978-3-642-22438-6_36}, volume = {6803}, year = {2011}, } @inproceedings{3366, abstract = {We present an algorithmic method for the quantitative, performance-aware synthesis of concurrent programs. The input consists of a nondeterministic partial program and of a parametric performance model. The nondeterminism allows the programmer to omit which (if any) synchronization construct is used at a particular program location. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the nondeterminism of the partial program so that both correctness is guaranteed and performance is optimal. As is standard for shared memory concurrency, correctness is formalized "specification free", in particular as race freedom or deadlock freedom. For worst-case (average-case) performance, we show that the problem can be reduced to 2-player graph games (with probabilistic transitions) with quantitative objectives. While we show, using game-theoretic methods, that the synthesis problem is Nexp-complete, we present an algorithmic method and an implementation that works efficiently for concurrent programs and performance models of practical interest. We have implemented a prototype tool and used it to synthesize finite-state concurrent programs that exhibit different programming patterns, for several performance models representing different architectures. }, author = {Cerny, Pavol and Chatterjee, Krishnendu and Henzinger, Thomas A and Radhakrishna, Arjun and Singh, Rohit}, editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz}, location = {Snowbird, USA}, pages = {243 -- 259}, publisher = {Springer}, title = {{Quantitative synthesis for concurrent programs}}, doi = {10.1007/978-3-642-22110-1_20}, volume = {6806}, year = {2011}, } @inproceedings{3345, abstract = {We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode ω-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition re- quires that the resource level never drops below 0, and the mean-payoff condi- tion requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, location = {Warsaw, Poland}, pages = {206 -- 218}, publisher = {Springer}, title = {{Energy and mean-payoff parity Markov Decision Processes}}, doi = {10.1007/978-3-642-22993-0_21}, volume = {6907}, year = {2011}, } @misc{5387, abstract = {We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode ω-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition re- quires that the resource level never drops below 0, and the mean-payoff condi- tion requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, issn = {2664-1690}, pages = {20}, publisher = {IST Austria}, title = {{Energy and mean-payoff parity Markov decision processes}}, doi = {10.15479/AT:IST-2011-0001}, year = {2011}, } @article{580, author = {Onur Hosten}, journal = {Nature}, number = {7350}, pages = {170 -- 171}, publisher = {Nature Publishing Group}, title = {{Quantum physics: How to catch a wave}}, doi = {10.1038/474170a}, volume = {474}, year = {2011}, } @inproceedings{585, abstract = {We present two independent schemes for the precise focusing of orthogonal polarizations of light at arbitrary relative locations. The first scheme uses a polarization Sagnac interferometer, the second a set of three birefringent elements. }, author = {Schmid, David and Hazrat, Shiraz and Rangarajan, Radhika and Onur Hosten and Quint, Stephan and Kwiat, Paul G}, publisher = {OSA}, title = {{Methods towards achieving precise birefringent focusing}}, doi = {10.1364/CLEO_AT.2011.JThB130}, year = {2011}, } @article{586, abstract = {We demonstrate a Raman laser using cold Rb87 atoms as the gain medium in a high-finesse optical cavity. We observe robust continuous wave lasing in the atypical regime where single atoms can considerably affect the cavity field. Consequently, we discover unusual lasing threshold behavior in the system causing jumps in lasing power, and propose a model to explain the effect. We also measure the intermode laser linewidth, and observe values as low as 80Hz. The tunable gain properties of this laser suggest multiple directions for future research.}, author = {Vrijsen, Geert and Onur Hosten and Lee, Jongmin and Bernon, Simon and Kasevich, Mark A}, journal = {Physical Review Letters}, number = {6}, publisher = {American Physical Society}, title = {{Raman lasing with a cold atom gain medium in a high-finesse optical cavity}}, doi = {10.1103/PhysRevLett.107.063904}, volume = {107}, year = {2011}, } @article{597, abstract = {The macromolecular assembly required to initiate transcription of protein-coding genes, known as the Pre-Initiation Complex (PIC), consists of multiple protein complexes and is approximately 3.5 MDa in size. At the heart of this assembly is the Mediator complex, which helps regulate PIC activity and interacts with the RNA polymerase II (pol II) enzyme. The structure of the human Mediator-pol II interface is not well-characterized, whereas attempts to structurally define the Mediator-pol II interaction in yeast have relied on incomplete assemblies of Mediator and/or pol II and have yielded inconsistent interpretations. We have assembled the complete, 1.9 MDa human Mediator-pol II-TFIIF complex from purified components and have characterized its structural organization using cryo-electron microscopy and single-particle reconstruction techniques. The orientation of pol II within this assembly was determined by crystal structure docking and further validated with projection matching experiments, allowing the structural organization of the entire human PIC to be envisioned. Significantly, pol II orientation within the Mediator-pol II-TFIIF assembly can be reconciled with past studies that determined the location of other PIC components relative to pol II itself. Pol II surfaces required for interacting with TFIIB, TFIIE, and promoter DNA (i.e., the pol II cleft) are exposed within the Mediator-pol II-TFIIF structure; RNA exit is unhindered along the RPB4/7 subunits; upstream and downstream DNA is accessible for binding additional factors; and no major structural re-organization is necessary to accommodate the large, multi-subunit TFIIH or TFIID complexes. The data also reveal how pol II binding excludes Mediator-CDK8 subcomplex interactions and provide a structural basis for Mediator-dependent control of PIC assembly and function. Finally, parallel structural analysis of Mediator-pol II complexes lacking TFIIF reveal that TFIIF plays a key role in stabilizing pol II orientation within the assembly.}, author = {Bernecky, Carrie A and Grob, Patricia and Ebmeier, Christopher and Nogales, Eva and Taatjes, Dylan}, journal = {PLoS Biology}, number = {3}, publisher = {Public Library of Science}, title = {{Molecular architecture of the human Mediator-RNA polymerase II-TFIIF assembly}}, doi = {10.1371/journal.pbio.1000603}, volume = {9}, year = {2011}, }