Semi supervised kernel canonical correlation analysis with application to human fMRI - Blaschko, Matthew; Shelton, Jacquelyn; Bartels, Andreas; Lampert, Christoph; Gretton, Arthur (Pattern Recognition Letters)
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.

Learning dynamic tactile sensing with robust vision based training - Kroemer, Oliver; Lampert, Christoph; Peters, Jan (IEEE Transactions on Robotics)
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.

Social influence on age and reproduction reduced lifespan and fecundity in multi queen ant colonies - Schrempf, Alexandra; Cremer, Sylvia; Heinze, Jürgen (Journal of Evolutionary Biology)
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.

Interstitial locomotion of leukocytes - Sixt, Michael K (Immunology Letters)

Invited Lectures ‐ Symposia Area - Heisenberg, Carl-Philipp J (FEBS Journal)

Competition and opportunity shape the reproductive tactics of males in the ant Cardiocondyla obscurior - Cremer, Sylvia; Schrempf, Alexandra; Heinze, Jürgen (PLoS One)
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.

Patterns of diversification in two species of short-tailed bats (Carollia Gray, 1838): the effects of historical fragmentation of Brazilian rainforests. - Pavan, Ana; Martins, Felipe; Santos, Fabrício; Ditchfield, Albert; Fernandes Redondo, Rodrigo A (Biological Journal of the Linnean Society)
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.

Estimating linkage disequilibria - Barton, Nicholas H (Heredity)

Cell sorting in development - Krens, Gabriel; Heisenberg, Carl-Philipp J (Forces and Tension in Development)
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.

Approximation of event probabilities in noisy cellular processes - Didier, Frédéric; Henzinger, Thomas A; Mateescu, Maria; Wolf, Verena (Theoretical Computer Science)
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.

Spontaneous glutamate release is independent of calcium influx and tonically activated by the calcium-sensing receptor - Vyleta, Nicholas; Smith, Stephen (European Journal of Neuroscience)
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.

BioSig: The free and open source software library for biomedical signal processing - Schlögl, Alois; Vidaurre, Carmen; Sander, Tilmann (Computational Intelligence and Neuroscience)
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.

Setting the clock for recirculating lymphocytes - Eichner, Alexander; Sixt, Michael K (Science Signaling)
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.

CAMTA1 is a novel tumour suppressor regulated by miR-9/9 * in glioblastoma stem cells - Schraivogel, Daniel; Weinmann, Lasse; Beier, Dagmar; Tabatabai, Ghazaleh; Eichner, Alexander; Zhu, Jia; Anton, Martina; Sixt, Michael K; Weller, Michael; Beier, Christoph; Meister, Gunter (EMBO Journal)
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.

Verification of STM on relaxed memory models - Guerraoui, Rachid; Henzinger, Thomas A; Singh, Vasu (Formal Methods in System Design)
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.

An O(n2) time algorithm for alternating Büchi games - Chatterjee, Krishnendu; Henzinger, Monika H
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.

Partial-observation stochastic games: How to win when belief fails - Chatterjee, Krishnendu; Doyen, Laurent
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.

Bounded rationality in concurrent parity games - Chatterjee, Krishnendu
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.

Robustness of structurally equivalent concurrent parity games - Chatterjee, Krishnendu
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).

Bounded rationality in concurrent parity games - Chatterjee, Krishnendu (arXiv)
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.

Temporal specifications with accumulative values - Boker, Udi; Chatterjee, Krishnendu; Henzinger, Thomas A; Kupferman, Orna
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.

Temporal specifications with accumulative values - Boker, Udi; Chatterjee, Krishnendu; Henzinger, Thomas A; Kupferman, Orna
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.

Enforcing topological constraints in random field image segmentation - Chen, Chao; Freedman, Daniel; Lampert, Christoph
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.

On an efficient decision procedure for imperative tree data structures - Wies, Thomas; Muñiz, Marco; Kuncak, Viktor
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.

Decidable problems for probabilistic automata on infinite words - Chatterjee, Krishnendu; Tracol, Mathieu
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.

Enforcing topological constraints in random field image segmentation - Chen, Chao; Freedman, Daniel; Lampert, Christoph (CVPR: Computer Vision and Pattern Recognition)
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.

An efficient decision procedure for imperative tree data structures - Wies, Thomas; Muñiz, Marco; Kuncak, Viktor
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.

Quantitative synthesis for concurrent programs - Cerny, Pavol; Chatterjee, Krishnendu; Henzinger, Thomas A; Radhakrishna, Arjun; Singh, Rohit
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.

Energy and mean-payoff parity Markov Decision Processes - Chatterjee, Krishnendu; Doyen, Laurent
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.

Energy and mean-payoff parity Markov decision processes - Chatterjee, Krishnendu; Doyen, Laurent
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.

Noise underlies switching behavior of the bacterial flagellum - Park, Heungwon; Oikonomou, Panos; Guet, Calin C; Cluzel, Philippe (Biophysical Journal)
We report the switching behavior of the full bacterial flagellum system that includes the filament and the motor in wild-type Escherichia coli cells. In sorting the motor behavior by the clockwise bias, we find that the distributions of the clockwise (CW) and counterclockwise (CCW) intervals are either exponential or nonexponential with long tails. At low bias, CW intervals are exponentially distributed and CCW intervals exhibit long tails. At intermediate CW bias (0.5) both CW and CCW intervals are mainly exponentially distributed. A simple model suggests that these two distinct switching behaviors are governed by the presence of signaling noise within the chemotaxis network. Low noise yields exponentially distributed intervals, whereas large noise yields nonexponential behavior with long tails. These drastically different motor statistics may play a role in optimizing bacterial behavior for a wide range of environmental conditions.

Regulation of imprinted gene expression in Arabidopsis endosperm - Hsieh, Tzung-Fu; Shin, Juhyun; Uzawa, Rie; Silva, Pedro; Cohen, Stephanie; Bauer, Matthew J.; Hashimoto, Meryl; Kirkbride, Ryan C.; Harada, John J.; Zilberman, Daniel; Fischer, Robert L. (Proceedings of the National Academy of Sciences)
Imprinted genes are expressed primarily or exclusively from either the maternal or paternal allele, a phenomenon that occurs in flowering plants and mammals. Flowering plant imprinted gene expression has been described primarily in endosperm, a terminal nutritive tissue consumed by the embryo during seed development or after germination. Imprinted expression in Arabidopsis thaliana endosperm is orchestrated by differences in cytosine DNA methylation between the paternal and maternal genomes as well as by Polycomb group proteins. Currently, only 11 imprinted A. thaliana genes are known. Here, we use extensive sequencing of cDNA libraries to identify 9 paternally expressed and 34 maternally expressed imprinted genes in A. thaliana endosperm that are regulated by the DNA-demethylating glycosylase DEMETER, the DNA methyltransferase MET1, and/or the core Polycomb group protein FIE. These genes encode transcription factors, proteins involved in hormone signaling, components of the ubiquitin protein degradation pathway, regulators of histone and DNA methylation, and small RNA pathway proteins. We also identify maternally expressed genes that may be regulated by unknown mechanisms or deposited from maternal tissues. We did not detect any imprinted genes in the embryo. Our results show that imprinted gene expression is an extensive mechanistically complex phenomenon that likely affects multiple aspects of seed development.

Balancing parental contributions in plant embryonic gene activation - Zilberman, Daniel (Developmental Cell)
Little is known about chromatin remodeling events immediately after fertilization. A recent report by Autran et al. (2011) in Cell now shows that chromatin regulatory pathways that silence transposable elements are responsible for global delayed activation of gene expression in the early Arabidopsis embryo.

Incremental-decremental algorithm for computing AT-models and persistent homology - Gonzalez-Diaz, Rocio; Ion, Adrian; Jimenez, Maria Jose; Poyatos, Regina (Computer Analysis of Images and Patterns)
In this paper, we establish a correspondence between the incremental algorithm for computing AT-models [8,9] and the one for computing persistent homology [6,14,15]. We also present a decremental algorithm for computing AT-models that allows to extend the persistence computation to a wider setting. Finally, we show how to combine incremental and decremental techniques for persistent homology computation.

