@article{11124, abstract = {Ran GTPase plays important roles in nucleocytoplasmic transport in interphase [1, 2] and in both spindle formation and nuclear envelope (NE) assembly during mitosis [3, 4, 5]. The latter functions rely on the presence of high local concentrations of GTP-bound Ran near mitotic chromatin [3, 4, 5]. RanGTP localization has been proposed to result from the association of Ran's GDP/GTP exchange factor, RCC1, with chromatin [6, 7, 8, 9], but Ran is shown here to bind directly to chromatin in two modes, either dependent or independent of RCC1, and, where bound, to increase the affinity of chromatin for NE membranes. We propose that the Ran binding capacity of chromatin contributes to localized spindle and NE assembly.}, author = {Bilbao-Cortés, Daniel and HETZER, Martin W and Längst, Gernot and Becker, Peter B. and Mattaj, Iain W.}, issn = {0960-9822}, journal = {Current Biology}, keywords = {General Agricultural and Biological Sciences, General Biochemistry, Genetics and Molecular Biology}, number = {13}, pages = {1151--1156}, publisher = {Elsevier BV}, title = {{Ran binds to chromatin by two distinct mechanisms}}, doi = {10.1016/s0960-9822(02)00927-2}, volume = {12}, year = {2002}, } @article{11123, abstract = {The small GTPase Ran is a key regulator of nucleocytoplasmic transport during interphase. The asymmetric distribution of the GTP-bound form of Ran across the nuclear envelope — that is, large quantities in the nucleus compared with small quantities in the cytoplasm — determines the directionality of many nuclear transport processes. Recent findings that Ran also functions in spindle formation and nuclear envelope assembly during mitosis suggest that Ran has a general role in chromatin-centred processes. Ran functions in these events as a signal for chromosome position.}, author = {HETZER, Martin W and Gruss, Oliver J. and Mattaj, Iain W.}, issn = {1476-4679}, journal = {Nature Cell Biology}, keywords = {Cell Biology}, number = {7}, pages = {E177--E184}, publisher = {Springer Nature}, title = {{The Ran GTPase as a marker of chromosome position in spindle formation and nuclear envelope assembly}}, doi = {10.1038/ncb0702-e177}, volume = {4}, year = {2002}, } @article{12659, abstract = {For many years considerable efforts have been put into investigating and modelling hydrological processes of mountainous catchments. On the one hand, the complexity and intrinsically high variability of the involved processes as well as insufficient knowledge of the underlying physical mechanisms still induce large uncertainties in understanding observed phenomena and predicting the behaviour of the system. On the other hand, the demand for models that are able to simulate mountainous water resource systems is increasing because of the needs related to both water exploitation and water conservation, which clearly call for an integrated vision and modelling of these systems. Accordingly, this paper moves from a brief survey of the most significant achievements in mountain hydrology to discuss what could be future challenging issues related to the broader spectrum of questions, which hydrologic modelling of mountainous river systems may face in the next decades. Firstly, reference is made to existing methodologies for modelling alpine water systems, focussing on some specific aspects that provide a basis for the discussion of the weaknesses and perspectives of present simulation tools. The future is thus discussed, delineating some of the research challenges that may foster a comprehensive and integrated vision of water related issues in mountainous regions.}, author = {Burlando, Paolo and Pellicciotti, Francesca and Strasser, Ulrich}, issn = {2224-7955}, journal = {Hydrology Research}, number = {1}, pages = {47--74}, publisher = {IWA Publishing}, title = {{Modelling mountainous water systems between learning and speculating looking for challenges}}, doi = {10.2166/nh.2002.0004}, volume = {33}, year = {2002}, } @inproceedings{1738, abstract = {New dyes of the type Ru(II)(bdmpp)(bpy) [where bdmpp is 2,6-bis(3,5-dimethyl-N-pyrazoyl)pyridine and bpy is 2,2′-bipyridine-4,4′-dicarboxylic acid] are prepared and characterized by infra-red (IR), mass (MS) and electrospray mass spectroscopy (ES-MS) as well as 1H NMR (1D and 2D) spectroscopies. The compounds present broad and very high intensity MLCT absorption bands in the visible and can be chemically anchored on TiO2 films via ester-like linkage involving carboxylato groups. These complexes have been tested with success as potential molecular antennas in dye-sensitized solar cells. Both opaque and transparent nanocrystalline TiO2 thin film electrodes obtained by a doctor blade technique sensitized by these complexes were incorporated in a sandwich type regenerative photoelectrochemical solar cell containing 0.1M LiI +0.01M I2 in propylene carbonate as well as a platinized conductive glass counter electrode. The cell was characterized by Raman spectroscopy under anodic and cathodic bias. Two new vibration bands were observed in the lower frequency region. The first one at 112 cm-1 is due to tri-iodide formed on the photoactive electrode, and the second one at 167 cm-1 is a sign of the dye/iodide interaction and corresponds to a vibration in a chemically stable "DI" intermediate species. Under direct sunlight illumination (solar irradiance of 60 mW/cm2) by using a composite polymer solid state electrolyte, the cell ITO/TiO2/[Ru(II)(bdmpp)(bpy)(NCS)](PF6)/electrolyte/Pt-ITO produced a continuous photocurrent as high as 4.29mA/cm2, and gave IPCE values about half of the corresponding values obtained by the standard N3 dye under the same conditions. The photovoltage is about 600 mV and the overall energy conversion cell's efficiency is as high as 1.72%.}, author = {Falaras, Polycarpos and Chryssou, Katerina and Stergiopoulos, Thomas and Arabatzis, Ioannis M and Georgios Katsaros and Catalano, Vincent J and Kurtaran, Raif and Hugot-Le Goff, Anne and Bernard, Marie C}, pages = {125 -- 135}, publisher = {SPIE}, title = {{Dye-sensitization of titanium dioxide thin films by Ru(II)-bpp-bpy complexes}}, doi = {10.1117/12.452446}, volume = {4801}, year = {2002}, } @article{1739, abstract = {Poly(ethylene oxide)/titania polymer electrolyte based photoelectrochemical cells have been fabricated with Ru(dcbpy)2(NCS)2 complex as the sensitizer and nanoporous TiO2 films as photoanodes. The introduction of the titania filler into the poly(ethylene oxide) matrix reduces the crystallinity of the polymer and enhances the mobility of the 1-/13 - redox couple, resulting in outstanding overall conversion efficiency (4.2% under direct sunlight illumination) of the corresponding dye-sensitized nanocrystalline TiO2 solar cell, one of the best efficiencies reported to date for a solid-state device.}, author = {Stergiopoulos, Thomas and Arabatzis, Iannis M and Georgios Katsaros and Falaras, Polycarpos}, journal = {Nano Letters}, number = {11}, pages = {1259 -- 1261}, publisher = {American Chemical Society}, title = {{Binary Polyethylene Oxide/Titania Solid-State Redox Electrolyte for Highly Efficient Nanocrystalline TiO2 Photoelectrochemical Cells}}, doi = {10.1021/nl025798u}, volume = {2}, year = {2002}, } @inproceedings{2339, author = {Robert Seiringer}, editor = {Weder, Richardo and Exner, Pavel and Grébert, Benoit}, pages = {281 -- 286}, publisher = {World Scientific Publishing}, title = {{Symmetry breaking in a model of a rotating Bose gas}}, doi = {10.1090/conm/307}, volume = {307}, year = {2002}, } @article{2351, abstract = {We study the Gross-Pitaevskii functional for a rotating two-dimensional Bose gas in a trap. We prove that there is a breaking of the rotational symmetry in the ground state; more precisely, for any value of the angular velocity and for large enough values of the interaction strength, the ground state of the functional is not an eigenfunction of the angular momentum. This has interesting consequences on the Bose gas with spin; in particular, the ground state energy depends non-trivially on the number of spin components, and the different components do not have the same wave function. For the special case of a harmonic trap potential, we give explicit upper and lower bounds on the critical coupling constant for symmetry breaking.}, author = {Robert Seiringer}, journal = {Communications in Mathematical Physics}, number = {3}, pages = {491 -- 509}, publisher = {Springer}, title = {{Gross-Pitaevskii theory of the rotating Bose gas}}, doi = {10.1007/s00220-002-0695-2}, volume = {229}, year = {2002}, } @article{2349, abstract = {The Bose-Einstein condensation (BEC) of the ground state of bosonic atoms in a trap was discussed. The BEC was proved for bosons with two-body repulsive interaction potentials in the dilute limit, starting from the basic Schrodinger equation. The BEC was 100% into the state which minimized the Gross-Pitaevskii energy functional. The analysis also included rigorous proof of BEC in a physically realistic, continuum model.}, author = {Lieb, Élliott H and Robert Seiringer}, journal = {Physical Review Letters}, number = {17}, pages = {1704091 -- 1704094}, publisher = {American Physical Society}, title = {{Proof of Bose-Einstein condensation for dilute trapped gases}}, doi = {10.1103/PhysRevLett.88.170409}, volume = {88}, year = {2002}, } @article{2352, abstract = {We present a generalization of the Fefferman-de la Llave decomposition of the Coulomb potential to quite arbitrary radial functions V on ℝn going to zero at infinity. This generalized decomposition can be used to extend previous results on N-body quantum systems with Coulomb interaction to a more general class of interactions. As an example of such an application, we derive the high density asymptotics of the ground state energy of jellium with Yukawa interaction in the thermodynamic limit, using a correlation estimate by Graf and Solovej.}, author = {Hainzl, Christian and Robert Seiringer}, journal = {Letters in Mathematical Physics}, number = {1}, pages = {75 -- 84}, publisher = {Springer}, title = {{General decomposition of radial functions on ℝn and applications to N-body quantum systems}}, doi = {10.1023/A:1020204818938}, volume = {61}, year = {2002}, } @article{2617, abstract = {Synapses exhibit different short-term plasticity patterns and this behaviour influences information processing in neuronal networks. We tested how the short-term plasticity of excitatory postsynaptic currents (EPSCs) depends on the postsynaptic cell type, identified by axonal arborizations and molecular markers in the hippocampal CA1 area. Three distinct types of short-term synaptic behaviour (facilitating, depressing and combined facilitating-depressing) were defined by fitting a dynamic neurotransmission model to the data. Approximately 75 % of the oriens-lacunosum-moleculare (O-LM) interneurones received facilitating EPSCs, but in three of 12 O-LM cells EPSCs also showed significant depression. Over 90 % of the O-LM cells were immunopositive for somatostatin and mGluR1α and all tested cells were decorated by strongly mGluR7a positive axon terminals. Responses in eight of 12 basket cells were described well with a model involving only depression, but the other cells displayed combined facilitating-depressing EPSCs. No apparent difference was found between the plasticity of EPSCs in cholecystokinin- or parvalbumin-containing basket cells. In oriens-bistratified cells (O-Bi), two of nine cells showed facilitating EPSCs, another two depressing, and the remaining five cells combined facilitating-depressing EPSCs. Seven of 10 cells tested for somatostatin were immunopositive, but mGluR1α was detectable only in two of 11 tested cells. Furthermore, most O-Bi cells projected to the CA3 area and the subiculum, as well as outside the hippocampal formation. Postsynaptic responses to action potentials recorded in vivo from a CA1 place cell were modelled, and revealed great differences between and within cell types. Our results demonstrate that the short-term plasticity of EPSCs is cell type dependent, but with significant heterogeneity within all three interneurone populations.}, author = {Losonczy, Attila and Zhang, Limei and Ryuichi Shigemoto and Somogyi, Péter and Nusser, Zoltán}, journal = {Journal of Physiology}, number = {1}, pages = {193 -- 210}, publisher = {Wiley-Blackwell}, title = {{Cell type dependence and variability in the short-term plasticity of EPSCs in identified mouse hippocampal interneurones}}, doi = {10.1113/jphysiol.2002.020024}, volume = {542}, year = {2002}, } @inproceedings{2708, author = {László Erdös}, pages = {129 -- 133}, publisher = {World Scientific Publishing}, title = {{Two dimensional Pauli operator via scalar potential}}, doi = {10.1090/conm/307}, volume = {307}, year = {2002}, } @article{2991, abstract = {Polar auxin transport controls multiple aspects of plant development including differential growth, embryo and root patterning and vascular tissue differentiation. Identification of proteins involved in this process and availability of new tools enabling `visualization' of auxin and auxin routes in planta largely contributed to the significant progress that has recently been made. New data support classical concepts, but several recent findings are likely to challenge our view on the mechanism of auxin transport. The aim of this review is to provide a comprehensive overview of the polar auxin transport field. It starts with classical models resulting from physiological studies, describes the genetic contributions and discusses the molecular basis of auxin influx and efflux. Finally, selected questions are presented in the context of developmental biology, integrating available data from different fields.}, author = {Friml, Jirí and Palme, Klaus}, journal = {Plant Molecular Biology}, number = {3-4}, pages = {273 -- 284}, publisher = {Springer}, title = {{Polar auxin transport - Old questions and new concepts?}}, doi = {10.1023/A:1015248926412}, volume = {49}, year = {2002}, } @misc{3508, abstract = {A method of automatic conversion of a physical object into a three-dimensional digital model. The method acquires a set of measured data points on the surface of a physical model. From the measured data points, the method reconstructs a digital model of the physical object using a Delaunay complex of the points, a flow strcuture of the simplicies in the Delaunay complex and retracting the Delaunay complex into a digital model of the physical object using the flow structure. The method then outputs the digital model of the physical object.}, author = {Edelsbrunner, Herbert and Fu, Ping}, title = {{Methods of generating three-dimensional digital models of objects by wrapping point cloud data points}}, year = {2002}, } @inproceedings{3448, author = {Mallick, Sanhita and Krishnendu Chatterjee and Merchant, Arif N and Dasgupta, Pallab}, publisher = {Elsevier}, title = {{Implementation of shape grammar for plan analysis}}, year = {2002}, } @phdthesis{4414, abstract = {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.}, author = {Mang, Freddy}, pages = {1 -- 116}, publisher = {University of California, Berkeley}, title = {{Games in open systems verification and synthesis}}, year = {2002}, } @article{6158, abstract = {Wild isolates of Caenorhabditis elegans can feed either alone or in groups1,2. This natural variation in behaviour is associated with a single residue difference in NPR-1, a predicted G-protein-coupled neuropeptide receptor related to Neuropeptide Y receptors2. Here we show that the NPR-1 isoform associated with solitary feeding acts in neurons exposed to the body fluid to inhibit social feeding. Furthermore, suppressing the activity of these neurons, called AQR, PQR and URX, using an activated K+ channel, inhibits social feeding. NPR-1 activity in AQR, PQR and URX neurons seems to suppress social feeding by antagonizing signalling through a cyclic GMP-gated ion channel encoded by tax-2 and tax-4. We show that mutations in tax-2 or tax-4 disrupt social feeding, and that tax-4 is required in several neurons for social feeding, including one or more of AQR, PQR and URX. The AQR, PQR and URX neurons are unusual in C. elegans because they are directly exposed to the pseudocoelomic body fluid3. Our data suggest a model in which these neurons integrate antagonistic signals to control the choice between social and solitary feeding behaviour.}, author = {Coates, Juliet C. and de Bono, Mario}, issn = {0028-0836}, journal = {Nature}, number = {6910}, pages = {925--929}, publisher = {Springer Nature}, title = {{Antagonistic pathways in neurons exposed to body fluid regulate social feeding in Caenorhabditis elegans}}, doi = {10.1038/nature01170}, volume = {419}, year = {2002}, } @article{6159, abstract = {Natural Caenorhabditis elegans isolates exhibit either social or solitary feeding on bacteria. We show here that social feeding is induced by nociceptive neurons that detect adverse or stressful conditions. Ablation of the nociceptive neurons ASH and ADL transforms social animals into solitary feeders. Social feeding is probably due to the sensation of noxious chemicals by ASH and ADL neurons; it requires the genes ocr-2 and osm-9, which encode TRP-related transduction channels, and odr-4 and odr-8, which are required to localize sensory chemoreceptors to cilia. Other sensory neurons may suppress social feeding, as social feeding in ocr-2 and odr-4 mutants is restored by mutations in osm-3, a gene required for the development of 26 ciliated sensory neurons. Our data suggest a model for regulation of social feeding by opposing sensory inputs: aversive inputs to nociceptive neurons promote social feeding, whereas antagonistic inputs from neurons that express osm-3 inhibit aggregation.}, author = {de Bono, Mario and Tobin, David M. and Davis, M. Wayne and Avery, Leon and Bargmann, Cornelia I.}, issn = {0028-0836}, journal = {Nature}, number = {6910}, pages = {899--903}, publisher = {Springer Nature}, title = {{Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli}}, doi = {10.1038/nature01169}, volume = {419}, year = {2002}, } @inproceedings{4631, abstract = {We present a theory of timed interfaces, which is capable of specifying both the timing of the inputs a component expects from the environment, and the timing of the outputs it can produce. Two timed interfaces are compatible if there is a way to use them together such that their timing expectations are met. Our theory provides algorithms for checking the compatibility between two interfaces and for deriving the composite interface; the theory can thus be viewed as a type system for real-time interaction. Technically, a timed interface is encoded as a timed game between two players, representing the inputs and outputs of the component. The algorithms for compatibility checking and interface composition are thus derived from algorithms for solving timed games.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Stoelinga, Mariëlle}, booktitle = {Proceedings of the 2nd International Conference on Embedded Software}, isbn = {9783540443070}, location = {Grenoble, France}, pages = {108 -- 122}, publisher = {ACM}, title = {{Timed interfaces}}, doi = {10.1007/3-540-45828-X_9}, volume = {2491}, year = {2002}, } @inproceedings{4562, abstract = {We present interface models that describe both the input assumptions of a component, and its output behavior. By enabling us to check that the input assumptions of a component are met in a design, interface models provide a compatibility check for component-based design. When refining a design into an implementation, interface models require that the output behavior of a component satisfies the design specification only when the input assumptions of the specification are satisfied, yielding greater flexibility in the choice of implementations. Technically, our interface models are games between two players, Input and Output; the duality of the players accounts for the dual roles of inputs and outputs in composition and refinement. We present two interface models in detail, one for a simple synchronous form of interaction between components typical in hardware, and the other for more complex synchronous interactions on bidirectional connections. As an example, we specify the interface of a bidirectional bus, with the input assumption that at any time at most one component has write access to the bus. For these interface models, we present algorithms for compatibility and refinement checking, and we describe efficient symbolic implementations.}, author = {Chakrabarti, Arindam and De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy}, booktitle = {Proceedings of the 14th International Conference on Computer Aided Verification}, isbn = {9783540439974}, location = {Copenhagen, Denmark}, pages = {414 -- 427}, publisher = {Springer}, title = {{Synchronous and bidirectional component interfaces}}, doi = {10.1007/3-540-45657-0_34}, volume = {2404}, year = {2002}, } @inproceedings{4565, abstract = {In the literature, we find several formulations of the control problem for timed and hybrid systems. We argue that formulations where a controller can cause an action at any point in dense (rational or real) time are problematic, by presenting an example where the controller must act faster and faster, yet causes no Zeno effects (say, the control actions are at times 0, 1/2, 1, 1 1/4, 2, 2 1/8, 3, 3 1/16 ,...). Such a controller is, of course, not implementable in software. Such controllers are avoided by formulations where the controller can cause actions only at discrete (integer) points in time. While the resulting control problem is well- understood if the time unit, or “sampling rate” of the controller, is fixed a priori, we define a novel, stronger formulation: the discrete-time control problem with unknown sampling rate asks if a sampling controller exists for some sampling rate. We prove that this problem is undecidable even in the special case of timed automata.}, author = {Cassez, Franck and Henzinger, Thomas A and Raskin, Jean}, booktitle = {Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control}, isbn = {9783540433217}, location = {Stanford, CA, USA}, pages = {134 -- 148}, publisher = {Springer}, title = {{A comparison of control problems for timed and hybrid systems}}, doi = {10.1007/3-540-45873-5_13}, volume = {2289}, year = {2002}, } @article{4595, abstract = {Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator "eventually" with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. The problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas. Depending on whether or not we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL*.ATL and ATL* are interpreted over concurrent game structures. Every state transition of a concurrent game structure results from a choice of moves, one for each player. The players represent individual components and the environment of an open system. Concurrent game structures can capture various forms of synchronous composition for open systems, and if augmented with fairness constraints, also asynchronous composition. Over structures without fairness constraints, the model-checking complexity of ATL is linear in the size of the game structure and length of the formula, and the symbolic model-checking algorithm for CTL extends with few modifications to ATL. Over structures with weak-fairness constraints, ATL model checking requires the solution of 1-pair Rabin games, and can be done in polynomial time. Over structures with strong-fairness constraints, ATL model checking requires the solution of games with Boolean combinations of Büchi conditions, and can be done in PSPACE. In the case of ATL*, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time.}, author = {Alur, Rajeev and Henzinger, Thomas A and Kupferman, Orna}, issn = {0004-5411}, journal = {Journal of the ACM}, number = {5}, pages = {672 -- 713}, publisher = {ACM}, title = {{Alternating-time temporal logic}}, doi = {10.1145/585265.585270}, volume = {49}, year = {2002}, } @inproceedings{4471, abstract = {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.}, author = {Henzinger, Thomas A and Krishnan, Sriram and Kupferman, Orna and Mang, Freddy}, booktitle = {Proceedings of the 29th International Colloquium on Automata, Languages and Programming}, isbn = {9783540438649}, location = {Malaga, Spain}, pages = {644 -- 656}, publisher = {Springer}, title = {{Synthesis of uninitialized systems}}, doi = {10.1007/3-540-45465-9_55}, volume = {2380}, year = {2002}, } @article{4474, abstract = {The simulation preorder for labeled transition systems is defined locally, and operationally, as a game that relates states with their immediate successor states. Simulation enjoys many appealing properties. First, simulation has a denotational characterization: system S simulates system I iff every computation tree embedded in the unrolling of I can be embedded also in the unrolling of S. Second, simulation has a logical characterization: S simulates I iff every universal branching-time formula satisfied by S is satisfied also by I. It follows that simulation is a suitable notion of implementation, and it is the coarsest abstraction of a system that preserves universal branching-time properties. Third, based on its local definition, simulation between finite-state systems can be checked in polynomial time. Finally, simulation implies trace containment, which cannot be defined locally and requires polynomial space for verification. Hence simulation is widely used both in manual and in automatic verification. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We propose a new view of fair simulation by extending the local definition of simulation to account for fairness: system View the MathML sourcefairly simulates system View the MathML source iff in the simulation game, there is a strategy that matches with each fair computation of View the MathML source a fair computation of View the MathML source. Our definition enjoys a denotational characterization and has a logical characterization: View the MathML source fairly simulates View the MathML source iff every fair computation tree (whose infinite paths are fair) embedded in the unrolling of View the MathML source can be embedded also in the unrolling of View the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by View the MathML source is satisfied also by View the MathML source (∀AFMC is the universal fragment of the alternation-free μ-calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace containment and is therefore useful as an efficiently computable local criterion for proving linear-time abstraction hierarchies of fair systems.}, author = {Henzinger, Thomas A and Kupferman, Orna and Rajamani, Sriram}, issn = {0890-5401}, journal = {Information and Computation}, number = {1}, pages = {64 -- 81}, publisher = {Elsevier}, title = {{Fair simulation}}, doi = {10.1006/inco.2001.3085}, volume = {173}, year = {2002}, } @inproceedings{4563, abstract = {We present a formal methodology and tool for uncovering errors in the interaction of software modules. Our methodology consists of a suite of languages for defining software interfaces, and algorithms for checking interface compatibility. We focus on interfaces that explain the method-call dependencies between software modules. Such an interface makes assumptions about the environment in the form of call and availability constraints. A call constraint restricts the accessibility of local methods to certain external methods. An availability constraint restricts the accessibility of local methods to certain states of the module. For example, the interface for a file server with local methods open and read may assert that a file cannot be read without having been opened. Checking interface compatibility requires the solution of games, and in the presence of availability constraints, of pushdown games. Based on this methodology, we have implemented a tool that has uncovered incompatibilities in TinyOS, a small operating system for sensor nodes in adhoc networks.}, author = {Chakrabarti, Arindam and De Alfaro, Luca and Henzinger, Thomas A and Jurdziński, Marcin and Mang, Freddy}, booktitle = {Proceedings of the 14th International Conference on Computer Aided Verification}, isbn = { 9783540439974}, location = {Copenhagen, Denmark}, pages = {428 -- 441}, publisher = {Springer}, title = {{Interface compatibility checking for software modules}}, doi = {10.1007/3-540-45657-0_35}, volume = {2404}, year = {2002}, } @inproceedings{4472, abstract = {We present a methodology and tool for verifying and certifying systems code. The verification is based on the lazy-abstraction paradigm for intertwining the following three logical steps: construct a predicate abstraction from the code, model check the abstraction, and automatically refine the abstraction based on counterexample analysis. The certification is based on the proof-carrying code paradigm. Lazy abstraction enables the automatic construction of small proof certificates. The methodology is implemented in Blast, the Berkeley Lazy Abstraction Software verification Tool. We describe our experience applying Blast to Linux and Windows device drivers. Given the C code for a driver and for a temporal-safety monitor, Blast automatically generates an easily checkable correctness certificate if the driver satisfies the specification, and an error trace otherwise.}, author = {Henzinger, Thomas A and Necula, George and Jhala, Ranjit and Sutre, Grégoire and Majumdar, Ritankar and Weimer, Westley}, booktitle = {Proceedings of the 14th International Conference on Computer Aided Verification}, isbn = {9783540439974}, location = {Copenhagen, Denmark}, pages = {526 -- 538}, publisher = {Springer}, title = {{Temporal safety proofs for systems code}}, doi = {10.1007/3-540-45657-0_45}, volume = {2404}, year = {2002}, } @inproceedings{4470, abstract = {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.}, author = {Henzinger, Thomas A and Kirsch, Christoph and Majumdar, Ritankar and Matic, Slobodan}, booktitle = {Proceedings of the 2nd International Conference on Embedded Software}, isbn = {9783540443070}, location = {Grenoble, France}, pages = {76 -- 92}, publisher = {ACM}, title = {{Time-safety checking for embedded programs}}, doi = {10.1007/3-540-45828-X_7}, volume = {2491}, year = {2002}, } @inproceedings{4444, abstract = {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.}, author = {Henzinger, Thomas A and Kirsch, Christoph}, booktitle = {Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation}, isbn = {9781581134636}, location = {Berlin, Germany}, pages = {315 -- 326}, publisher = {ACM}, title = {{The embedded machine: predictable, portable real-time code}}, doi = {10.1145/512529.512567}, year = {2002}, } @inproceedings{4476, abstract = {One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.}, author = {Henzinger, Thomas A and Jhala, Ranjit and Majumdar, Ritankar and Sutre, Grégoire}, booktitle = {Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, isbn = {9781581134506}, location = {Portland, OR, USA}, pages = {58 -- 70}, publisher = {ACM}, title = {{Lazy abstraction}}, doi = {10.1145/503272.503279}, year = {2002}, } @article{4473, abstract = {The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P ≤s Q, denoting "P is simulated by Q," into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P ≤s Q. We also extend our assume-guarantee rule to account for fairness constraints on transition systems.}, author = {Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram and Tasiran, Serdar}, issn = {0164-0925}, journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, number = {1}, pages = {51 -- 64}, publisher = {ACM}, title = {{An assume-guarantee rule for checking simulation}}, doi = {10.1145/509705.509707}, volume = {24}, year = {2002}, } @inproceedings{4423, abstract = {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).}, author = {Horowitz, Benjamin and Liebman, Judith and Ma, Cedric and Koo, T John and Henzinger, Thomas A and Sangiovanni Vincentelli, Alberto and Sastry, Shankar}, booktitle = {Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control}, issn = {1474-6670}, location = {Barcelona, Spain}, number = {1}, publisher = {Elsevier}, title = {{Embedded software design and system integration for rotorcraft UAV using platforms}}, doi = {10.3182/20020721-6-ES-1901.01628}, volume = {15}, year = {2002}, } @inproceedings{4421, abstract = {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.}, author = {Kirsch, Christoph and Sanvido, Marco and Henzinger, Thomas A and Pree, Wolfgang}, booktitle = {Proceedings of the 2nd International Conference on Embedded Software}, isbn = {9783540443070}, location = {Grenoble, France}, pages = {46 -- 60}, publisher = {ACM}, title = {{A Giotto-based helicopter control system}}, doi = {10.1007/3-540-45828-X_5}, volume = {2491}, year = {2002}, } @inproceedings{4422, abstract = {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.}, author = {Jurdziński, Marcin and Kupferman, Orna and Henzinger, Thomas A}, booktitle = {Proceedings of the 16th International Workshop on Computer Science Logic}, isbn = {9783540442400}, location = {Edinburgh, Scotland}, pages = {292 -- 305}, publisher = {Springer}, title = {{Trading probability for fairness}}, doi = {10.1007/3-540-45793-3_20}, volume = {2471}, year = {2002}, } @inproceedings{4413, abstract = {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.}, author = {Passerone, Roberto and De Alfaro, Luca and Henzinger, Thomas A and Sangiovanni Vincentelli, Alberto}, booktitle = {Proceedings of the 11th IEEE/ACM international conference on Computer-aided design}, isbn = {9780780376076}, location = {San Jose, CA, USA}, pages = {132 -- 139}, publisher = {IEEE}, title = {{Convertibility verification and converter synthesis: Two faces of the same coin}}, doi = {10.1145/774572.774592}, year = {2002}, } @article{4262, abstract = {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.}, author = {Barton, Nicholas H and Navarro, Arcadio}, issn = {0016-6723}, journal = {Genetical Research}, number = {2}, pages = {129 -- 139}, publisher = {Cambridge University Press}, title = {{Extending the coalescent to multilocus systems: the case of balancing selection}}, doi = {10.1017/S0016672301005493}, volume = {79}, year = {2002}, } @article{4260, abstract = {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. }, author = {Johnson, Toby and Barton, Nicholas H}, issn = {0016-6731}, journal = {Genetics}, number = {1}, pages = {395 -- 411}, publisher = {Genetics Society of America}, title = {{The effect of deleterious alleles on adaptation in asexual populations}}, doi = {10.1093/genetics/162.1.395}, volume = {162}, year = {2002}, } @article{4349, abstract = {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.}, author = {Bollback, Jonathan P}, issn = {0737-4038}, journal = {Molecular Biology and Evolution}, number = {7}, pages = {1171 -- 80}, publisher = {Oxford University Press}, title = {{Bayesian model adequacy and choice in phylogenetics}}, doi = {10.1093/oxfordjournals.molbev.a004175}, volume = {19}, year = {2002}, } @article{4263, abstract = {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.}, author = {Barton, Nicholas H and Depaulis, Frantz and Etheridge, Alison}, issn = {0040-5809}, journal = {Theoretical Population Biology}, number = {1}, pages = {31 -- 48}, publisher = {Academic Press}, title = {{Neutral evolution in spatially continuous populations}}, doi = {10.1006/tpbi.2001.1557}, volume = {61}, year = {2002}, } @article{4261, abstract = {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.}, author = {Barton, Nicholas H and Keightley, Peter}, issn = {1471-0056}, journal = {Nature Reviews Genetics}, pages = {11 -- 21}, publisher = {Nature Publishing Group}, title = {{Understanding quantitative genetic variation}}, doi = {10.1038/nrg700}, volume = {3}, year = {2002}, } @article{4347, abstract = {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.}, author = {Huelsenbeck, John and Bollback, Jonathan P and Levine, Amy}, issn = {0039-7989}, journal = {Systematic Biology}, number = {1}, pages = {32 -- 43}, publisher = {Oxford University Press}, title = {{Inferring the root of a phylogenetic tree}}, doi = {10.1080/106351502753475862}, volume = {51}, year = {2002}, } @article{4407, abstract = {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).}, author = {Raskin, Jean and Schobbens, Pierre and Henzinger, Thomas A}, issn = {0304-3975}, journal = {Theoretical Computer Science}, number = {1-2}, pages = {151 -- 182}, publisher = {Elsevier}, title = {{Axioms for real-time logics}}, doi = {10.1016/S0304-3975(00)00308-X}, volume = {274}, year = {2002}, } @article{4258, abstract = {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.}, author = {Navarro, Arcadio and Barton, Nicholas H}, issn = {0016-6731}, journal = {Genetics}, number = {2}, pages = {849 -- 863}, publisher = {Genetics Society of America}, title = {{The effects of multilocus balancing selection on neutral variability}}, doi = {10.1093/genetics/161.2.849}, volume = {161}, year = {2002}, } @article{4259, abstract = {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. }, author = {Orive, Maria and Barton, Nicholas H}, issn = {0016-6731}, journal = {Genetics}, number = {3}, pages = {1469 -- 1485}, publisher = {Genetics Society of America}, title = {{Associations between cytoplasmic and nuclear loci in hybridizing populations}}, doi = {10.1093/genetics/162.3.1469}, volume = {162}, year = {2002}, } @article{4209, abstract = {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.}, author = {Hannus, Michael and Feiguin, Fabian and Heisenberg, Carl-Philipp J and Eaton, Suzanne}, issn = {0950-1991}, journal = {Development}, number = {14}, pages = {3493 -- 3503}, publisher = {Company of Biologists}, title = {{Planar cell polarization requires Widerborst, a B′ regulatory subunit of protein phosphatase 2A}}, doi = {10.1242/dev.129.14.3493}, volume = {129}, year = {2002}, } @article{4207, abstract = {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.}, author = {Heisenberg, Carl-Philipp J}, issn = {0960-9822}, journal = {Current Biology}, number = {19}, pages = {R657 -- R659}, publisher = {Cell Press}, title = {{Wnt signalling: Refocusing on Strabismus}}, doi = {10.1016/S0960-9822(02)01160-0}, volume = {12}, year = {2002}, } @article{4194, abstract = {Cells at the anterior boundary of the neural plate (ANB) can induce telencephalic gene expression when transplanted to more posterior regions. Here, we identify a secreted Frizzled-related Wnt antagonist, Tic, that is expressed in ANB cells and can cell nonautonomously promote telencephalic gene expression in a concentration-dependent manner. Moreover, abrogation of Tlc function compromises telencephalic development. We also identify Wnt8b as a locally acting modulator of regional fate in the anterior neural plate and a likely target for antagonism by Tic. Finally, we show that tlc expression is regulated by signals that establish early antero-posterior and dorso-ventral ectodermal pattern. From these studies, we propose that local antagonism of Wnt activity within the anterior ectoderm is required to establish the telencephalon.}, author = {Houart, Corinne and Caneparo, Luca and Heisenberg, Carl-Philipp J and Barth, K Anukampa and Take Uchi, Masaya and Wilson, Stephen}, issn = {0896-6273}, journal = {Neuron}, number = {2}, pages = {255 -- 265}, publisher = {Elsevier}, title = {{Establishment of the telencephalon during gastrulation by local antagonism of Wnt signaling}}, doi = {10.1016/S0896-6273(02)00751-1}, volume = {35}, year = {2002}, } @article{4148, abstract = {Members of the Wnt family have been implicated in a variety of developmental processes including axis formation, Patterning of the central nervous system and tissue morphogenesis. Recent studies have shown that a Wnt signalling pathway similar to that involved in the establishment of planar cell polarity in Drosophila regulates convergent extension movements during zebrafish and Xenopus gastrulation. This finding provides a good starting point to dissect the complex cell biology and genetic regulation of vertebrate gastrulation movements.}, author = {Tada, Masazumi and Concha, Miguel and Heisenberg, Carl-Philipp J}, issn = {1084-9521}, journal = {Seminars in Cell & Developmental Biology}, number = {3}, pages = {251 -- 260}, publisher = {Academic Press}, title = {{Non-canonical Wnt signalling and regulation of gastrulation movements}}, doi = {10.1016/S1084-9521(02)00052-6}, volume = {13}, year = {2002}, } @article{4196, abstract = {During vertebrate gastrulation, large cellular rearrangements lead to the formation of the three germ layers, ectoderm, mesoderm and endoderm. Zebrafish offer many genetic and experimental advantages for studying vertebrate gastrulation movements. For instance, several mutants, including silberblick, knypek and trilobite, exhibit defects in morphogenesis during gastrulation. The identification of the genes mutated in these lines together with the analysis of the mutant phenotypes has provided new insights into the molecular and cellular mechanisms that underlie vertebrate gastrulation movements.}, author = {Heisenberg, Carl-Philipp J and Tada, Masazumi}, issn = {1084-9521}, journal = {Seminars in Cell & Developmental Biology}, number = {6}, pages = {471 -- 479}, publisher = {Academic Press}, title = {{Zebrafish gastrulation movements: bridging cell and developmental biology}}, doi = {10.1016/S1084952102001003}, volume = {13}, year = {2002}, } @article{4199, abstract = {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.}, author = {Heisenberg, Carl-Philipp J and Tada, Masazumi}, issn = {0960-9822}, journal = {Current Biology}, number = {4}, pages = {R126 -- R128}, publisher = {Cell Press}, title = {{Wnt signalling: A moving picture emerges from van gogh}}, doi = {10.1016/S0960-9822(02)00704-2}, volume = {12}, year = {2002}, } @article{4139, abstract = {Pilot studies in England by Stopka and Macdonald revealed that allogrooming in the Old World wood mouse, Apodemus sylvaticus, is a commodity that males can trade for reproductive benefits with females. This study, which used a combination of field study and observations in experimental enclosures, revealed that specific experimental conditions such as group-size and sex-ratio manipulations have a significant effect on the pattern of allogrooming exchanged between individuals. Furthermore, females from the Czech population were more likely to associate with each other as revealed by the clustering of activity centers of females (i.e., as opposed to almost exclusive ranges in English populations), and also by the higher intensity of allogrooming exchanged between females (i.e., virtually lacking in the previous experiment with English mice). Therefore, geographic variation and specific social conditions seem to be important driving factors for allogrooming behavior. Together with changes in overall grooming patterns, allogrooming between males and females remained invariably asymmetrical over all four experimental groups (i.e., two conditions for each sex) in that males provided more allogrooming to females than they received from them.}, author = {Polechova, Jitka and Stopka, P.}, issn = {0008-4301}, journal = {Canadian Journal of Zoology}, number = {8}, pages = {1383 -- 1388}, publisher = {NRC Research Press}, title = {{Geometry of social relationships in the Old World wood mouse, Apodemus sylvaticus}}, doi = {10.1139/z02-128}, volume = {80}, year = {2002}, } @inproceedings{4003, abstract = {The writhing number measures the global geometry of a closed space curve or knot. We show that this measure is related to the average winding number of its Gauss map. Using this relationship, we give an algorithm for computing the writhing number for a polygonal knot with n edges in time roughly proportional to n(1.6). We also implement a different, simple algorithm and provide experimental evidence for its practical efficiency.}, author = {Agarwal, Pankaj and Edelsbrunner, Herbert and Wang, Yusu}, booktitle = {Proceedings of the 13th annual ACM-SIAM symposium on Discrete algorithms}, isbn = {9780898715132}, location = {San Francisco, CA, USA}, pages = {791 -- 799}, publisher = {SIAM}, title = {{Computing the writhing number of a polygonal knot}}, year = {2002}, }