@inproceedings{4552, abstract = {A concurrent reachability game is a two-player game played on a graph: at each state, the players simultaneously and independently select moves; the two moves determine jointly a probability distribution over the successor states. The objective for player 1 consists in reaching a set of target states; the objective for player 2 is to prevent this, so that the game is zero-sum. Our contributions are two-fold. First, we present a simple proof of the fact that in concurrent reachability games, for all epsilon > 0, memoryless epsilon-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an epsilon-optimal strategy achieves the objective with probability within epsilon of the value of the game. In contrast to previous proofs of this fact, which rely on the limit behavior of discounted games using advanced Puisieux series analysis, our proof is elementary and combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives.}, author = {Chatterjee, Krishnendu and De Alfaro, Luca and Henzinger, Thomas A}, booktitle = {Proceedings of the 3rd international conference on the Quantitative Evaluation of Systems}, isbn = {0769526659}, location = {Riverside, CA, United States}, pages = {291 -- 300}, publisher = {IEEE}, title = {{Strategy improvement for concurrent reachability games}}, doi = {10.1109/QEST.2006.48}, year = {2006}, } @inproceedings{4528, abstract = {Computational modeling of biological systems is becoming increasingly common as scientists attempt to understand biological phenomena in their full complexity. Here we distinguish between two types of biological models mathematical and computational - according to their different representations of biological phenomena and their diverse potential. We call the approach of constructing computational models of biological systems executable biology, as it focuses on the design of executable computer algorithms that mimic biological phenomena. We give an overview of the main modeling efforts in this direction, and discuss some of the new challenges that executable biology poses for computer science and biology. We argue that for executable biology to reach its full potential as a mainstream biological technique, formal and algorithmic approaches must be integrated into biological research, driving biology towards a more precise engineering discipline.}, author = {Fisher, Jasmin and Henzinger, Thomas A}, booktitle = {Proceedings of the 38th conference on Winter simulation}, isbn = {1424405009}, issn = {1558-4305}, location = {Monterey, CA, United States}, pages = {1675 -- 1682}, publisher = {IEEE}, title = {{Executable biology}}, doi = {10.1109/WSC.2006.322942}, year = {2006}, } @article{4550, abstract = {In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent's payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it sometimes suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is secure if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of ω-regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jurdziński, Marcin}, issn = {1879-2294}, journal = {Theoretical Computer Science}, number = {1-2}, pages = {67 -- 82}, publisher = {Elsevier}, title = {{Games with secure equilibria}}, doi = {10.1016/j.tcs.2006.07.032}, volume = {365}, year = {2006}, } @inproceedings{4437, abstract = {The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton that is good for solving games with objective . The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.}, author = {Henzinger, Thomas A and Piterman, Nir}, booktitle = {Proceedings of the 20th international conference on Computer Science Logic}, isbn = {9783540454588}, issn = {1611-3349}, location = {Szeged, Hungary}, pages = {395 -- 410}, publisher = {Springer}, title = {{Solving games without determinization}}, doi = {10.1007/11874683_26}, volume = {4207}, year = {2006}, } @inproceedings{4436, abstract = {We present an assume-guarantee interface algebra for real-time components. In our formalism a component implements a set of task sequences that share a resource. A component interface consists of an arrival rate function and a latency for each task sequence, and a capacity function for the shared resource. The interface specifies that the component guarantees certain task latencies depending on assumptions about task arrival rates and allocated resource capacities. Our algebra defines compatibility and refinement relations on interfaces. Interface compatibility can be checked on partial designs, even when some component interfaces are yet unknown. In this case interface composition computes as new assumptions the weakest constraints on the unknown components that are necessary to satisfy the specified guarantees. Interface refinement is defined in a way that ensures that compatible interfaces can be refined and implemented independently. Our algebra thus formalizes an interface-based design methodology that supports both the incremental addition of new components and the independent stepwise refinement of existing components. We demonstrate the flexibility and efficiency of the framework through simulation experiments.}, author = {Henzinger, Thomas A and Matic, Slobodan}, booktitle = {Proceedings of the 12th IEEE Real-Time and Embedded Technology and Applications Symposium}, isbn = {0769525164}, issn = {1545-3421}, location = {San Jose, CA, United States}, pages = {253 -- 266}, publisher = {IEEE}, title = {{An interface algebra for real-time components}}, doi = {10.1109/RTAS.2006.11}, year = {2006}, } @inproceedings{4523, abstract = {We consider the problem if a given program satisfies a specified safety property. Interesting programs have infinite state spaces, with inputs ranging over infinite domains, and for these programs the property checking problem is undecidable. Two broad approaches to property checking are testing and verification. Testing tries to find inputs and executions which demonstrate violations of the property. Verification tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to find, but it is often difficult to achieve sufficient coverage for correct programs. On the other hand, verification methods are most successful when proofs are easy to find, but they are often inefficient at discovering errors. We propose a new algorithm, Synergy, which combines testing and verification. Synergy unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi.}, author = {Gulavani, Bhargav and Henzinger, Thomas A and Kannan, Yamini and Nori, Aditya and Rajamani, Sriram}, booktitle = {Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering}, isbn = {9781595934680}, location = {Portland, Oregon, United States}, pages = {117 -- 127}, publisher = {ACM}, title = {{Synergy: A new algorithm for property checking}}, doi = {10.1145/1181775.1181790}, year = {2006}, } @inproceedings{4526, abstract = {We designed and implemented a new programming language called Hierarchical Timing Language (HTL) for hard realtime systems. Critical timing constraints are specified within the language,and ensured by the compiler. Programs in HTL are extensible in two dimensions without changing their timing behavior: new program modules can be added, and individual program tasks can be refined. The mechanism supporting time invariance under parallel composition is that different program modules communicate at specified instances of time. Time invariance under refinement is achieved by conservative scheduling of the top level. HTL is a coordination language, in that individual tasks can be implemented in "foreign" languages. As a case study, we present a distributed HTL implementation of an automotive steer-by-wire controller.}, author = {Ghosal, Arkadeb and Henzinger, Thomas A and Iercan, Daniel and Kirsch, Christoph and Sangiovanni Vincentelli, Alberto}, booktitle = {Proceedings of the 6th ACM & IEEE International conference on Embedded software}, isbn = {9781595935427}, location = {Seoul, Korea}, pages = {132 -- 141}, publisher = {ACM}, title = {{A hierarchical coordination language for interacting real-time tasks}}, doi = {10.1145/1176887.1176907}, year = {2006}, } @article{4451, abstract = {One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternation-free fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment.}, author = {Henzinger, Thomas A and Kupferman, Orna and Majumdar, Ritankar}, issn = {1879-2294}, journal = {Theoretical Computer Science}, number = {2}, pages = {173 -- 186}, publisher = {Elsevier}, title = {{On the universal and existential fragments of the mu-calculus}}, doi = {10.1016/j.tcs.2005.11.015}, volume = {354}, year = {2006}, } @article{4352, abstract = {Anopheles darlingi is the primary malaria vector in Latin America, and is especially important in Amazonian Brazil. Historically, control efforts have been focused on indoor house spraying using a variety of insecticides, but since the mid-1990s there has been a shift to patient treatment and focal insecticide fogging. Anopheles darlingi was believed to have been significantly reduced in a gold-mining community, Peixoto de Azevedo (in Mato Grosso State), in the early 1990s by insecticide use during a severe malaria epidemic. In contrast, although An. darlingi was eradicated from some districts of the city of Belem (the capital of Para State) in 1968 to reduce malaria, populations around the water protection area in the eastern district were treated only briefly. To investigate the population structure of An. darlingi including evidence for a population bottleneck in Peixoto, we analyzed eight microsatellite loci of 256 individuals from seven locations in Brazil: three in Amapa State, three in Para State, and one in Mato Grosso State. Allelic diversity and mean expected heterozygosity were high for all populations (mean number alleles/locus and H(E) were 13.5 and 0.834, respectively) and did not differ significantly between locations. Significant heterozygote deficits were associated with linkage disequilibrium, most likely due to either the Wahlund effect or selection. We found no evidence for a population bottleneck in Peixoto, possibly because the reduction was not extreme enough to be detected. Overall estimates of long-term N(e) varied from 92.4 individuals under the linkage disequilibrium model to infinity under the heterozygote excess model. Fixation indices and analysis of molecular variance demonstrated significant differentiation between locations north and south of the Amazon River, suggesting a degree of genetic isolation between them, attributed to isolation by distance.}, author = {Conn, Jan and Vineis, Joseph and Bollback, Jonathan P and Onyabe, David and Wilkerson, Richard and Povoa, Marinete}, issn = {1476-1645}, journal = {The American Journal of Tropical Medicine and Hygiene}, number = {5}, pages = {798 -- 806}, publisher = {American Society of Tropical Medicine and Hygiene}, title = {{Population structure of the malaria vector Anopheles darlingi in a malaria-endemic region of eastern Amazonian Brazil}}, volume = {74}, year = {2006}, } @inproceedings{4406, abstract = {We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata.}, author = {De Wulf, Martin and Doyen, Laurent and Henzinger, Thomas A and Raskin, Jean}, booktitle = {Proceedings of the 18th international conference on Computer Aided Verification}, isbn = {9783540374060}, issn = {1611-3349}, location = {Seattle, WA, United States}, pages = {17 -- 30}, publisher = {Springer Nature}, title = {{Antichains: A new algorithm for checking universality of finite automata}}, doi = {10.1007/11817963_5}, volume = {4144}, year = {2006}, } @inproceedings{4432, abstract = {We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision.}, author = {Henzinger, Thomas A and Prabhu, Vinayak}, booktitle = {Proceedings of the 4th international conference on Formal Modeling and Analysis of Timed Systems}, isbn = {9783540450269}, issn = {1611-3349}, location = {Paris, France}, pages = {1 -- 17}, publisher = {Springer Nature}, title = {{Timed alternating-time temporal logic}}, doi = {10.1007/11867340_1}, volume = {4202}, year = {2006}, } @inproceedings{4431, abstract = {We summarize some current trends in embedded systems design and point out some of their characteristics, such as the chasm between analytical and computational models, and the gap between safety-critical and best-effort engineering practices. We call for a coherent scientific foundation for embedded systems design, and we discuss a few key demands on such a foundation: the need for encompassing several manifestations of heterogeneity, and the need for constructivity in design. We believe that the development of a satisfactory Embedded Systems Design Science provides a timely challenge and opportunity for reinvigorating computer science.}, author = {Henzinger, Thomas A and Sifakis, Joseph}, booktitle = {Proceedings of the 14th international conference on Formal Methods}, isbn = {9783540372158}, issn = {1611-3349}, location = {Hamilton, Canada}, pages = {1 -- 15}, publisher = {Springer Nature}, title = {{The embedded systems design challenge}}, doi = {10.1007/11813040_1}, volume = {4085}, year = {2006}, } @article{4351, abstract = {BACKGROUND: Character mapping on phylogenies has played an important, if not critical role, in our understanding of molecular, morphological, and behavioral evolution. Until very recently we have relied on parsimony to infer character changes. Parsimony has a number of serious limitations that are drawbacks to our understanding. Recent statistical methods have been developed that free us from these limitations enabling us to overcome the problems of parsimony by accommodating uncertainty in evolutionary time, ancestral states, and the phylogeny. RESULTS: SIMMAP has been developed to implement stochastic character mapping that is useful to both molecular evolutionists, systematists, and bioinformaticians. Researchers can address questions about positive selection, patterns of amino acid substitution, character association, and patterns of morphological evolution. CONCLUSION: Stochastic character mapping, as implemented in the SIMMAP software, enables users to address questions that require mapping characters onto phylogenies using a probabilistic approach that does not rely on parsimony. Analyses can be performed using a fully Bayesian approach that is not reliant on considering a single topology, set of substitution model parameters, or reconstruction of ancestral states. Uncertainty in these quantities is accommodated by using MCMC samples from their respective posterior distributions.}, author = {Bollback, Jonathan P}, issn = {1471-2105}, journal = {BMC Bioinformatics}, publisher = {BioMed Central}, title = {{SIMMAP: stochastic character mapping of discrete traits on phylogenies}}, doi = {10.1186/1471-2105-7-88}, volume = {7}, year = {2006}, } @article{4248, abstract = {In finite populations, genetic drift generates interference between selected loci, causing advantageous alleles to be found more often on different chromosomes than on the same chromosome, which reduces the rate of adaptation. This “Hill–Robertson effect” generates indirect selection to increase recombination rates. We present a new method to quantify the strength of this selection. Our model represents a new beneficial allele (A) entering a population as a single copy, while another beneficial allele (B) is sweeping at another locus. A third locus affects the recombination rate between selected loci. Using a branching process model, we calculate the probability distribution of the number of copies of A on the different genetic backgrounds, after it is established but while it is still rare. Then, we use a deterministic model to express the change in frequency of the recombination modifier, due to hitchhiking, as A goes to fixation. We show that this method can give good estimates of selection for recombination. Moreover, it shows that recombination is selected through two different effects: it increases the fixation probability of new alleles, and it accelerates selective sweeps. The relative importance of these two effects depends on the relative times of occurrence of the beneficial alleles.}, author = {Roze, Denis and Barton, Nicholas H}, issn = {1943-2631}, journal = {Genetics}, number = {3}, pages = {1793 -- 1811}, publisher = {Genetics Society of America}, title = {{The Hill-Robertson effect and the evolution of recombination}}, doi = {10.1534/genetics.106.058586 }, volume = {173}, year = {2006}, } @misc{4250, author = {Barton, Nicholas H}, booktitle = {Current Biology}, issn = {1879-0445}, number = {16}, pages = {647 -- 650}, publisher = {Cell Press}, title = {{Evolutionary Biology: How did the human species form?}}, doi = {10.1016/j.cub.2006.07.032}, volume = {16}, year = {2006}, } @article{4218, abstract = {The molecular and cellular mechanisms governing cell motility and directed migration in response to the chemokine SDF-1 are largely unknown. Here, we demonstrate that zebrafish primordial germ cells whose migration is guided by SDF-1 generate bleb-like protrusions that are powered by cytoplasmic flow. Protrusions are formed at sites of higher levels of free calcium where activation of myosin contraction occurs. Separation of the acto-myosin cortex from the plasma membrane at these sites is followed by a flow of cytoplasm into the forming bleb. We propose that polarized activation of the receptor CXCR4 leads to a rise in free calcium that in turn activates myosin contraction in the part of the cell responding to higher levels of the ligand SDF-1. The biased formation of new protrusions in a particular region of the cell in response to SDF-1 defines the leading edge and the direction of cell migration.}, author = {Blaser, Heiko and Reichman Fried, Michal and Castanon, Irinka and Dumstrei, Karin and Marlow, Florence and Kawakami, Koichi and Solnica Krezel, Lilianna and Heisenberg, Carl-Philipp J and Raz, Erez}, issn = {1878-1551}, journal = {Developmental Cell}, number = {5}, pages = {613 -- 627}, publisher = {Cell Press}, title = {{Migration of zebrafish primordial germ cells: A role for myosin contraction and cytoplasmic flow}}, doi = {10.1016/j.devcel.2006.09.023}, volume = {11}, year = {2006}, } @article{4184, abstract = {Epithelial morphogenesis depends on coordinated changes in cell shape, a process that is still poorly understood. During zebrafish epiboly and Drosophila dorsal closure, cell-shape changes at the epithelial margin are of critical importance. Here evidence is provided for a conserved mechanism of local actin and myosin 2 recruitment during theses events. It was found that during epiboly of the zebrafish embryo, the movement of the outer epithelium (enveloping layer) over the yolk cell surface involves the constriction of marginal cells. This process depends on the recruitment of actin and myosin 2 within the yolk cytoplasm along the margin of the enveloping layer. Actin and myosin 2 recruitment within the yolk cytoplasm requires the Ste20-like kinase Msn1, an orthologue of Drosophila Misshapen. Similarly, in Drosophila, actin and myosin 2 localization and cell constriction at the margin of the epidermis mediate dorsal closure and are controlled by Misshapen. Thus, this study has characterized a conserved mechanism underlying coordinated cell-shape changes during epithelial morphogenesis.}, author = {Köppen, Mathias and Fernández, Beatriz and Carvalho, Lara and Jacinto, António and Heisenberg, Carl-Philipp J}, issn = {1477-9129}, journal = {Development}, number = {14}, pages = {2671 -- 2681}, publisher = {Company of Biologists}, title = {{Coordinated cell-shape changes control epithelial movement in zebrafish and Drosophila}}, doi = {doi: 10.1242/dev.02439}, volume = {133}, year = {2006}, } @article{4176, abstract = {During vertebrate gastrulation, a well-orchestrated series of morphogenetic changes leads to the formation of the three germ layers: the ectoderm, mesoderm and endoderm. The analysis of gene expression patterns during gastrulation has been central to the identification of genes involved in germ layer formation. However, many proteins are regulated on a translational or post-translational level and are thus undetectable by gene expression analysis. Therefore, we developed a 2D-gel-based comparative proteomic approach to target proteins involved in germ layer morphogenesis during zebrafish gastrulation. Proteomes of ectodermal and mesendodermal progenitor cells were compared and 35 significantly regulated proteins were identified by mass spectrometry, including several proteins with predicted functions in cytoskeletal organization. A comparison of our proteomic results with data obtained in an accompanying microarray-based gene expression analysis revealed no significant overlap, confirming the complementary nature of proteomics and transcriptomics. The regulation of ezrin2, which was identified based on a reduction in spot intensity in mesendodermal cells, was independently validated. Furthermore, we show that ezrin2 is activated by phosphorylation in mesendodermal cells and is required for proper germ layer morphogenesis. We demonstrate the feasibility of proteomics in zebrafish, concluding that proteomics is a valuable tool for analysis of early development.}, author = {Link, Vinzenz and Carvalho, Lara and Castanon, Irinka and Stockinger, Petra and Shevchenko, Andrej and Heisenberg, Carl-Philipp J}, issn = {1477-9137}, journal = {Journal of Cell Science}, number = {10}, pages = {2073 -- 2083}, publisher = {Company of Biologists}, title = {{Identification of regulators of germ layer morphogenesis using proteomics in zebrafish}}, doi = {10.1242/jcs.02928}, volume = {119}, year = {2006}, } @article{4178, abstract = {Detailed reconstruction of the spatiotemporal history of embryonic cells is key to understanding tissue formation processes but is often complicated by the large number of cells involved, particularly so in vertebrates. Through a combination of high-resolution time-lapse lineage tracing and antibody staining, we have analyzed the movement of mesencephalic and metencephalic cell populations in the early zebrafish embryo. To facilitate the analysis of our cell tracking data, we have created TracePilot, a software tool that allows interactive manipulation and visualization of tracking data. We demonstrate its utility by showing novel visualizations of cell movement in the developing zebrafish brain. TracePilot (http://www.mpi-cbg.de/tracepilot) is Java-based, available free of charge, and has a program structure that allows the incorporation of additional analysis tools.}, author = {Langenberg, Tobias and Dracz, Tadeusz and Oates, Andrew and Heisenberg, Carl-Philipp J and Brand, Michael}, issn = {1097-0177}, journal = {Developmental Dynamics}, number = {4}, pages = {928 -- 933}, publisher = {Wiley-Blackwell}, title = {{Analysis and visualization of cell movement in the developing zebrafish brain}}, doi = {10.1002/dvdy.20692}, volume = {235}, year = {2006}, } @article{4140, abstract = {Wnt11 is a key signal, determining cell polarization and migration during vertebrate gastrulation. It is known that Wnt11 functionally interacts with several signaling components, the homologues of which control planar cell polarity in Drosophila melanogaster. Although in D. melanogaster these components are thought to polarize cells by asymmetrically localizing at the plasma membrane, it is not yet clear whether their subcellular localization plays a similarly important role in vertebrates. We show that in zebrafish embryonic cells, Wnt11 locally functions at the plasma membrane by accumulating its receptor, Frizzled 7, on adjacent sites of cell contacts. Wnt11-induced Frizzled 7 accumulations recruit the intracellular Wnt signaling mediator Dishevelled, as well as Wnt11 itself, and locally increase cell contact persistence. This increase in cell contact persistence is mediated by the local interaction of Wnt11, Frizzled 7, and the atypical cadherin Flamingo at the plasma membrane, and it does not require the activity of further downstream effectors of Wnt11 signaling, such as RhoA and Rok2. We propose that Wnt11, by interacting with Frizzled 7 and Flamingo, modulates local cell contact persistence to coordinate cell movements during gastrulation.}, author = {Witzel, Sabine and Zimyanin, Vitaly and Carreira Barbosa, Filipa and Tada, Masazumi and Heisenberg, Carl-Philipp J}, issn = {1540-8140}, journal = {Journal of Cell Biology}, number = {5}, pages = {791 -- 802}, publisher = {Rockefeller University Press}, title = {{Wnt11 controls cell contact persistence by local accumulation of Frizzled 7 at the plasma membrane}}, doi = {10.1083/jcb.200606017}, volume = {175}, year = {2006}, }