Effect of oceanographic barriers and overfishing on the population genetic structure of the European spiny lobster Palinurus elephas - Palero, Ferran; Abello, Pere; Macpherson, Enrique; Beaumont, Mark; Pascual, Marta (Biological Journal of the Linnean Society)
Defining population structure and genetic diversity levels is of the utmost importance for developing efficient conservation strategies. Overfishing has caused mean annual catches of the European spiny lobster (Palinurus elephas) to decrease alarmingly along its distribution area. In this context, there is a need for comprehensive studies aiming to evaluate the genetic health of the exploited populations. The present study is based on a set of ten nuclear markers amplified in 331 individuals from ten different localities covering most of P. elephas distribution area. Samples from Atlantic and Mediterranean basins showed small but significant differences, indicating that P. elephas populations do not behave as a single panmictic unit but form two partially-overlapping groups. Despite intense overfishing, our dataset did not recover a recent bottleneck signal, and instead showed a large and stable historical effective size. This result could be accounted for by specific life-history traits (reproduction and longevity) and the limitations of molecular markers in covering recent timescales for nontemporal samples. The findings of the present study emphasize the need to integrate information on effective population sizes and life-history parameters when evaluating population connectivity levels from genetic data.

Data from: Effect of oceanographic barriers and overfishing on the population genetic structure of the European spiny lobster (Palinurus elephas) - Palero, Ferran; Abello, Pere; Macpherson, Enrique; Beaumont, Mark; Pascual, Marta
Defining population structure and genetic diversity levels is of the utmost importance for developing efficient conservation strategies. Overfishing has caused mean annual catches of the European spiny lobster (Palinurus elephas) to decrease alarmingly along its distribution area. In this context, there is a need for comprehensive studies to evaluate the genetic health of the exploited populations. The present work is based on a set of 10 nuclear markers amplified in 331 individuals from 10 different localities covering most of P. elephas distribution area. Samples from Atlantic and Mediterranean basins showed small but significant differences, indicating that P. elephas populations do not behave as a single panmictic unit but form two partially-overlapping groups. Despite intense overfishing, our dataset did not recover a recent bottleneck signal, and showed a large and stable historical effective size instead. This result could be accounted for by specific life history traits (reproduction and longevity) and the limitations of molecular markers in covering very recent timescales for non temporal samples. Our study emphasizes the necessity of integrating information on effective population sizes and life history parameters when evaluating population connectivity levels from genetic data.

Ilastik: Interactive learning and segmentation toolkit - Sommer, Christoph M; Straehle, Christoph; Köthe, Ullrich; Hamprecht, Fred A. (2011 IEEE International Symposium on Biomedical Imaging: from Nano to Micro)
Segmentation is the process of partitioning digital images into meaningful regions. The analysis of biological high content images often requires segmentation as a first step. We propose ilastik as an easy-to-use tool which allows the user without expertise in image processing to perform segmentation and classification in a unified way. ilastik learns from labels provided by the user through a convenient mouse interface. Based on these labels, ilastik infers a problem specific segmentation. A random forest classifier is used in the learning step, in which each pixel's neighborhood is characterized by a set of generic (nonlinear) features. ilastik supports up to three spatial plus one spectral dimension and makes use of all dimensions in the feature calculation. ilastik provides realtime feedback that enables the user to interactively refine the segmentation result and hence further fine-tune the classifier. An uncertainty measure guides the user to ambiguous regions in the images. Real time performance is achieved by multi-threading which fully exploits the capabilities of modern multi-core machines. Once a classifier has been trained on a set of representative images, it can be exported and used to automatically process a very large number of images (e.g. using the CellProfiler pipeline). ilastik is an open source project and released under the BSD license at www.ilastik.org.
Keywords: image segmentation; biomedical imaging; three dimensional displays; neurons; retina; observers; image color analysis

Spatio-temporal extraction of articulated models in a graph pyramid - Artner, Nicole M.; Ion, Adrian; Kropatsch, Walter G. (Graph-Based Representations in Pattern Recognition)
This paper presents a method to create a model of an articulated object using the planar motion in an initialization video. The model consists of rigid parts connected by points of articulation. The rigid parts are described by the positions of salient feature-points tracked throughout the video. Following a filtering step that identifies points that belong to different objects, rigid parts are found by a grouping process in a graph pyramid. Valid articulation points are selected by verifying multiple hypotheses for each pair of parts.

The role of chemotactic gradients in dendritic cell migration - Schumann, Kathrin
Chemokines organize immune cell trafficking by inducing either directed (tactic) or random (kinetic) migration and by activating integrins in order to support surface adhesion (haptic). Beyond that the same chemokines can establish clearly defined functional areas in secondary lymphoid organs. Until now it is unclear how chemokines can fulfill such diverse functions. One decisive prerequisite to explain these capacities is to know how chemokines are presented in tissue. In theory chemokines could occur either soluble or immobilized, and could be distributed either homogenously or as a concentration gradient. To dissect if and how the presenting mode of chemokines influences immune cells, I tested the response of dendritic cells (DCs) to differentially displayed chemokines. DCs are antigen presenting cells that reside in the periphery and migrate into draining lymph nodes (LNs) once exposed to inflammatory stimuli to activate naïve T cells. DCs are guided to and within the LN by the chemokine receptor CCR7, which has two ligands, the chemokines CCL19 and CCL21. Both CCR7 ligands are expressed by fibroblastic reticular cells in the LN, but differ in their ability to bind to heparan sulfate residues. CCL21 has a highly charged C-terminal extension, which mediates binding to anionic surfaces, whereas CCL19 is lacking such residues and likely distributes as a soluble molecule. This study shows that surface-bound CCL21 causes random, haptokinetic DC motility, which is confined to the chemokine coated area by insideout activation of β2 integrins that mediate cell binding to the surface. CCL19 on the other hand forms concentration gradients which trigger directional, chemotactic movement, but no surface adhesion. In addition DCs can actively manipulate this system by recruiting and activating serine proteases on their surfaces, which create - by proteolytically removing the adhesive C-terminus - a solubilized variant of CCL21 that functionally resembles CCL19. By generating a CCL21 concentration gradient DCs establish a positive feedback loop to recruit further DCs from the periphery to the CCL21 coated region. In addition DCs can sense chemotactic gradients as well as immobilized haptokinetic fields at the same time and integrate these signals. The result is chemotactically biased haptokinesis - directional migration confined to a chemokine coated track or area - which could explain the dynamic but spatially tightly controlled swarming leukocyte locomotion patterns that have been observed in lymphatic organs by intravital microscopists. The finding that DCs can approach soluble cues in a non-adhesive manner while they attach to surfaces coated with immobilized cues raises the question how these cells transmit intracellular forces to the environment, especially in the non-adherent migration mode. In order to migrate, cells have to generate and transmit force to the extracellular substrate. Force transmission is the prerequisite to procure an expansion of the leading edge and a forward motion of the whole cell body. In the current conceptions actin polymerization at the leading edge is coupled to extracellular ligands via the integrin family of transmembrane receptors, which allows the transmission of intracellular force. Against the paradigm of force transmission during migration, leukocytes, like DCs, are able to migrate in threedimensional environments without using integrin transmembrane receptors (Lämmermann et al., 2008). This reflects the biological function of leukocytes, as they can invade almost all tissues, whereby their migration has to be independent from the extracellular environment. How the cells can achieve this is unclear. For this study I examined DC migration in a defined threedimensional environment and highlighted actin-dynamics with the probe Lifeact-GFP. The result was that chemotactic DCs can switch between integrin-dependent and integrin- independent locomotion and can thereby adapt to the adhesive properties of their environment. If the cells are able to couple their actin cytoskeleton to the substrate, actin polymerization is entirely converted into protrusion. Without coupling the actin cortex undergoes slippage and retrograde actin flow can be observed. But retrograde actin flow can be completely compensated by higher actin polymerization rate keeping the migration velocity and the shape of the cells unaltered. Mesenchymal cells like fibroblast cannot balance the loss of adhesive interaction, cannot protrude into open space and, therefore, strictly depend on integrinmediated force coupling. This leukocyte specific phenomenon of “adaptive force transmission” endows these cells with the unique ability to transit and invade almost every type of tissue.

Mechanics of adhesion and de‐adhesion in zebrafish germ layer progenitors - Maître, Jean-Léon

