@article{4220, abstract = {In the zebrafish, Danio rerio, a caudal and pectoral fin fold develop during embryogenesis. At larval stages the caudal fin fold is replaced by four different fins, the unpaired anal, dorsal and tail fins. In addition the paired pelvic fins are formed, We have identified a total of 118 mutations affecting larval fin formation, Mutations in 11 genes lead to abnormal morphology or degeneration of both caudal and pectoral fin folds, Most mutants survive to adulthood and form a surprisingly normal complement of adult fins, Mutations in nine genes result in an increased or reduced size of the pectoral fins, Interestingly, in mutants of one of these genes, dackel (dak), pectoral fin buds form initially, but later the fin epithelium fails to expand, Expression of sonic hedgehog mRNA in the posterior mesenchyme of the pectoral fin bud is initiated in dak embryos, but not maintained, Mutations in five other genes affect adult fin but not larval fin development, Two mutants, longfin (lof) and another longfin (alf) have generally longer fins. Stein und bein (sub) has reduced dorsal and pelvic fins, whereas finless (fls) and wanda (wan) mutants affect all adult fins, Finally, mutations in four genes causing defects in embryonic skin formation will be briefly reported.}, author = {Van Eeden, Fredericus and Granato, Michael and Schach, Ursula and Brand, Michael and Furutani Seiki, Makoto and Haffter, Pascal and Hammerschmidt, Matthias and Heisenberg, Carl-Philipp J and Jiang, Yunjin and Kane, Donald and Kelsh, Robert and Mullins, Mary and Odenthal, Jörg and Warga, Rachel and Nüsslein Volhard, Christiane}, issn = {0950-1991}, journal = {Development}, number = {1}, pages = {255 -- 262}, publisher = {Company of Biologists}, title = {{Genetic analysis of fin formation in the zebrafish, Danio rerio}}, doi = {10.1242/dev.123.1.255 }, volume = {123}, year = {1996}, } @article{4222, abstract = {Somitogenesis is the basis of segmentation of the mesoderm in the trunk and tail of vertebrate embryos, Two groups of mutants with defects in this patterning process have been isolated in our screen for zygotic mutations affecting the embryonic development of the zebrafish (Danio rerio), In mutants of the first group, boundaries between individual somites are invisible early on, although the paraxial mesoderm is present, Later, irregular boundaries between somites are present, Mutations infused somites (fss) and beamter (bea) affect all somites, whereas mutations in deadly seven (des), after eight (aei) and white tail (wit) only affect the more posterior somites, Mutants of all genes but wit are homozygous viable and fertile, Skeletal stainings and the expression pattern of myoD and snail1 suggest that anteroposterior patterning within individual somites is abnormal, In the second group of mutants, formation of the horizontal myoseptum, which separates the dorsal and ventral part of the myotome, is reduced, Six genes have been defined in this group (you-type genes), yea-too mutants show the most severe phenotype; in these the adaxial cells, muscle pioneers and the primary motoneurons are affected, in addition to the horizontal myoseptum. The horizontal myoseptum is also missing in mutants that lack a notochord. The similarity of the somite phenotype in mutants lacking the notochord and in the you-type mutants suggests that the genes mutated in these two groups are involved in a signaling pathway from the notochord, important for patterning of the somites.}, author = {Van Eeden, Fredericus and Granato, Michael and Schach, Ursula and Brand, Michael and Furutani Seiki, Makoto and Haffter, Pascal and Hammerschmidt, Matthias and Heisenberg, Carl-Philipp J and Jiang, Yunjin and Kane, Donald and Kelsh, Robert and Mullins, Mary and Odenthal, Jörg and Warga, Rachel and Allende, Miguel and Weinberg, Eric and Nüsslein Volhard, Christiane}, issn = {0950-1991}, journal = {Development}, number = {1}, pages = {153 -- 164}, publisher = {Company of Biologists}, title = {{Mutations affecting somite formation and patterning in the zebrafish, Danio rerio}}, doi = {10.1242/dev.123.1.153}, volume = {123}, year = {1996}, } @article{4292, abstract = {Ageing, or senescence, is a decline in state at later ages that is manifested through a reduction in survival and fecundity. Ageing means that reproductive prospects and hence the life history options (trade-offs) open to the organism decline. Evolutionary theories of ageing suggest that it evolves in response to the level of externally imposed mortality and insults to fertility, either as part of life history optimization or as a result of mutation pressure. Several recent empirical and theoretical studies have produced apparently anomalous results. Some have suggested that the rate of ageing can decline at later ages, others that demographic evidence for ageing can appear in parallel with an improvement in state. All of these studies used measures of ageing that would not be expected to give an accurate reflection of changes in the state of the organism with age. We propose that Fisher's `reproductive value' is a natural measure of state at each age, which includes prospects for both survival and reproduction. If this measure is used, the apparently anomalous findings are not at variance with evolutionary theories of ageing.}, author = {Partridge, Linda and Barton, Nicholas H}, issn = {0950-1193}, journal = {Proceedings of the Royal Society of London Series B Biological Sciences}, number = {1375}, pages = {1365 -- 1371}, publisher = {Royal Society of London}, title = {{On measuring the rate of ageing}}, doi = {10.1098/rspb.1996.0200}, volume = {263}, year = {1996}, } @inbook{4294, abstract = {Any sample of genes traces back to a single common ancestor. Each gene also has other properties: its sequence, its geographic location and the phenotype and fitness of the organism that carries it. With sexual reproduction, different genes have different genealogies, which gives us much more information, but also greatly complicates population genetic analysis. We review the close relation between the distribution of genealogies and the classic theory of identity by descent in spatially structured populations, and develop a simple diffusion approximation to the distribution of coalescence times in a homogeneous two-dimensional habitat. This shows that when neighbourhood size is large (as in most populations) only a small fraction of pairs of genes are closely related, and only this fraction gives information about current rates of gene flow. The increase of spatial dispersion with lineage age is thus a poor estimator of gene flow. The bulk of the genealogy depends on the long-term history of the population; we discuss ways of inferring this history from the concordance between genealogies across loci.}, author = {Barton, Nicholas H and Wilson, Ian}, booktitle = {New uses for new phylogenies}, isbn = {978-0198549840}, pages = {23 -- 56}, publisher = {Oxford University Press}, title = {{Genealogies and geography}}, doi = {10.1098/rstb.1995.0090}, year = {1996}, } @inbook{4295, abstract = {Genetic studies are beginning to provide insights into the evolutionary processes that reduce the fitness of hybrids between recently diverged species. However, the deleterious gene interactions responsible for this fitness reduction are still poorly understood.}, author = {Barton, Nicholas H}, booktitle = {Current Biology}, issn = {0960-9822}, pages = {1244 -- 1246}, publisher = {Cell Press}, title = {{Speciation: more than the sum of its parts}}, doi = {10.1016/S0960-9822(02)70707-0}, volume = {6}, year = {1996}, } @phdthesis{4419, abstract = {A {\em hybrid automaton\/} consists of a finite automaton interacting with a dynamical system. Hybrid automata are used to model embedded controllers and other systems that consist of interacting discrete and continuous components. A hybrid automaton is {\em rectangular\/} if each of its continuous variables~x satisfies a nondeterministic differential equation of the form a≤dxdt≤b, where a and~b are rational constants. Rectangular hybrid automata are particularly useful for the analysis of communication protocols in which local clocks have bounded drift, and for the conservative approximation of systems with more complex continuous behavior. We examine several verification problems on the class of rectangular hybrid automata, including reachability, temporal logic model checking, and controller synthesis. Both dense-time and discrete-time models are considered. We identify subclasses of rectangular hybrid automata for which these problems are decidable and give complexity analyses. An investigation of the structural properties of rectangular hybrid automata is undertaken. One method for proving the decidability of verification problems on infinite-state systems is to find finite quotient systems on which analysis can proceed. Three state-space equivalence relations with strong connections to temporal logic are bisimilarity, similarity, and language equivalence. We characterize the quotient spaces of rectangular hybrid automata with respect to these equivalence relations.}, author = {Kopke, Peter}, publisher = {Cornell University}, title = {{The Theory of Rectangular Hybrid Automata}}, year = {1996}, } @inproceedings{4426, abstract = {We use linear hybrid automata to define linear approximations of the phase portraits of nonlinear hybrid systems. The approximating automata can be analyzed automatically using the symbolic model checker HyTech. We demonstrate the technique through the study of predator-prey systems, where we compute population bounds for both species. We also identify a class of nonlinear hybrid automata for which linear phase-portrait approximations can be generated automatically.}, author = {Henzinger, Thomas A and Wong Toi, Howard}, booktitle = {Hybrid Systems III: Verification and Control}, editor = {Alur, Rajeev and Henzinger, Thomas A and Sontag, Eduardo}, isbn = {9783540611554}, pages = {377 -- 388}, publisher = {Springer}, title = {{Linear phase-portrait approximations for nonlinear hybrid systems}}, doi = {10.1007/BFb0020961}, volume = {1066}, year = {1996}, } @inbook{4427, abstract = {We model a steam-boiler control system using hybrid automata. We provide two abstracted linear models of the nonlinear behavior of the boiler. For each model, we define and verify a controller that maintains safe operation of the boiler. The less abstract model permits the design of a more efficient controller. We also demonstrate how the tool HyTech can be used to automatically synthesize control parameter constraints that guarantee safety of the boiler.}, author = {Henzinger, Thomas A and Wong Toi, Howard}, booktitle = {Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control}, isbn = {9783540495666}, pages = {265 -- 282}, publisher = {Springer}, title = {{Using HyTech to synthesize control parameters for a steam boiler}}, doi = {10.1007/BFb0027241}, volume = {1165}, year = {1996}, } @inproceedings{4443, abstract = {Three natural equivalence relations on the infinite state space of a hybrid automaton are language equivalence, simulation equivalence, and bisimulation equivalence. When one of these equivalence relations has a finite quotient, certain model checking and controller synthesis problems are decidable. When bounds on the number of equivalence classes are obtained, bounds on the running times of model checking and synthesis algorithms follow as corollaries. We characterize the time-abstract versions of these equivalence relations on the state spaces of rectangular hybrid automata (RHA), in which each continuous variable is a clock with bounded drift. These automata are useful for modeling communications protocols with drifting local clocks, and for the conservative approximation of more complex hybrid systems. Of our two main results, one has positive implications for automatic verification, and the other has negative implications. On the positive side, we find that the (finite) language equivalence quotient for RHA is coarser than was previously known by a multiplicative exponential factor. On the negative side, we show that simulation equivalence for RHA is equality (which obviously has an infinite quotient). Our main positive result is established by analyzing a subclass of timed automata, called one-sided timed automata (OTA), for which the language equivalence quotient is coarser than for the class of all timed automata. An exact characterization of language equivalence for OTA requires a distinction between synchronous and asynchronous definitions of (bi)simulation: if time actions are silent, then the induced quotient for OTA is coarser than if time actions (but not their durations) are visible.}, author = {Henzinger, Thomas A and Kopke, Peter}, booktitle = {7th International Conference on Concurrency Theory}, isbn = {9783540616047}, location = {Pisa, Italy}, pages = {530 -- 545}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{State equivalences for rectangular hybrid automata}}, doi = {10.1007/3-540-61604-7_74}, volume = {1119}, year = {1996}, } @inproceedings{4495, abstract = {In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The main practical limitation of model checking is caused by the size of the state space of the program, which grows exponentially with the number of concurrent components. This problem, known as the state-explosion problem, becomes more difficult when we consider real-time model checking, where the program and the specification involve quantitative references to time. In particular, when use timed automata to describe real-time programs and we specify timed behaviors in the logic TCTL, a real-time extension of the temporal logic CTL with clock variables, then the state space under consideration grows exponentially not only with the number of concurrent components, but also with the number of clocks and the length of the clock constraints used in the program and the specification. Two powerful methods for coping with the state-explosion problem are on-the-fly and space-efficient model checking. In on-the-fly model checking, we explore only the portion of the state space of the program whose exploration is essential for determining the satisfaction of the specification. In space-efficient model checking, we store in memory the minimal information required, preferring to spend time on reconstructing information rather than spend space on storing it. In this work we develop an automata-theoretic approach to TCTL model checking that combines both methods. We suggest, for the first time, a PSPACE on-the-fly model-checking algorithm for TCTL.}, author = {Henzinger, Thomas A and Kupferman, Orna and Vardi, Moshe}, booktitle = {7th International Conference on Concurrency Theory}, isbn = {978-3-540-70625-0}, location = {Pisa, Italy}, pages = {514 -- 529}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{A space-efficient on-the-fly algorithm for real-time model checking}}, doi = {10.1007/3-540-61604-7_73}, volume = {1119}, year = {1996}, } @inproceedings{4519, abstract = {We summarize several recent results about hybrid automata. Our goal is to demonstrate that concepts from the theory of discrete concurrent systems can give insights into partly continuous systems, and that methods for the verification of finite-state systems can be used to analyze certain systems with uncountable state spaces}, author = {Henzinger, Thomas A}, booktitle = {Proceedings 11th Annual IEEE Symposium on Logic in Computer Science}, issn = {1043-6871}, location = {New Brunswick, NJ, United States of America}, pages = {278 -- 292}, publisher = {IEEE}, title = {{The theory of hybrid automata}}, doi = {10.1109/LICS.1996.561342 }, year = {1996}, }