TY - JOUR
AB - Recent studies on vertebrate homologues of the van gogh/strabismus (vang/stbm) gene, a key player in planar cell polarity signalling in Drosophila, show that vang/stbm is involved in patterning and morphogenesis during vertebrate gastrulation where it modulates two distinct Wnt signals.
AU - Heisenberg, Carl-Philipp J
AU - Tada, Masazumi
ID - 4199
IS - 4
JF - Current Biology
TI - Wnt signalling: A moving picture emerges from van gogh
VL - 12
ER -
TY - JOUR
AB - Vertebrate homologues of the Strabismus/van Gogh (stbm/vang) gene have been implicated in patterning and morphogenesis during gastrulation. Recent work shows that stbm/vang is mutated in zebrafish trilobite mutants and that stbm/vang is required for morphogenesis but not patterning during zebrafish gastrulation.
AU - Heisenberg, Carl-Philipp J
ID - 4207
IS - 19
JF - Current Biology
TI - Wnt signalling: Refocusing on Strabismus
VL - 12
ER -
TY - JOUR
AB - We have identified widerborst (wdb), a B' regulatory subunit of PP2A, as a conserved component of planar cell polarization mechanisms in both Drosophila and in zebrafish. In Drosophila, wdb acts at two steps during planar polarization of wing epithelial cells. It is required to organize tissue polarity proteins into proximal and distal cortical domains, thus determining wing hair orientation. It is also needed to generate the polarized membrane outgrowth that becomes the wing hair. Widerborst activates the catalytic subunit of PP2A and localizes to the distal side of a planar microtubule web that lies at the level of apical cell junctions. This suggests that polarized PP2A activation along the planar microtubule web is important for planar polarization. In zebrafish, two wdb homologs are required for convergent extension during gastrulation, supporting the conjecture that Drosophila planar cell polarization and vertebrate gastrulation movements are regulated by similar mechanisms.
AU - Hannus, Michael
AU - Feiguin, Fabian
AU - Heisenberg, Carl-Philipp J
AU - Eaton, Suzanne
ID - 4209
IS - 14
JF - Development
TI - Planar cell polarization requires Widerborst, a B ' regulatory subunit of protein phosphatase 2A
VL - 129
ER -
TY - JOUR
AB - We studied the effect of multilocus balancing selection on neutral nucleotide variability at linked sites by simulating a model where diallelic polymorphisms are maintained at an arbitrary number of selected loci by means of symmetric overdominance. Different combinations of alleles define different genetic backgrounds that subdivide the population and strongly affect variability. Several multilocus fitness regimes with different degrees of epistasis and gametic disequilibrium are allowed. Analytical results based on a multilocus extension of the structured coalescent predict that the expected linked neutral diversity increases exponentially with the number of selected loci and can become extremely large. Our simulation results show that although variability increases with the number of genetic backgrounds that are maintained in the population, it is reduced by random fluctuations in the frequencies of those backgrounds and does not reach high levels even in very large populations. We also show that previous results on balancing selection in single-locus systems do not extend to the multilocus scenario in a straightforward way. Different patterns of linkage disequilibrium and of the frequency spectrum of neutral mutations are expected under different degrees of epistasis. Interestingly, the power to detect balancing selection using deviations from a neutral distribution of allele frequencies seems to be diminished under the fitness regime that leads to the largest increase of variability over the neutral case. This and other results are discussed in the light of data from the Mhc.
AU - Navarro, Arcadio
AU - Nicholas Barton
ID - 4258
IS - 2
JF - Genetics
TI - The effects of multilocus balancing selection on neutral variability
VL - 161
ER -
TY - JOUR
AB - We extend current multilocus models to describe the effects of migration, recombination, selection, and nonrandom mating on sets of genes in diploids with varied modes of inheritance, allowing us to consider the patterns of nuclear and cytonuclear associations (disequilibria) under various models of migration. We show the relationship between the multilocus notation recently presented by Kirkpatrick, Johnson, and Barton (developed from previous work by Barton and Turelli) and the cytonuclear parameterization of Asmussen, Arnold, and Avise and extend this notation to describe associations between cytoplasmic elements and multiple nuclear genes. Under models with sexual symmetry, both nuclear-nuclear and cytonuclear disequilibria are equivalent. They differ, however, in cases involving some type of sexual asymmetry, which is then reflected in the asymmetric inheritance of cytoplasmic markers. An example given is the case of different migration rates in males and females; simulations using 2, 3, 4, or 5 unlinked autosomal markers with a maternally inherited cytoplasmic marker illustrate how nuclear-nuclear and cytonuclear associations can be used to separately estimate female and male migration rates. The general framework developed here allows us to investigate conditions where associations between loci with different modes of inheritance are not equivalent and to use this nonequivalence to test for deviations from simple models of admixture.
AU - Orive, Maria E
AU - Nicholas Barton
ID - 4259
IS - 3
JF - Genetics
TI - Associations between cytoplasmic and nuclear loci in hybridizing populations
VL - 162
ER -
TY - JOUR
AB - We calculate the fixation probability of a beneficial allele that arises as the result of a unique mutation in an asexual population that is subject to recurrent deleterious mutation at rate U. Our analysis is an extension of previous works, which make a biologically restrictive assumption that selection against deleterious alleles is stronger than that on the beneficial allele of interest. We show that when selection against deleterious alleles is weak, beneficial alleles that confer a selective advantage that is small relative to U have greatly reduced probabilities of fixation. We discuss the consequences of this effect for the distribution of effects of alleles fixed during adaptation. We show that a selective sweep will increase the fixation probabilities of other beneficial mutations arising during some short interval afterward. We use the calculated fixation probabilities to estimate the expected rate of fitness improvement in an asexual population when beneficial alleles arise continually at some low rate proportional to U. We estimate the rate of mutation that is optimal in the sense that it maximizes this rate of fitness improvement. Again, this analysis relaxes the assumption made previously that selection against deleterious alleles is stronger than on beneficial alleles.
AU - Johnson, Toby
AU - Nicholas Barton
ID - 4260
IS - 1
JF - Genetics
TI - The effect of deleterious alleles on adaptation in asexual populations
VL - 162
ER -
TY - JOUR
AB - Until recently, it was impracticable to identify the genes that are responsible for variation in continuous traits, or to directly observe the effects of their different alleles. Now, the abundance of genetic markers has made it possible to identify quantitative trait loci (QTL) — the regions of a chromosome or, ideally, individual sequence variants that are responsible for trait variation. What kind of QTL do we expect to find and what can our observations of QTL tell us about how organisms evolve? The key to understanding the evolutionary significance of QTL is to understand the nature of inherited variation, not in the immediate mechanistic sense of how genes influence phenotype, but, rather, to know what evolutionary forces maintain genetic variability.
AU - Nicholas Barton
AU - Keightley, Peter D
ID - 4261
JF - Nature Reviews Genetics
TI - Understanding quantitative genetic variation
VL - 3
ER -
TY - JOUR
AB - Natural populations are structured spatially into local populations and genetically into diverse ‘genetic backgrounds’ defined by different combinations of selected alleles. If selection maintains genetic backgrounds at constant frequency then neutral diversity is enhanced. By contrast, if background frequencies fluctuate then diversity is reduced. Provided that the population size of each background is large enough, these effects can be described by the structured coalescent process. Almost all the extant results based on the coalescent deal with a single selected locus. Yet we know that very large numbers of genes are under selection and that any substantial effects are likely to be due to the cumulative effects of many loci. Here, we set up a general framework for the extension of the coalescent to multilocus scenarios and we use it to study the simplest model, where strong balancing selection acting on a set of n loci maintains 2n backgrounds at constant frequencies and at linkage equilibrium. Analytical results show that the expected linked neutral diversity increases exponentially with the number of selected loci and can become extremely large. However, simulation results reveal that the structured coalescent approach breaks down when the number of backgrounds approaches the population size, because of stochastic fluctuations in background frequencies. A new method is needed to extend the structured coalescent to cases with large numbers of backgrounds.
AU - Nicholas Barton
AU - Navarro, Arcadio
ID - 4262
IS - 2
JF - Genetical Research
TI - Extending the coalescent to multilocus systems: the case of balancing selection
VL - 79
ER -
TY - JOUR
AB - We introduce a general recursion for the probability of identity in state of two individuals sampled from a population subject to mutation, migration, and random drift in a two-dimensional continuum. The recursion allows for the interactions induced by density-dependent regulation of the population, which are inevitable in a continuous population. We give explicit series expansions for large neighbourhood size and for low mutation rates respectively and investigate the accuracy of the classical Malécot formula for these general models. When neighbourhood size is small, this formula does not give the identity even over large scales. However, for large neighbourhood size, it is an accurate approximation which summarises the local population structure in terms of three quantities: the effective dispersal rate, σe; the effective population density, ρe; and a local scale, κ, at which local interactions become significant. The results are illustrated by simulations.
AU - Nicholas Barton
AU - Depaulis, Frantz
AU - Etheridge, Alison M
ID - 4263
IS - 1
JF - Theoretical Population Biology
TI - Neutral evolution in spatially continuous populations
VL - 61
ER -
TY - JOUR
AB - Phylogenetic trees can be rooted by a number of criteria. Here, we introduce a Bayesian method for inferring the root of a phylogenetic tree by using one of several criteria: the outgroup, molecular clock, and nonreversible model of DNA substitution. We perform simulation analyses to examine the relative ability of these three criteria to correctly identify the root of the tree. The outgroup and molecular clock criteria were best able to identify the root of the tree, whereas the nonreversible model was able to identify the root only when the substitution process was highly nonreversible. We also examined the performance of the criteria for a tree of four species for which the topology and root position are well supported. Results of the analyses of these data are consistent with the simulation results.
AU - Huelsenbeck, John P
AU - Jonathan Bollback
AU - Levine, Amy M
ID - 4347
IS - 1
JF - Systematic Biology
TI - Inferring the root of a phylogenetic tree
VL - 51
ER -
TY - JOUR
AB - Bayesian inference is becoming a common statistical approach to phylogenetic estimation because, among other reasons, it allows for rapid analysis of large data sets with complex evolutionary models. Conveniently, Bayesian phylogenetic methods use currently available stochastic models of sequence evolution. However, as with other model-based approaches, the results of Bayesian inference are conditional on the assumed model of evolution: inadequate models (models that poorly fit the data) may result in erroneous inferences. In this article, I present a Bayesian phylogenetic method that evaluates the adequacy of evolutionary models using posterior predictive distributions. By evaluating a model's posterior predictive performance, an adequate model can be selected for a Bayesian phylogenetic study. Although I present a single test statistic that assesses the overall (global) performance of a phylogenetic model, a variety of test statistics can be tailored to evaluate specific features (local performance) of evolutionary models to identify sources failure. The method presented here, unlike the likelihood-ratio test and parametric bootstrap, accounts for uncertainty in the phylogeny and model parameters.
AU - Jonathan Bollback
ID - 4349
IS - 7
JF - Molecular Biology and Evolution
TI - Bayesian model adequacy and choice in phylogenetics
VL - 19
ER -
TY - JOUR
AB - This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating MetricIntervalTL formulae into EventClockTL formulae, the two logics being equally expressive. Our proof is structured to yield axiomatizations also for interesting fragments of these logics, such as the linear temporal logic of the real numbers (TLR).
AU - Raskin, Jean-François
AU - Schobbens, Pierre Y
AU - Thomas Henzinger
ID - 4407
IS - 1-2
JF - Theoretical Computer Science
TI - Axioms for real-time logics
VL - 274
ER -
TY - CONF
AB - An essential problem in component-based design is how to compose components designed in isolation. Several approaches have been proposed for specifying component interfaces that capture behavioral aspects such as interaction protocols, and for verifying interface compatibility. Likewise, several approaches have been developed for synthesizing converters between incompatible protocols. In this paper, we introduce the notion of adaptability as the property that two interfaces have when they can be made compatible by communicating through a converter that meets specified requirements. We show that verifying adaptability and synthesizing an appropriate converter are two faces of the same coin: adaptability can be formalized and solved using a game-theoretic framework, and then the converter can be synthesized as a strategy that always wins the game. Finally we show that this framework can be related to the rectification problem in trace theory.
AU - Passerone, Roberto
AU - de Alfaro, Luca
AU - Thomas Henzinger
AU - Sangiovanni-Vincentelli, Alberto
ID - 4413
TI - Convertibility verification and converter synthesis: Two faces of the same coin
ER -
TY - THES
AB - This dissertation investigates game-theoretic approaches to the algorithmic analysis of concurrent, reactive systems. A concurrent system comprises a number of components working concurrently; a reactive system maintains an ongoing interaction with its environment. Traditional approaches to the formal analysis of concurrent reactive systems usually view the system as an unstructured state-transition graphs; instead, we view them as collections of interacting components, where each one is an open system which accepts inputs from the other components. The interactions among the components are naturally modeled as games.
Adopting this game-theoretic view, we study three related problems pertaining to the verification and synthesis of systems. Firstly, we propose two novel game-theoretic techniques for the model-checking of concurrent reactive systems, and improve the performance of model-checking. The first technique discovers an error as soon as it cannot be prevented, which can be long before it actually occurs. This technique is based on the key observation that "unpreventability" is a local property to a module: an error is unpreventable in a module state if no environment can prevent it. The second technique attempts to decompose a model-checking proof into smaller proof obligations by constructing abstract modules automatically, using reachability and "unpreventability" information about the concrete modules. Three increasingly powerful proof decomposition rules are proposed and we show that in practice, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification. Both techniques fall into the category of compositional reasoning.
Secondly, we investigate the composition and control of synchronous systems. An essential property of synchronous systems for compositional reasoning is non-blocking. In the composition of synchronous systems, however, due to circular causal dependency of input and output signals, non-blocking is not always guaranteed. Blocking compositions of systems can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping systems with types, which make the dependencies between input and output signals transparent. We characterize various typing mechanisms in game-theoretic terms, and study their effects on the controller synthesis problem. We show that our typing systems are general enough to capture interesting real-life synchronous systems such as all delay-insensitive digital circuits. We then study their corresponding single-step control problems --a restricted form of controller synthesis problem whose solutions can be iterated in appropriate manners to solve all LTL controller synthesis problems. We also consider versions of the controller synthesis problem in which the type of the controller is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions.
Thirdly, we study the synthesis of a class of open systems, namely, uninitialized state machines. The sequential synthesis problem, which is closely related to Church's solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. We solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Buechi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. The lower bound proofs require nontrivial generic reductions.
AU - Mang, Freddy
ID - 4414
TI - Games in open systems verification and synthesis
ER -
TY - CONF
AB - We demonstrate the feasibility and benefits of Giotto-based control software development by reimplementing the autopilot system of an autonomously flying model helicopter. Giotto offers a clean separation between the platform-independent concerns of software functionality and I/O timing, and the platform-dependent concerns of software scheduling and execution. Functionality code such as code computing control laws can be generated automatically from Simulink models or, as in the case of this project, inherited from a legacy system. I/O timing code is generated automatically from Giotto models that specify real-time requirements such as task frequencies and actuator update rates. We extend Simulink to support the design of Giotto models, and from these models, the automatic generation of Giotto code that supervises the interaction of the functionality code with the physical environment. The Giotto compiler performs a schedulability analysis on the Giotto code, and generates timing code for the helicopter platform. The Giotto methodology guarantees the stringent hard real-time requirements of the autopilot system, and at the same time supports the automation of the software development process in a way that produces a transparent software architecture with predictable behavior and reusable components.
AU - Kirsch, Christoph M
AU - Sanvido, Marco A
AU - Thomas Henzinger
AU - Pree, Wolfgang
ID - 4421
TI - A Giotto-based helicopter control system
VL - 2491
ER -
TY - CONF
AB - Behavioral properties of open systems can be formalized as objectives in two-player games. Turn-based games model asynchronous interaction between the players (the system and its environment) by interleaving their moves. Concurrent games model synchronous interaction: the players always move simultaneously. Infinitary winning criteria are considered: Büchi, co-Büchi, and more general parity conditions. A generalization of determinacy for parity games to concurrent parity games demands probabilistic (mixed) strategies: either player 1 has a mixed strategy to win with probability 1 (almost-sure winning), or player 2 has a mixed strategy to win with positive probability.
This work provides efficient reductions of concurrent probabilistic Büchi and co-Büchi games to turn-based games with Büchi condition and parity winning condition with three priorities, respectively. From a theoretical point of view, the latter reduction shows that one can trade the probabilistic nature of almost-sure winning for a more general parity (fairness) condition. The reductions improve understanding of concurrent games and provide an alternative simple proof of determinacy of concurrent Büchi and co-Büchi games. From a practical point of view, the reductions turn solvers of turn-based games into solvers of concurrent probabilistic games. Thus improvements in the well-studied algorithms for the former carry over immediately to the latter. In particular, a recent improvement in the complexity of solving turn-based parity games yields an improvement in time complexity of solving concurrent probabilistic co-Büchi games from cubic to quadratic.
AU - Jurdziński, Marcin
AU - Kupferman, Orna
AU - Thomas Henzinger
ID - 4422
TI - Trading probability for fairness
VL - 2471
ER -
TY - CONF
AB - Automation control systems typically incorporate legacy code and components that were originally designed to operate independently. Furthermore, they operate under stringent safety and timing constraints. Current design strategies deal with these requirements and characteristics with ad hoc approaches. In particular, when designing control laws, implementation constraints are often ignored or cursorily estimated. Indeed, costly redesigns are needed after a prototype of the control system is built due to missed timing constraints and subtle transient errors. In this paper, we use the concepts of platform-based design, and the Giotto programming language, to develop a methodology for the design of automation control systems that builds in modularity and correct-by-construction procedures. We illustrate our strategy by describing the (successful) application of the methodology to the design of a time-based control system for a rotorcraft Uninhabited Aerial Vehicle (UAV).
AU - Horowitz, Benjamin
AU - Liebman, Judith
AU - Ma, Cedric
AU - Koo, T John
AU - Thomas Henzinger
AU - Sangiovanni-Vincentelli, Alberto
AU - Sastry, Shankar
ID - 4423
IS - 1
TI - Embedded software design and system integration for rotorcraft UAV using platforms
VL - 15
ER -
TY - CONF
AB - The Embedded Machine is a virtual machine that mediates in real time the interaction between software processes and physical processes. It separates the compilation of embedded programs into two phases. The first, platform-independent compiler phase generates E code (code executed by the Embedded Machine), which supervises the timing ---not the scheduling--- of application tasks relative to external events, such as clock ticks and sensor interrupts. E~code is portable and exhibits, given an input behavior, predictable (i.e., deterministic) timing and output behavior. The second, platform-dependent compiler phase checks the time safety of the E code, that is, whether platform performance (determined by the hardware) and platform utilization (determined by the scheduler of the operating system) enable its timely execution. We have used the Embedded Machine to compile and execute high-performance control applications written in Giotto, such as the flight control system of an autonomous model helicopter.
AU - Thomas Henzinger
AU - Kirsch, Christoph M
ID - 4444
TI - The embedded machine: predictable, portable real-time code
ER -
TY - CONF
AB - Giotto is a platform-independent language for specifying software for high-performance control applications. In this paper we present a new approach to the compilation of Giotto. Following this approach, the Giotto compiler generates code for a virtual machine, called the E machine, which can be ported to different platforms. The Giotto compiler also checks if the generated E code is time safe for a given platform, that is, if the platform offers sufficient performance to ensure that the E code is executed in a timely fashion that conforms with the Giotto semantics. Time-safety checking requires a schedulability analysis. We show that while for arbitrary E code, the analysis is exponential, for E code generated from typical Giotto programs, the analysis is polynomial. This supports our claim that Giotto identifies a useful fragment of embedded programs.
AU - Thomas Henzinger
AU - Kirsch, Christoph M
AU - Majumdar, Ritankar S
AU - Matic, Slobodan
ID - 4470
TI - Time-safety checking for embedded programs
VL - 2491
ER -
TY - CONF
AB - The sequential synthesis problem, which is closely related to Church’s solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. In this paper we solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Büchi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. We also study the problem of deciding whether a given specification is uninitialized, that is, if its uninitialized and initialized synthesis problems coincide. We show that this problem has, for each specification formalism, the same complexity as the equivalence problem.
AU - Thomas Henzinger
AU - Krishnan, Sriram C
AU - Kupferman, Orna
AU - Mang, Freddy Y
ID - 4471
TI - Synthesis of uninitialized systems
VL - 2380
ER -