In vivo analysis of uropod function during physiological T cell trafficking - Soriano, Silvia; Hons, Miroslav; Schumann, Kathrin; Kumar, Varsha; Dennier, Timo; Lyck, Ruth; Sixt, Michael K; Stein, Jens (Journal of Immunology)
Migrating lymphocytes acquire a polarized phenotype with a leading and a trailing edge, or uropod. Although in vitro experiments in cell lines or activated primary cell cultures have established that Rho-p160 coiled-coil kinase (ROCK)-myosin II-mediated uropod contractility is required for integrin de-adhesion on two-dimensional surfaces and nuclear propulsion through narrow pores in three-dimensional matrices, less is known about the role of these two events during the recirculation of primary, nonactivated lymphocytes. Using pharmacological antagonists of ROCK and myosin II, we report that inhibition of uropod contractility blocked integrin-independent mouse T cell migration through narrow, but not large, pores in vitro. T cell crawling on chemokine-coated endothelial cells under shear was severely impaired by ROCK inhibition, whereas transendothelial migration was only reduced through endothelial cells with high, but not low, barrier properties. Using three-dimensional thick-tissue imaging and dynamic two-photon microscopy of T cell motility in lymphoid tissue, we demonstrated a significant role for uropod contractility in intraluminal crawling and transendothelial migration through lymph node, but not bone marrow, endothelial cells. Finally, we demonstrated that ICAM-1, but not anatomical constraints or integrin-independent interactions, reduced parenchymal motility of inhibitor-treated T cells within the dense lymphoid microenvironment, thus assigning context-dependent roles for uropod contraction during lymphocyte recirculation.

Maximum margin multi-label structured prediction - Lampert, Christoph
We study multi-label prediction for structured output sets, a problem that occurs, for example, in object detection in images, secondary structure prediction in computational biology, and graph matching with symmetries. Conventional multilabel classification techniques are typically not applicable in this situation, because they require explicit enumeration of the label set, which is infeasible in case of structured outputs. Relying on techniques originally designed for single-label structured prediction, in particular structured support vector machines, results in reduced prediction accuracy, or leads to infeasible optimization problems. In this work we derive a maximum-margin training formulation for multi-label structured prediction that remains computationally tractable while achieving high prediction accuracy. It also shares most beneficial properties with single-label maximum-margin approaches, in particular formulation as a convex optimization problem, efficient working set training, and PAC-Bayesian generalization bounds.

Maximum margin multi label structured prediction - Lampert, Christoph (NIPS: Neural Information Processing Systems)
We study multi-label prediction for structured output spaces, a problem that occurs, for example, in object detection in images, secondary structure prediction in computational biology, and graph matching with symmetries. Conventional multi-label classification techniques are typically not applicable in this situation, because they require explicit enumeration of the label space, which is infeasible in case of structured outputs. Relying on techniques originally designed for single- label structured prediction, in particular structured support vector machines, results in reduced prediction accuracy, or leads to infeasible optimization problems. In this work we derive a maximum-margin training formulation for multi-label structured prediction that remains computationally tractable while achieving high prediction accuracy. It also shares most beneficial properties with single-label maximum-margin approaches, in particular a formulation as a convex optimization problem, efficient working set training, and PAC-Bayesian generalization bounds.

Structured learning and prediction in computer vision - Nowozin, Sebastian; Lampert, Christoph (Foundations and Trends in Computer Graphics and Vision)
Powerful statistical models that can be learned efficiently from large amounts of data are currently revolutionizing computer vision. These models possess a rich internal structure reflecting task-specific relations and constraints. This monograph introduces the reader to the most popular classes of structured models in computer vision. Our focus is discrete undirected graphical models which we cover in detail together with a description of algorithms for both probabilistic inference and maximum a posteriori inference. We discuss separately recently successful techniques for prediction in general structured models. In the second part of this monograph we describe methods for parameter learning where we distinguish the classic maximum likelihood based methods from the more recent prediction-based parameter learning methods. We highlight developments to enhance current models and discuss kernelized models and latent variable models. To make the monograph more practical and to provide links to further study we provide examples of successful application of many methods in the computer vision literature.

Learning multi-view neighborhood preserving projections - Quadrianto, Novi; Lampert, Christoph
We address the problem of metric learning for multi-view data, namely the construction of embedding projections from data in different representations into a shared feature space, such that the Euclidean distance in this space provides a meaningful within-view as well as between-view similarity. Our motivation stems from the problem of cross-media retrieval tasks, where the availability of a joint Euclidean distance function is a pre-requisite to allow fast, in particular hashing-based, nearest neighbor queries. We formulate an objective function that expresses the intuitive concept that matching samples are mapped closely together in the output space, whereas non-matching samples are pushed apart, no matter in which view they are available. The resulting optimization problem is not convex, but it can be decomposed explicitly into a convex and a concave part, thereby allowing efficient optimization using the convex-concave procedure. Experiments on an image retrieval task show that nearest-neighbor based cross-view retrieval is indeed possible, and the proposed technique improves the retrieval accuracy over baseline techniques.

Measuring the complete force field of an optical trap - Jahnel, Marcus; Behrndt, Martin; Jannasch, Anita; Schaeffer, Erik; Grill, Stephan (Optics Letters)
The use of optical traps to measure or apply forces on the molecular level requires a precise knowledge of the trapping force field. Close to the trap center, this field is typically approximated as linear in the displacement of the trapped microsphere. However, applications demanding high forces at low laser intensities can probe the light-microsphere interaction beyond the linear regime. Here, we measured the full nonlinear force and displacement response of an optical trap in two dimensions using a dual-beam optical trap setup with back-focal-plane photodetection. We observed a substantial stiffening of the trap beyond the linear regime that depends on microsphere size, in agreement with Mie theory calculations. Surprisingly, we found that the linear detection range for forces exceeds the one for displacement by far. Our approach allows for a complete calibration of an optical trap.

The statistical mechanics of a polygenic character under stabilizing selection mutation and drift - de Vladar, Harold; Barton, Nicholas H (Journal of the Royal Society Interface)
By exploiting an analogy between population genetics and statistical mechanics, we study the evolution of a polygenic trait under stabilizing selection, mutation and genetic drift. This requires us to track only four macroscopic variables, instead of the distribution of all the allele frequencies that influence the trait. These macroscopic variables are the expectations of: the trait mean and its square, the genetic variance, and of a measure of heterozygosity, and are derived from a generating function that is in turn derived by maximizing an entropy measure. These four macroscopics are enough to accurately describe the dynamics of the trait mean and of its genetic variance (and in principle of any other quantity). Unlike previous approaches that were based on an infinite series of moments or cumulants, which had to be truncated arbitrarily, our calculations provide a well-defined approximation procedure. We apply the framework to abrupt and gradual changes in the optimum, as well as to changes in the strength of stabilizing selection. Our approximations are surprisingly accurate, even for systems with as few as five loci. We find that when the effects of drift are included, the expected genetic variance is hardly altered by directional selection, even though it fluctuates in any particular instance. We also find hysteresis, showing that even after averaging over the microscopic variables, the macroscopic trajectories retain a memory of the underlying genetic states.

Spatial waves of advance with bistable dynamics: Cytoplasmic and genetic analogues of Allee effects - Barton, Nicholas H; Turelli, Michael (American Naturalist)
Unlike unconditionally advantageous “Fisherian” variants that tend to spread throughout a species range once introduced anywhere, “bistable” variants, such as chromosome translocations, have two alternative stable frequencies, absence and (near) fixation. Analogous to populations with Allee effects, bistable variants tend to increase locally only once they become sufficiently common, and their spread depends on their rate of increase averaged over all frequencies. Several proposed manipulations of insect populations, such as using Wolbachia or “engineered underdominance” to suppress vector-borne diseases, produce bistable rather than Fisherian dynamics. We synthesize and extend theoretical analyses concerning three features of their spatial behavior: rate of spread, conditions to initiate spread from a localized introduction, and wave stopping caused by variation in population densities or dispersal rates. Unlike Fisherian variants, bistable variants tend to spread spatially only for particular parameter combinations and initial conditions. Wave initiation requires introduction over an extended region, while subsequent spatial spread is slower than for Fisherian waves and can easily be halted by local spatial inhomogeneities. We present several new results, including robust sufficient conditions to initiate (and stop) spread, using a one-parameter cubic approximation applicable to several models. The results have both basic and applied implications.

ABC: Algebraic Bound Computation for loops - Blanc, Régis; Henzinger, Thomas A; Hottelier, Thibaud; Kovács, Laura (Logic for Programming, Artificial Intelligence, and Reasoning)
We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of nested program loops. The system combines static analysis of programs with symbolic summation techniques to derive loop invariant relations between program variables. Iteration bounds are obtained from the inferred invariants, by replacing variables with bounds on their greatest values. We have successfully applied ABC to a large number of examples. The derived symbolic bounds express non-trivial polynomial relations over loop variables. We also report on results to automatically infer symbolic expressions over harmonic numbers as upper bounds on loop iteration counts.

