TY - GEN
AB - We present an algorithmic method for the synthesis of concurrent programs that are optimal with respect to quantitative performance measures. The input consists of a sequential sketch, that is, a program that does not contain synchronization constructs, and of a parametric performance model that assigns costs to actions such as locking, context switching, and idling. The quantitative synthesis problem is to automatically introduce synchronization constructs into the sequential sketch so that both correctness is guaranteed and worst-case (or average-case) performance is optimized. Correctness is formalized as race freedom or linearizability.
We show that for worst-case performance, the problem can be modeled
as a 2-player graph game with quantitative (limit-average) objectives, and
for average-case performance, as a 2 1/2 -player graph game (with probabilistic transitions). In both cases, the optimal correct program is derived from an optimal strategy in the corresponding quantitative game. We prove that the respective game problems are computationally expensive (NP-complete), and present several techniques that overcome the theoretical difficulty in cases of concurrent programs of practical interest.
We have implemented a prototype tool and used it for the automatic syn- thesis of programs that access a concurrent list. For certain parameter val- ues, our method automatically synthesizes various classical synchronization schemes for implementing a concurrent list, such as fine-grained locking or a lazy algorithm. For other parameter values, a new, hybrid synchronization style is synthesized, which uses both the lazy approach and coarse-grained locks (instead of standard fine-grained locks). The trade-off occurs because while fine-grained locking tends to decrease the cost that is due to waiting for locks, it increases cache size requirements.
AU - Chatterjee, Krishnendu
AU - Cerny, Pavol
AU - Henzinger, Thomas A
AU - Radhakrishna, Arjun
AU - Singh, Rohit
ID - 5388
SN - 2664-1690
TI - Quantitative synthesis for concurrent programs
ER -
TY - GEN
AB - Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of “fit” or “desirability.” We extend the simulation preorder to the quantitative setting, by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the im- plementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.
AU - Cerny, Pavol
AU - Henzinger, Thomas A
AU - Radhakrishna, Arjun
ID - 5389
SN - 2664-1690
TI - Simulation distances
ER -
TY - GEN
AB - The class of ω regular languages provide a robust specification language in verification. Every ω-regular condition can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. In this work we consider the finitary parity and Streett (fairness) conditions. We present the topological, automata-theoretic and logical characterization of finitary languages defined by finitary parity and Streett conditions. We (a) show that the finitary parity and Streett languages are Σ2-complete; (b) present a complete characterization of the expressive power of various classes of automata with finitary and infinitary conditions (in particular we show that non-deterministic finitary parity and Streett automata cannot be determinized to deterministic finitary parity or Streett automata); and (c) show that the languages defined by non-deterministic finitary parity automata exactly characterize the star-free fragment of ωB-regular languages.
AU - Chatterjee, Krishnendu
AU - Fijalkow, Nathanaël
ID - 5390
SN - 2664-1690
TI - Topological, automata-theoretic and logical characterization of finitary languages
ER -
TY - GEN
AB - Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each node consists an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free imple- mentation and proved that the corrected version is linearizable.
AU - Cerny, Pavol
AU - Radhakrishna, Arjun
AU - Zufferey, Damien
AU - Chaudhuri, Swarat
AU - Alur, Rajeev
ID - 5391
SN - 2664-1690
TI - Model checking of linearizability of concurrent list implementations
ER -
TY - CONF
AB - 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.
AU - Feret, Jérôme
AU - Henzinger, Thomas A
AU - Koeppl, Heinz
AU - Petrov, Tatjana
ID - 3719
TI - Lumpability abstractions of rule-based systems
VL - 40
ER -
TY - JOUR
AU - Barton, Nicholas H
ID - 3772
IS - 6
JF - PLoS Genetics
TI - Understanding adaptation in large populations
VL - 6
ER -
TY - JOUR
AB - 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.
AU - Barton, Nicholas H
ID - 3773
IS - 1547
JF - Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences
TI - What role does natural selection play in speciation?
VL - 365
ER -
TY - JOUR
AB - 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.
AU - Barton, Nicholas H
ID - 3776
IS - 1552
JF - Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences
TI - Genetic linkage and natural selection
VL - 365
ER -
TY - JOUR
AB - 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.
AU - Barton, Nicholas H
ID - 3777
IS - 1544
JF - Philosophical Transactions of the Royal Society of London. Series B, Biological Sciences
TI - Mutation and the evolution of recombination
VL - 365
ER -
TY - JOUR
AB - Crosses between closely related species give two contrasting results. One result is that species hybrids may be inferior to their parents, for example, being less fertile [1]. The other is that F1 hybrids may display superior performance (heterosis), for example with increased vigour [2]. Although various hypotheses have been proposed to account for these two aspects of hybridisation, their biological basis is still poorly understood [3]. To gain further insights into this issue, we analysed the role that variation in gene expression may play. We took a conserved trait, flower asymmetry in Antirrhinum, and determined the extent to which the underlying regulatory genes varied in expression among closely related species. We show that expression of both genes analysed, CYC and RAD, varies significantly between species because of cis-acting differences. By making a quantitative genotype-phenotype map, using a range of mutant alleles, we demonstrate that the species lie on a plateau in gene expression-morphology space, so that the variation has no detectable phenotypic effect. However, phenotypic differences can be revealed by shifting genotypes off the plateau through genetic crosses. Our results can be readily explained if genomes are free to evolve within an effectively neutral zone in gene expression space. The consequences of this drift will be negligible for individual loci, but when multiple loci across the genome are considered, we show that the variation may have significant effects on phenotype and fitness, causing a significant drift load. By considering these consequences for various gene-expression-fitness landscapes, we conclude that F1 hybrids might be expected to show increased performance with regard to conserved traits, such as basic physiology, but reduced performance with regard to others. Thus, our study provides a new way of explaining how various aspects of hybrid performance may arise through natural variation in gene activity.
AU - Rosas, Ulises
AU - Barton, Nicholas H
AU - Copsey, Lucy
AU - Barbier De Reuille, Pierre
AU - Coen, Enrico
ID - 3779
IS - 7
JF - PLoS Biology
TI - Cryptic variation between species and the basis of hybrid performance
VL - 8
ER -
TY - JOUR
AB - 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.
AU - Palero, Ferran
AU - Hall, Sally
AU - Clark, Paul
AU - Johnston, David
AU - Mackenzie Dodds, Jackie
AU - Thatje, Sven
ID - 3787
IS - 3
JF - Scientia Marina
TI - DNA extraction from formalin-fixed tissue: new light from the deep sea
VL - 74
ER -
TY - JOUR
AB - 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.
AU - Diz Muñoz, Alba
AU - Krieg, Michael
AU - Bergert, Martin
AU - Ibarlucea Benitez, Itziar
AU - Müller, Daniel
AU - Paluch, Ewa
AU - Heisenberg, Carl-Philipp J
ID - 3790
IS - 11
JF - PLoS Biology
TI - Control of directed cell migration in vivo by membrane-to-cortex attachment
VL - 8
ER -
TY - CONF
AB - 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.
AU - Nowozin, Sebastian
AU - Gehler, Peter
AU - Lampert, Christoph
ID - 3793
TI - On parameter learning in CRF-based approaches to object class image segmentation
VL - 6316
ER -
TY - CHAP
AB - 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.
AU - Edelsbrunner, Herbert
AU - Morozov, Dmitriy
AU - Patel, Amit
ID - 3795
T2 - Topological Data Analysis and Visualization: Theory, Algorithms and Applications
TI - The stability of the apparent contour of an orientable 2-manifold
ER -
TY - JOUR
AB - 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.
AU - Guzmán, José
AU - Jonas, Peter M
ID - 3832
IS - 1
JF - Neuron
TI - Beyond TARPs: The growing list of auxiliary AMPAR subunits
VL - 66
ER -
TY - JOUR
AB - 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.
AU - Wolf, Verena
AU - Goel, Rushil
AU - Mateescu, Maria
AU - Henzinger, Thomas A
ID - 3834
IS - 42
JF - BMC Systems Biology
TI - Solving the chemical master equation using sliding windows
VL - 4
ER -
TY - CONF
AB - 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.
AU - Henzinger, Thomas A
AU - Mateescu, Maria
AU - Mikeev, Linar
AU - Wolf, Verena
ID - 3838
TI - Hybrid numerical solution of the chemical master equation
ER -
TY - CONF
AB - 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.
AU - Henzinger, Thomas A
AU - Hottelier, Thibaud
AU - Kovács, Laura
AU - Voronkov, Andrei
ID - 3839
TI - Invariant and type inference for matrices
VL - 5944
ER -
TY - JOUR
AB - 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.
AU - Didier, Frédéric
AU - Henzinger, Thomas A
AU - Mateescu, Maria
AU - Wolf, Verena
ID - 3842
IS - 6
JF - IET Systems Biology
TI - Fast adaptive uniformization of the chemical master equation
VL - 4
ER -
TY - CONF
AB - 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.
AU - Henzinger, Thomas A
AU - Hottelier, Thibaud
AU - Kovács, Laura
AU - Rybalchenko, Andrey
ID - 3845
TI - Aligators for arrays
VL - 6397
ER -