Accuracy of phylogeny reconstruction methods combining overlapping gene data sets - Kupczok, Anne; Schmidt, Heiko; Von Haeseler, Arndt (Algorithms for Molecular Biology)
Background: The availability of many gene alignments with overlapping taxon sets raises the question of which strategy is the best to infer species phylogenies from multiple gene information. Methods and programs abound that use the gene alignment in different ways to reconstruct the species tree. In particular, different methods combine the original data at different points along the way from the underlying sequences to the final tree. Accordingly, they are classified into superalignment, supertree and medium-level approaches. Here, we present a simulation study to compare different methods from each of these three approaches. Results: We observe that superalignment methods usually outperform the other approaches over a wide range of parameters including sparse data and gene-specific evolutionary parameters. In the presence of high incongruency among gene trees, however, other combination methods show better performance than the superalignment approach. Surprisingly, some supertree and medium-level methods exhibit, on average, worse results than a single gene phylogeny with complete taxon information. Conclusions: For some methods, using the reconstructed gene tree as an estimation of the species tree is superior to the combination of incomplete information. Superalignment usually performs best since it is less susceptible to stochastic error. Supertree methods can outperform superalignment in the presence of gene-tree conflict.

Hardness results for homology localization - Chen, Chao; Freedman, Daniel (Proceedings of the 2010 Annual ACM-SIAM Symposium on Discrete Algorithms)
We address the problem of localizing homology classes, namely, finding the cycle representing a given class with the most concise geometric measure. We focus on the volume measure, that is, the 1-norm of a cycle. Two main results are presented. First, we prove the problem is NP-hard to approximate within any constant factor. Second, we prove that for homology of dimension two or higher, the problem is NP-hard to approximate even when the Betti number is O(1). A side effect is the inapproximability of the problem of computing the nonbounding cycle with the smallest volume, and computing cycles representing a homology basis with the minimal total volume. We also discuss other geometric measures (diameter and radius) and show their disadvantages in homology localization. Our work is restricted to homology over the ℤ2 field.

The rate of fitness-valley crossing in sexual populations - Weissman, Daniel; Feldman, Marcus; Fisher, Daniel (Genetics)
Biological traits result in part from interactions between different genetic loci. This can lead to sign epistasis, in which a beneficial adaptation involves a combination of individually deleterious or neutral mutations; in this case, a population must cross a “fitness valley” to adapt. Recombination can assist this process by combining mutations from different individuals or retard it by breaking up the adaptive combination. Here, we analyze the simplest fitness valley, in which an adaptation requires one mutation at each of two loci to provide a fitness benefit. We present a theoretical analysis of the effect of recombination on the valley-crossing process across the full spectrum of possible parameter regimes. We find that low recombination rates can speed up valley crossing relative to the asexual case, while higher recombination rates slow down valley crossing, with the transition between the two regimes occurring when the recombination rate between the loci is approximately equal to the selective advantage provided by the adaptation. In large populations, if the recombination rate is high and selection against single mutants is substantial, the time to cross the valley grows exponentially with population size, effectively meaning that the population cannot acquire the adaptation. Recombination at the optimal (low) rate can reduce the valley-crossing time by up to several orders of magnitude relative to that in an asexual population.

Investigating temporal changes in hybridisation and introgression between invasive sika (Cervus nippon) and native red deer (Cervus elaphus) on the Kintyre Peninsula, Scotland - Senn, Helen; Goodman, Simon; Swanson, Graeme; Barton, Nicholas H; Pemberton, Josephine (Molecular Ecology)
We investigated temporal changes in hybridization and introgression between native red deer (Cervus elaphus) and invasive Japanese sika (Cervus nippon) on the Kintyre Peninsula, Scotland, over 15 years, through analysis of 1513 samples of deer at 20 microsatellite loci and a mtDNA marker. We found no evidence that either the proportion of recent hybrids, or the levels of introgression had changed over the study period. Nevertheless, in one population where the two species have been in contact since ∼1970, 44% of individuals sampled during the study were hybrids. This suggests that hybridization between these species can proceed fairly rapidly. By analysing the number of alleles that have introgressed from polymorphic red deer into the genetically homogenous sika population, we reconstructed the haplotypes of red deer alleles introduced by backcrossing. Five separate hybridization events could account for all the recently hybridized sika-like individuals found across a large section of the Peninsula. Although we demonstrate that low rates of F1 hybridization can lead to substantial introgression, the progress of hybridization and introgression appears to be unpredictable over the short timescales.

Lumpability abstractions of rule-based systems - Feret, Jérôme; Henzinger, Thomas A; Koeppl, Heinz; Petrov, Tatjana
The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a math- ematical model is an important challenge in systems biology. Exploiting the limited context on which most binding and modification events are conditioned, attempts have been made to reduce the com- binatorial complexity by quotienting the reachable set of molecular species, into species aggregates while preserving the deterministic semantics of the thermodynamic limit. Recently we proposed a quotienting that also preserves the stochastic semantics and that is complete in the sense that the semantics of individual species can be recovered from the aggregate semantics. In this paper we prove that this quotienting yields a sufficient condition for weak lumpability and that it gives rise to a backward Markov bisimulation between the original and aggregated transition system. We illustrate the framework on a case study of the EGF/insulin receptor crosstalk.

P2Y1 receptors inhibit long-term depression in the prefrontal cortex. - Guzmán, José; Schmidt, Hartmut; Franke, Heike; Krügel, Ute; Eilers, Jens; Illes, Peter; Gerevich, Zoltan (Neuropharmacology)
Long-term depression (LTD) is a form of synaptic plasticity that may contribute to information storage in the central nervous system. Here we report that LTD can be elicited in layer 5 pyramidal neurons of the rat prefrontal cortex by pairing low frequency stimulation with a modest postsynaptic depolarization. The induction of LTD required the activation of both metabotropic glutamate receptors of the mGlu1 subtype and voltage-sensitive Ca(2+) channels (VSCCs) of the T/R, P/Q and N types, leading to the stimulation of intracellular inositol trisphosphate (IP3) receptors by IP3 and Ca(2+). The subsequent release of Ca(2+) from intracellular stores activated the protein phosphatase cascade involving calcineurin and protein phosphatase 1. The activation of purinergic P2Y(1) receptors blocked LTD. This effect was prevented by P2Y(1) receptor antagonists and was absent in mice lacking P2Y(1) but not P2Y(2) receptors. We also found that activation of P2Y(1) receptors inhibits Ca(2+) transients via VSCCs in the apical dendrites and spines of pyramidal neurons. In addition, we show that the release of ATP under hypoxia is able to inhibit LTD by acting on postsynaptic P2Y(1) receptors. In conclusion, these data suggest that the reduction of Ca(2+) influx via VSCCs caused by the activation of P2Y(1) receptors by ATP is the possible mechanism for the inhibition of LTD in prefrontal cortex.

Microsatelight – Pipeline to expedite microsatellite analysis - Palero, Ferran; González Candelas, Fernando; Pascual, Marta (Journal of Heredity)
MICROSATELIGHT is a Perl/Tk pipeline with a graphical user interface that facilitates several tasks when scoring microsatellites. It implements new subroutines in R and PERL and takes advantage of features provided by previously developed freeware. MICROSATELIGHT takes raw genotype data and automates the peak identification through PeakScanner. The PeakSelect subroutine assigns peaks to different microsatellite markers according to their multiplex group, fluorochrome type, and size range. After peak selection, binning of alleles can be carried out 1) automatically through AlleloBin or 2) by manual bin definition through Binator. In both cases, several features for quality checking and further binning improvement are provided. The genotype table can then be converted into input files for several population genetics programs through CREATE. Finally, Hardy–Weinberg equilibrium tests and confidence intervals for null allele frequency can be obtained through GENEPOP. MICROSATELIGHT is the only freely available public-domain software that facilitates full multiplex microsatellite scoring, from electropherogram files to user-defined text files to be used with population genetics software. MICROSATELIGHT has been created for the Windows XP operating system and has been successfully tested under Windows 7. It is available at http://sourceforge.net/projects/microsatelight/.

Topology noise removal for curve and surface evolution - Chen, Chao; Freedman, Daniel (Conference proceedings MCV 2010)
In cortex surface segmentation, the extracted surface is required to have a particular topology, namely, a two-sphere. We present a new method for removing topology noise of a curve or surface within the level set framework, and thus produce a cortical surface with correct topology. We define a new energy term which quantifies topology noise. We then show how to minimize this term by computing its functional derivative with respect to the level set function. This method differs from existing methods in that it is inherently continuous and not digital; and in the way that our energy directly relates to the topology of the underlying curve or surface, versus existing knot-based measures which are related in a more indirect fashion. The proposed flow is validated empirically.

The stability of the apparent contour of an orientable 2-manifold - Edelsbrunner, Herbert; Morozov, Dmitriy; Patel, Amit (Topological Data Analysis and Visualization: Theory, Algorithms and Applications)
The (apparent) contour of a smooth mapping from a 2-manifold to the plane, f: M → R2 , is the set of critical values, that is, the image of the points at which the gradients of the two component functions are linearly dependent. Assuming M is compact and orientable and measuring difference with the erosion distance, we prove that the contour is stable.

Weakly-paired maximum covariance analysis for multimodal dimensionality reduction and transfer learning - Lampert, Christoph; Krömer, Oliver
We study the problem of multimodal dimensionality reduction assuming that data samples can be missing at training time, and not all data modalities may be present at application time. Maximum covariance analysis, as a generalization of PCA, has many desirable properties, but its application to practical problems is limited by its need for perfectly paired data. We overcome this limitation by a latent variable approach that allows working with weakly paired data and is still able to efficiently process large datasets using standard numerical routines. The resulting weakly paired maximum covariance analysis often finds better representations than alternative methods, as we show in two exemplary tasks: texture discrimination and transfer learning.

Beyond TARPs: The growing list of auxiliary AMPAR subunits - Guzmán, José; Jonas, Peter M (Neuron)
A recent paper by von Engelhardt et al. identifies a novel auxiliary subunit of native AMPARs, termedCKAMP44. Unlike other auxiliary subunits, CKAMP44 accelerates desensitization and prolongs recovery from desensitization. CKAMP44 is highly expressed in hippocampal dentate gyrus granule cells and decreases the paired-pulse ratio at perforant path input synapses. Thus, both principal and auxiliary AMPAR subunits control the time course of signaling at glutamatergic synapses.

GABA release at terminals of CCK-interneurons: synchrony, asynchrony and modulation by cannabinoid receptors (commentary on Ali & Todorova) - Jonas, Peter M; Hefft, Stefan (The European Journal of Neuroscience)

SABRE: A tool for the stochastic analysis of biochemical reaction networks - Didier, Frédéric; Henzinger, Thomas A; Mateescu, Maria; Wolf, Verena
The importance of stochasticity within biological systems has been shown repeatedly during the last years and has raised the need for efficient stochastic tools. We present SABRE, a tool for stochastic analysis of biochemical reaction networks. SABRE implements fast adaptive uniformization (FAU), a direct numerical approximation algorithm for computing transient solutions of biochemical reaction networks. Biochemical reactions networks represent biological systems studied at a molecular level and these reactions can be modeled as transitions of a Markov chain. SABRE accepts as input the formalism of guarded commands, which it interprets either as continuous-time or as discrete-time Markov chains. Besides operating in a stochastic mode, SABRE may also perform a deterministic analysis by directly computing a mean-field approximation of the system under study. We illustrate the different functionalities of SABRE by means of biological case studies.

Aligators for arrays - Henzinger, Thomas A; Hottelier, Thibaud; Kovács, Laura; Rybalchenko, Andrey
This paper presents Aligators, a tool for the generation of universally quantified array invariants. Aligators leverages recurrence solving and algebraic techniques to carry out inductive reasoning over array content. The Aligators’ loop extraction module allows treatment of multi-path loops by exploiting their commutativity and serializability properties. Our experience in applying Aligators on a collection of loops from open source software projects indicates the applicability of recurrence and algebraic solving techniques for reasoning about arrays.

Fast adaptive uniformization of the chemical master equation - Didier, Frédéric; Henzinger, Thomas A; Mateescu, Maria; Wolf, Verena (IET Systems Biology)
Within systems biology there is an increasing interest in the stochastic behavior of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equation, which represents a continuous-time Markov chain (CTMC). The uniformization technique is an efficient method to compute probability distributions of a CTMC if the number of states is manageable. However, the size of a CTMC that represents a biochemical reaction network is usually far beyond what is feasible. In this paper we present an on-the-fly variant of uniformization, where we improve the original algorithm at the cost of a small approximation error. By means of several examples, we show that our approach is particularly well-suited for biochemical reaction networks.

The robustness of level sets - Bendich, Paul; Edelsbrunner, Herbert; Morozov, Dmitriy; Patel, Amit
We define the robustness of a level set homology class of a function f:XR as the magnitude of a perturbation necessary to kill the class. Casting this notion into a group theoretic framework, we compute the robustness for each class, using a connection to extended persistent homology. The special case X=R3 has ramifications in medical imaging and scientific visualization.

The complexity of partial-observation parity games - Chatterjee, Krishnendu; Doyen, Laurent
We consider two-player zero-sum games on graphs. On the basis of the information available to the players these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have com- plete view of the game). We survey the complexity results for the problem of de- ciding the winner in various classes of partial-observation games with ω-regular winning conditions specified as parity objectives. We present a reduction from the class of parity objectives that depend on sequence of states of the game to the sub-class of parity objectives that only depend on the sequence of observations. We also establish that partial-observation acyclic games are PSPACE-complete.

Randomness for free - Chatterjee, Krishnendu; Doyen, Laurent; Gimbert, Hugo; Henzinger, Thomas A
We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided complete-observation (one player has complete observation); and (c) complete-observation (both players have complete view of the game). On the basis of mode of interaction we have the following classification: (a) concurrent (players interact simultaneously); and (b) turn-based (players interact in turn). The two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. We present a complete characterization for the classes of games where randomness is not helpful in: (a) the transition function (probabilistic transition can be simulated by deterministic transition); and (b) strategies (pure strategies are as powerful as randomized strategies). As consequence of our characterization we obtain new undecidability results for these games.

Formal modeling and analysis of timed systems
This book constitutes the proceedings of the 8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2010, held in Klosterneuburg, Austria in September 2010. The 14 papers presented were carefully reviewed and selected from 31 submissions. In addition, the volume contains 3 invited talks and 2 invited tutorials.The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share an interest in the modeling and analysis of timed systems. Typical topics include foundations and semantics, methods and tools, and applications.

Robustness in the presence of liveness - Bloem, Roderick; Chatterjee, Krishnendu; Greimel, Karin; Henzinger, Thomas A; Jobstmann, Barbara
Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees.

Algorithms for game metrics - Chatterjee, Krishnendu; De Alfaro, Luca; Majumdar, Ritankar; Raman, Vishwanath (Logical Methods in Computer Science)
Simulation and bisimulation metrics for stochastic systems provide a quantitative generalization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative mu-calculus and related probabilistic logics. We first show that the metrics provide a bound for the difference in long-run average and discounted average behavior across states, indicating that the metrics can be used both in system verification, and in performance evaluation. For turn-based games and MDPs, we provide a polynomial-time algorithm for the computation of the one-step metric distance between states. The algorithm is based on linear programming; it improves on the previous known exponential-time algorithm 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 algorithms for Markov chains. For the bisimulation kernel of the metric our algorithm works in time O(n(4)) for both turn-based games and MDPs; improving the previously best known O(n(9).log(n)) time algorithm for MDPs. For a concurrent game G, we show that computing the exact distance be tween 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 done via a reduction to the theory of real closed fields, involving a formula with three quantifier alternations, yielding O(vertical bar G vertical bar(O(vertical bar G vertical bar 5))) time complexity, improving the previously known reduction, which yielded O(vertical bar G vertical bar(O(vertical bar G vertical bar 7))) time complexity. These algorithms can be iterated to approximate the metrics using binary search

Why is adaptation prevented at ecological margins? New insights from individual-based simulations - Bridle, Jon; Polechova, Jitka; Kawata, Masakado; Butlin, Roger (Ecology Letters)
All species are restricted in their distribution. Currently, ecological models can only explain such limits if patches vary in quality, leading to asymmetrical dispersal, or if genetic variation is too low at the margins for adaptation. However, population genetic models suggest that the increase in genetic variance resulting from dispersal should allow adaptation to almost any ecological gradient. Clearly therefore, these models miss something that prevents evolution in natural populations. We developed an individual-based simulation to explore stochastic effects in these models. At high carrying capacities, our simulations largely agree with deterministic predictions. However, when carrying capacity is low, the population fails to establish for a wide range of parameter values where adaptation was expected from previous models. Stochastic or transient effects appear critical around the boundaries in parameter space between simulation behaviours. Dispersal, gradient steepness, and population density emerge as key factors determining adaptation on an ecological gradient.

A new model for evolution in a spatial continuum - Barton, Nicholas H; Etheridge, Alison; Véber, Amandine (Electronic Journal of Probability)
We investigate a new model for populations evolving in a spatial continuum. This model can be thought of as a spatial version of the Lambda-Fleming-Viot process. It explicitly incorporates both small scale reproduction events and large scale extinction-recolonisation events. The lineages ancestral to a sample from a population evolving according to this model can be described in terms of a spatial version of the Lambda-coalescent. Using a technique of Evans (1997), we prove existence and uniqueness in law for the model. We then investigate the asymptotic behaviour of the genealogy of a finite number of individuals sampled uniformly at random (or more generally `far enough apart') from a two-dimensional torus of sidelength L as L tends to infinity. Under appropriate conditions (and on a suitable timescale) we can obtain as limiting genealogical processes a Kingman coalescent, a more general Lambda-coalescent or a system of coalescing Brownian motions (with a non-local coalescence mechanism).

Handbuch Bibliothek 2.0
With the term "Library 2.0" the editors mean an institution which applies the principles of the Web 2.0 such as openness, re-use, collaboration and interaction in the entire organization. Libraries are extending their service offerings and work processes to include the potential of Web 2.0 technologies. This changes the job description and self-image of librarians. The collective volume offers a complete overview of the topic Library 2.0 and the current state of developments from a technological, sociological, information theoretical and practice-oriented perspective.

From MTL to deterministic timed automata - Nickovic, Dejan; Piterman, Nir
In this paper we propose a novel technique for constructing timed automata from properties expressed in the logic mtl, under bounded-variability assumptions. We handle full mtl and include all future operators. Our construction is based on separation of the continuous time monitoring of the input sequence and discrete predictions regarding the future. The separation of the continuous from the discrete allows us to determinize our automata in an exponential construction that does not increase the number of clocks. This leads to a doubly exponential construction from mtl to deterministic timed automata, compared with triply exponential using existing approaches. We offer an alternative to the existing approach to linear real-time model checking, which has never been implemented. It further offers a unified framework for model checking, runtime monitoring, and synthesis, in an approach that can reuse tools, implementations, and insights from the discrete setting.

Genetic linkage and natural selection - Barton, Nicholas H (Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences)
The prevalence of recombination in eukaryotes poses one of the most puzzling questions in biology. The most compelling general explanation is that recombination facilitates selection by breaking down the negative associations generated by random drift (i.e. Hill-Robertson interference, HRI). I classify the effects of HRI owing to: deleterious mutation, balancing selection and selective sweeps on: neutral diversity, rates of adaptation and the mutation load. These effects are mediated primarily by the density of deleterious mutations and of selective sweeps. Sequence polymorphism and divergence suggest that these rates may be high enough to cause significant interference even in genomic regions of high recombination. However, neither seems able to generate enough variance in fitness to select strongly for high rates of recombination. It is plausible that spatial and temporal fluctuations in selection generate much more fitness variance, and hence selection for recombination, than can be explained by uniformly deleterious mutations or species-wide selective sweeps.

What role does natural selection play in speciation? - Barton, Nicholas H (Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences)
If distinct biological species are to coexist in sympatry, they must be reproductively isolated and must exploit different limiting resources. A two-niche Levene model is analysed, in which habitat preference and survival depend on underlying additive traits. The population genetics of preference and viability are equivalent. However, there is a linear trade-off between the chances of settling in either niche, whereas viabilities may be constrained arbitrarily. With a convex trade-off, a sexual population evolves a single generalist genotype, whereas with a concave trade-off, disruptive selection favours maximal variance. A pure habitat preference evolves to global linkage equilibrium if mating occurs in a single pool, but remarkably, evolves to pairwise linkage equilibrium within niches if mating is within those niches--independent of the genetics. With a concave trade-off, the population shifts sharply between a unimodal distribution with high gene flow and a bimodal distribution with strong isolation, as the underlying genetic variance increases. However, these alternative states are only simultaneously stable for a narrow parameter range. A sharp threshold is only seen if survival in the 'wrong' niche is low; otherwise, strong isolation is impossible. Gene flow from divergent demes makes speciation much easier in parapatry than in sympatry.

Mutation and the evolution of recombination - Barton, Nicholas H (Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences)
Under the classical view, selection depends more or less directly on mutation: standing genetic variance is maintained by a balance between selection and mutation, and adaptation is fuelled by new favourable mutations. Recombination is favoured if it breaks negative associations among selected alleles, which interfere with adaptation. Such associations may be generated by negative epistasis, or by random drift (leading to the Hill-Robertson effect). Both deterministic and stochastic explanations depend primarily on the genomic mutation rate, U. This may be large enough to explain high recombination rates in some organisms, but seems unlikely to be so in general. Random drift is a more general source of negative linkage disequilibria, and can cause selection for recombination even in large populations, through the chance loss of new favourable mutations. The rate of species-wide substitutions is much too low to drive this mechanism, but local fluctuations in selection, combined with gene flow, may suffice. These arguments are illustrated by comparing the interaction between good and bad mutations at unlinked loci under the infinitesimal model.

Phenotypic correlates of hybridisation between red and sika deer (genus Cervus) - Senn, Helen; Swanson, Graeme; Goodman, Simon; Barton, Nicholas H; Pemberton, Josephine (Journal of Animal Ecology)
1. Hybridisation with an invasive species has the potential to alter the phenotype and hence the ecology of a native counterpart. 2. Here data from populations of native red deer Cervus elaphus and invasive sika deer Cervus nippon in Scotland is used to assess the extent to which hybridisation between them is causing phenotypic change. This is done by regression of phenotypic traits against genetic hybrid scores. 3. Hybridisation is causing increases in the body weight of sika-like deer and decreases in the body weight of red-like females. Hybridisation is causing increases in jaw length and increases in incisor arcade breadth in sika-like females. Hybridisation is also causing decreases in incisor arcade breadth in red-like females. 4. There is currently no evidence that hybridisation is causing changes in the kidney fat weight or pregnancy rates of either population. 5. Increased phenotypic similarity between the two species is likely to lead to further hybridisation. The ecological consequences of this are difficult to predict.

Understanding adaptation in large populations - Barton, Nicholas H (PLoS Genetics)

Control of directed cell migration in vivo by membrane-to-cortex attachment - Diz Muñoz, Alba; Krieg, Michael; Bergert, Martin; Ibarlucea Benitez, Itziar; Müller, Daniel; Paluch, Ewa; Heisenberg, Carl-Philipp J (PLoS Biology)
Cell shape and motility are primarily controlled by cellular mechanics. The attachment of the plasma membrane to the underlying actomyosin cortex has been proposed to be important for cellular processes involving membrane deformation. However, little is known about the actual function of membrane-to-cortex attachment (MCA) in cell protrusion formation and migration, in particular in the context of the developing embryo. Here, we use a multidisciplinary approach to study MCA in zebrafish mesoderm and endoderm (mesendoderm) germ layer progenitor cells, which migrate using a combination of different protrusion types, namely, lamellipodia, filopodia, and blebs, during zebrafish gastrulation. By interfering with the activity of molecules linking the cortex to the membrane and measuring resulting changes in MCA by atomic force microscopy, we show that reducing MCA in mesendoderm progenitors increases the proportion of cellular blebs and reduces the directionality of cell migration. We propose that MCA is a key parameter controlling the relative proportions of different cell protrusion types in mesendoderm progenitors, and thus is key in controlling directed migration during gastrulation.

On parameter learning in CRF-based approaches to object class image segmentation - Nowozin, Sebastian; Gehler, Peter; Lampert, Christoph
Recent progress in per-pixel object class labeling of natural images can be attributed to the use of multiple types of image features and sound statistical learning approaches. Within the latter, Conditional Random Fields (CRF) are prominently used for their ability to represent interactions between random variables. Despite their popularity in computer vision, parameter learning for CRFs has remained difficult, popular approaches being cross-validation and piecewise training. In this work, we propose a simple yet expressive tree-structured CRF based on a recent hierarchical image segmentation method. Our model combines and weights multiple image features within a hierarchical representation and allows simple and efficient globally-optimal learning of ≈ 105 parameters. The tractability of our model allows us to pose and answer some of the open questions regarding parameter learning applying to CRF-based approaches. The key findings for learning CRF models are, from the obvious to the surprising, i) multiple image features always help, ii) the limiting dimension with respect to current models is the amount of training data, iii) piecewise training is competitive, iv) current methods for max-margin training fail for models with many parameters.

Stereotypical cell division orientation controls neural rod midline formation in zebrafish - Quesada-Hernández, Elena; Caneparo, Luca; Schneider, Sylvia; Winkler, Sylke; Liebling, Michael; Fraser, Scott; Heisenberg, Carl-Philipp J (Current Biology)
The development of multicellular organisms is dependent on the tight coordination between tissue growth and morphogenesis. The stereotypical orientation of cell divisions has been proposed to be a fundamental mechanism by which proliferating and growing tissues take shape. However, the actual contribution of stereotypical division orientation (SDO) to tissue morphogenesis is unclear. In zebrafish, cell divisions with stereotypical orientation have been implicated in both body-axis elongation and neural rod formation [1, 2], although there is little direct evidence for a critical function of SDO in either of these processes. Here we show that SDO is required for formation of the neural rod midline during neurulation but dispensable for elongation of the body axis during gastrulation. Our data indicate that SDO during both gastrulation and neurulation is dependent on the noncanonical Wnt receptor Frizzled 7 (Fz7) and that interfering with cell division orientation leads to severe defects in neural rod midline formation but not body-axis elongation. These findings suggest a novel function for Fz7-controlled cell division orientation in neural rod midline formation during neurulation.

DNA extraction from formalin-fixed tissue: new light from the deep sea - Palero, Ferran; Hall, Sally; Clark, Paul; Johnston, David; Mackenzie Dodds, Jackie; Thatje, Sven (Scientia Marina)
DNA samples were extracted from ethanol and formalin-fixed decapod crustacean tissue using a new method based on Tetramethylsilane (TMS)-Chelex. It is shown that neither an indigestible matrix of cross-linked protein nor soluble PCR inhibitors impede PCR success when dealing with formalin-fixed material. Instead, amplification success from formalin-fixed tissue appears to depend on the presence of unmodified DNA in the extracted sample. A staining method that facilitates the targeting of samples with a high content of unmodified DNA is provided.

Finite-size corrections to scaling behavior in sorted cell aggregates - Klopper, Abigail; Krens, Gabriel; Grill, Stephan; Heisenberg, Carl-Philipp J (The European Physical Journal E: Soft Matter and Biological Physics)
Cell sorting is a widespread phenomenon pivotal to the early development of multicellular organisms. In vitro cell sorting studies have been instrumental in revealing the cellular properties driving this process. However, these studies have as yet been limited to two-dimensional analysis of three-dimensional cell sorting events. Here we describe a method to record the sorting of primary zebrafish ectoderm and mesoderm germ layer progenitor cells in three dimensions over time, and quantitatively analyze their sorting behavior using an order parameter related to heterotypic interface length. We investigate the cell population size dependence of sorted aggregates and find that the germ layer progenitor cells engulfed in the final configuration display a relationship between total interfacial length and system size according to a simple geometrical argument, subject to a finite-size effect.

Final-stage phyllosoma of Palinustus A. Milne-Edwards, 1880 (Crustacea: Decapoda: Achelata: Palinuridae)-The first complete description - Palero, Ferran; Guerao, Guillermo; Clark, Paul; Abello, Pere (Zootaxa)
Four rare palinurid phyllosoma larvae, one mid-stage and three final stage, were found among the unclassified collections in the Crustacea Section, Natural History Museum, London. Detailed morphological analysis of the larvae indicated that they belong to several Palinustus species given the presence of incipient blunt-horns, length of antennula, length ratio of segments of antennular peduncle, distribution of pereiopod spines, and shape of uropods and telson. Moreover, the size of the final-stage larvae agrees with that expected given the size of the recently described puerulus stage of Palinustus mossambicus. This constitutes the first description of a complete phyllosoma assigned to Palinustus species. The phyllosoma described in the present study include the largest Palinuridae larva ever found.

Solving the chemical master equation using sliding windows - Wolf, Verena; Goel, Rushil; Mateescu, Maria; Henzinger, Thomas A (BMC Systems Biology)
Background The chemical master equation (CME) is a system of ordinary differential equations that describes the evolution of a network of chemical reactions as a stochastic process. Its solution yields the probability density vector of the system at each point in time. Solving the CME numerically is in many cases computationally expensive or even infeasible as the number of reachable states can be very large or infinite. We introduce the sliding window method, which computes an approximate solution of the CME by performing a sequence of local analysis steps. In each step, only a manageable subset of states is considered, representing a "window" into the state space. In subsequent steps, the window follows the direction in which the probability mass moves, until the time period of interest has elapsed. We construct the window based on a deterministic approximation of the future behavior of the system by estimating upper and lower bounds on the populations of the chemical species. Results In order to show the effectiveness of our approach, we apply it to several examples previously described in the literature. The experimental results show that the proposed method speeds up the analysis considerably, compared to a global analysis, while still providing high accuracy. Conclusions The sliding window method is a novel approach to address the performance problems of numerical algorithms for the solution of the chemical master equation. The method efficiently approximates the probability distributions at the time points of interest for a variety of chemically reacting systems, including systems for which no upper bound on the population sizes of the chemical species is known a priori.

From boolean to quantitative notions of correctness - Henzinger, Thomas A
Classical formalizations of systems and properties are boolean: given a system and a property, the property is either true or false of the system. Correspondingly, classical methods for system analysis determine the truth value of a property, preferably giving a proof if the property is true, and a counterexample if the property is false; classical methods for system synthesis construct a system for which a property is true; classical methods for system transformation, composition, and abstraction aim to preserve the truth of properties. The boolean view is prevalent even if the system, the property, or both refer to numerical quantities, such as the times or probabilities of events. For example, a timed automaton either satisfies or violates a formula of a real-time logic; a stochastic process either satisfies or violates a formula of a probabilistic logic. The classical black-and-white view partitions the world into "correct" and "incorrect" systems, offering few nuances. In reality, of several systems that satisfy a property in the boolean sense, often some are more desirable than others, and of the many systems that violate a property, usually some are less objectionable than others. For instance, among the systems that satisfy the response property that every request be granted, we may prefer systems that grant requests quickly (the quicker, the better), or we may prefer systems that issue few unnecessary grants (the fewer, the better); and among the systems that violate the response property, we may prefer systems that serve many initial requests (the more, the better), or we may prefer systems that serve many requests in the long run (the greater the fraction of served to unserved requests, the better). Formally, while a boolean notion of correctness is given by a preorder on systems and properties, a quantitative notion of correctness is defined by a directed metric on systems and properties, where the distance between a system and a property provides a measure of "fit" or "desirability." There are many ways how such distances can be defined. In a linear-time framework, one assigns numerical values to individual behaviors before assigning values to systems and properties, which are sets of behaviors. For example, the value of a single behavior may be a discounted value, which is largely determined by a prefix of the behavior, e.g., by the number of requests that are granted before the first request that is not granted; or a limit value, which is independent of any finite prefix. A limit value may be an average, such as the average response time over an infinite sequence of requests and grants, or a supremum, such as the worst-case response time. Similarly, the value of a set of behaviors may be an extremum or an average across the values of all behaviors in the set: in this way one can measure the worst of all possible average-case response times, or the average of all possible worst-case response times, etc. Accordingly, the distance between two sets of behaviors may be defined as the worst or average difference between the values of corresponding behaviors. In summary, we propagate replacing boolean specifications for the correctness of systems with quantitative measures for the desirability of systems. In quantitative analysis, the aim is to compute the distance between a system and a property (or between two systems, or two properties); in quantitative synthesis, the objective is to construct a system that has minimal distance from a given property. Multiple quantitative measures can be prioritized (e.g., combined lexicographically into a single measure) or studied along the Pareto curve. Quantitative transformations, compositions, and abstractions of systems are useful if they allow us to bound the induced change in distance from a property. We present some initial results in some of these directions. We also give some potential applications, which not only generalize tradiditional correctness concerns in the functional, timed, and probabilistic domains, but also capture such system measures as resource use, performance, cost, reliability, and robustness.

Invariant and type inference for matrices - Henzinger, Thomas A; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei
We present a loop property generation method for loops iterating over multi-dimensional arrays. When used on matrices, our method is able to infer their shapes (also called types), such as upper-triangular, diagonal, etc. To gen- erate loop properties, we first transform a nested loop iterating over a multi- dimensional array into an equivalent collection of unnested loops. Then, we in- fer quantified loop invariants for each unnested loop using a generalization of a recurrence-based invariant generation technique. These loop invariants give us conditions on matrices from which we can derive matrix types automatically us- ing theorem provers. Invariant generation is implemented in the software package Aligator and types are derived by theorem provers and SMT solvers, including Vampire and Z3. When run on the Java matrix package JAMA, our tool was able to infer automatically all matrix types describing the matrix shapes guaranteed by JAMA’s API.

Hybrid numerical solution of the chemical master equation - Henzinger, Thomas A; Mateescu, Maria; Mikeev, Linar; Wolf, Verena
We present a numerical approximation technique for the analysis of continuous-time Markov chains that describe net- works of biochemical reactions and play an important role in the stochastic modeling of biological systems. Our approach is based on the construction of a stochastic hybrid model in which certain discrete random variables of the original Markov chain are approximated by continuous deterministic variables. We compute the solution of the stochastic hybrid model using a numerical algorithm that discretizes time and in each step performs a mutual update of the transient prob- ability distribution of the discrete stochastic variables and the values of the continuous deterministic variables. We im- plemented the algorithm and we demonstrate its usefulness and efficiency on several case studies from systems biology.

Mean-payoff automaton expressions - Chatterjee, Krishnendu; Doyen, Laurent; Edelsbrunner, Herbert; Henzinger, Thomas A; Rannou, Philippe
Quantitative languages are an extension of boolean languages that assign to each word a real number. Mean-payoff automata are finite automata with numerical weights on transitions that assign to each infinite path the long-run average of the transition weights. When the mode of branching of the automaton is deterministic, nondeterministic, or alternating, the corresponding class of quantitative languages is not robust as it is not closed under the pointwise operations of max, min, sum, and numerical complement. Nondeterministic and alternating mean-payoff automata are not decidable either, as the quantitative generalization of the problems of universality and language inclusion is undecidable. We introduce a new class of quantitative languages, defined by mean-payoff automaton expressions, which is robust and decidable: it is closed under the four pointwise operations, and we show that all decision problems are decidable for this class. Mean-payoff automaton expressions subsume deterministic meanpayoff automata, and we show that they have expressive power incomparable to nondeterministic and alternating mean-payoff automata. We also present for the first time an algorithm to compute distance between two quantitative languages, and in our case the quantitative languages are given as mean-payoff automaton expressions.

Persistent homology under non-uniform error - Bendich, Paul; Edelsbrunner, Herbert; Kerber, Michael; Patel, Amit
Using ideas from persistent homology, the robustness of a level set of a real-valued function is defined in terms of the magnitude of the perturbation necessary to kill the classes. Prior work has shown that the homology and robustness information can be read off the extended persistence diagram of the function. This paper extends these results to a non-uniform error model in which perturbations vary in their magnitude across the domain.

Obliging games - Chatterjee, Krishnendu; Horn, Florian; Löding, Christof
Graph games of infinite length provide a natural model for open reactive systems: one player (Eve) represents the controller and the other player (Adam) represents the environment. The evolution of the system depends on the decisions of both players. The specification for the system is usually given as an ω-regular language L over paths and Eve’s goal is to ensure that the play belongs to L irrespective of Adam’s behaviour. The classical notion of winning strategies fails to capture several interesting scenarios. For example, strong fairness (Streett) conditions are specified by a number of request-grant pairs and require every pair that is requested infinitely often to be granted infinitely often: Eve might win just by preventing Adam from making any new request, but a “better” strategy would allow Adam to make as many requests as possible and still ensure fairness. To address such questions, we introduce the notion of obliging games, where Eve has to ensure a strong condition Φ, while always allowing Adam to satisfy a weak condition Ψ. We present a linear time reduction of obliging games with two Muller conditions Φ and Ψ to classical Muller games. We consider obliging Streett games and show they are co-NP complete, and show a natural quantitative optimisation problem for obliging Streett games is in FNP. We also show how obliging games can provide new and interesting semantics for multi-player games.

Energy parity games - Chatterjee, Krishnendu; Doyen, Laurent
Energy parity games are infinite two-player turn-based games played on weighted graphs. The objective of the game combines a (qualitative) parity condition with the (quantitative) requirement that the sum of the weights (i.e., the level of energy in the game) must remain positive. Beside their own interest in the design and synthesis of resource-constrained omega-regular specifications, energy parity games provide one of the simplest model of games with combined qualitative and quantitative objective. Our main results are as follows: (a) exponential memory is sufficient and may be necessary for winning strategies in energy parity games; (b) the problem of deciding the winner in energy parity games can be solved in NP ∩ coNP; and (c) we give an algorithm to solve energy parity by reduction to energy games. We also show that the problem of deciding the winner in energy parity games is polynomially equivalent to the problem of deciding the winner in mean-payoff parity games, which can thus be solved in NP ∩ coNP. As a consequence we also obtain a conceptually simple algorithm to solve mean-payoff parity games.

Polygonal reconstruction from approximate offsets - Berberich, Eric; Halperin, Dan; Kerber, Michael; Pogalnikova, Roza
Given a polygonal shape Q with n vertices, can it be expressed, up to a tolerance ε in Hausdorff distance, as the Minkowski sum of another polygonal shape with a disk of fixed radius? If it does, we also seek a preferably simple solution shape P;P’s offset constitutes an accurate, vertex-reduced, and smoothened approximation of Q. We give a decision algorithm for fixed radius in O(nlogn) time that handles any polygonal shape. For convex shapes, the complexity drops to O(n), which is also the time required to compute a solution shape P with at most one more vertex than a vertex-minimal one.

Generalized mean-payoff and energy games - Chatterjee, Krishnendu; Doyen, Laurent; Henzinger, Thomas A; Raskin, Jean
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Generalized mean-payoff and energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of generalized energy games and show the inter- reducibility of generalized mean-payoff and energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete.

Measuring and synthesizing systems in probabilistic environments - Chatterjee, Krishnendu; Henzinger, Thomas A; Jobstmann, Barbara; Singh, Rohit
Often one has a preference order among the different systems that satisfy a given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal-synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification tinder the given input assumption, synthesize a system that optimizes the measured value. For safety specifications and measures that are defined by mean-payoff automata, the optimal-synthesis problem amounts to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be done in polynomial time. For general omega-regular specifications, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. We present some experimental results showing optimal systems that were automatically generated in this way.

Analyzing the impact of change in multi-threaded programs - Chatterjee, Krishnendu; De Alfaro, Luca; Raman, Vishwanath; Sánchez, César
We introduce a technique for debugging multi-threaded C programs and analyzing the impact of source code changes, and its implementation in the prototype tool DIRECT. Our approach uses a combination of source code instrumentation and runtime management. The source code along with a test harness is instrumented to monitor Operating System (OS) and user defined function calls. DIRECT tracks all concurrency control primitives and, optionally, data from the program. DIRECT maintains an abstract global state that combines information from every thread, including the sequence of function calls and concurrency primitives executed. The runtime manager can insert delays, provoking thread inter-leavings that may exhibit bugs that are difficult to reach otherwise. The runtime manager collects an approximation of the reachable state space and uses this approximation to assess the impact of change in a new version of the program.

Strategy construction for parity games with imperfect information - Berwanger, Dietmar; Chatterjee, Krishnendu; De Wulf, Martin; Doyen, Laurent; Henzinger, Thomas A (Information and Computation)
We consider two-player parity games with imperfect information 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. One major obstacle in adapting the classical procedure is that the complementation of attractor sets would break the invariant of downward-closedness on which the antichain representation relies. We overcome this difficulty by decomposing problem instances recursively into games with a combination of reachability, safety, and simpler parity conditions. We also report on an experimental implementation of our algorithm: to our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.

Strategy logic - Chatterjee, Krishnendu; Henzinger, Thomas A; Piterman, Nir (Information and Computation)
We introduce strategy logic, a logic that treats strategies in two-player games as explicit first-order objects. The explicit treatment of strategies allows us to specify properties of nonzero-sum games in a simple and natural way. We show that the one-alternation fragment of strategy logic is strong enough to express the existence of Nash equilibria and secure equilibria, and subsumes other logics that were introduced to reason about games, such as ATL, ATL*, and game logic. We show that strategy logic is decidable, by constructing tree automata that recognize sets of strategies. While for the general logic, our decision procedure is nonelementary, for the simple fragment that is used above we show that the complexity is polynomial in the size of the game graph and optimal in the size of the formula (ranging from polynomial to 2EXPTIME depending on the form of the formula).

Computing robustness and persistence for images - Bendich, Paul; Edelsbrunner, Herbert; Kerber, Michael (IEEE Transactions of Visualization and Computer Graphics)
We are interested in 3-dimensional images given as arrays of voxels with intensity values. Extending these values to acontinuous function, we study the robustness of homology classes in its level and interlevel sets, that is, the amount of perturbationneeded to destroy these classes. The structure of the homology classes and their robustness, over all level and interlevel sets, can bevisualized by a triangular diagram of dots obtained by computing the extended persistence of the function. We give a fast hierarchicalalgorithm using the dual complexes of oct-tree approximations of the function. In addition, we show that for balanced oct-trees, thedual complexes are geometrically realized in $R^3$ and can thus be used to construct level and interlevel sets. We apply these tools tostudy 3-dimensional images of plant root systems.