TY - CONF AU - Robert Seiringer ED - Weder, Richardo ED - Exner, Pavel ED - Grébert, Benoit ID - 2339 TI - Symmetry breaking in a model of a rotating Bose gas VL - 307 ER - TY - JOUR AB - 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. AU - Robert Seiringer ID - 2351 IS - 3 JF - Communications in Mathematical Physics TI - Gross-Pitaevskii theory of the rotating Bose gas VL - 229 ER - TY - JOUR AB - 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. AU - Lieb, Élliott H AU - Robert Seiringer ID - 2349 IS - 17 JF - Physical Review Letters TI - Proof of Bose-Einstein condensation for dilute trapped gases VL - 88 ER - TY - JOUR AB - 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. AU - Hainzl, Christian AU - Robert Seiringer ID - 2352 IS - 1 JF - Letters in Mathematical Physics TI - General decomposition of radial functions on ℝn and applications to N-body quantum systems VL - 61 ER - TY - JOUR AB - 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. AU - Losonczy, Attila AU - Zhang, Limei AU - Ryuichi Shigemoto AU - Somogyi, Péter AU - Nusser, Zoltán ID - 2617 IS - 1 JF - Journal of Physiology TI - Cell type dependence and variability in the short-term plasticity of EPSCs in identified mouse hippocampal interneurones VL - 542 ER - TY - CONF AU - László Erdös ID - 2708 TI - Two dimensional Pauli operator via scalar potential VL - 307 ER - TY - JOUR AB - 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. AU - Friml, Jirí AU - Palme, Klaus ID - 2991 IS - 3-4 JF - Plant Molecular Biology TI - Polar auxin transport - Old questions and new concepts? VL - 49 ER - TY - GEN AB - 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. AU - Edelsbrunner, Herbert AU - Fu, Ping ID - 3508 TI - Methods of generating three-dimensional digital models of objects by wrapping point cloud data points ER - TY - CONF AU - Mallick, Sanhita AU - Krishnendu Chatterjee AU - Merchant, Arif N AU - Dasgupta, Pallab ID - 3448 TI - Implementation of shape grammar for plan analysis ER - TY - THES AB - This dissertation investigates game-theoretic approaches to the algorithmic analysis of concurrent, reactive systems. A concurrent system comprises a number of components working concurrently; a reactive system maintains an ongoing interaction with its environment. Traditional approaches to the formal analysis of concurrent reactive systems usually view the system as an unstructured state-transition graphs; instead, we view them as collections of interacting components, where each one is an open system which accepts inputs from the other components. The interactions among the components are naturally modeled as games. Adopting this game-theoretic view, we study three related problems pertaining to the verification and synthesis of systems. Firstly, we propose two novel game-theoretic techniques for the model-checking of concurrent reactive systems, and improve the performance of model-checking. The first technique discovers an error as soon as it cannot be prevented, which can be long before it actually occurs. This technique is based on the key observation that "unpreventability" is a local property to a module: an error is unpreventable in a module state if no environment can prevent it. The second technique attempts to decompose a model-checking proof into smaller proof obligations by constructing abstract modules automatically, using reachability and "unpreventability" information about the concrete modules. Three increasingly powerful proof decomposition rules are proposed and we show that in practice, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification. Both techniques fall into the category of compositional reasoning. Secondly, we investigate the composition and control of synchronous systems. An essential property of synchronous systems for compositional reasoning is non-blocking. In the composition of synchronous systems, however, due to circular causal dependency of input and output signals, non-blocking is not always guaranteed. Blocking compositions of systems can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping systems with types, which make the dependencies between input and output signals transparent. We characterize various typing mechanisms in game-theoretic terms, and study their effects on the controller synthesis problem. We show that our typing systems are general enough to capture interesting real-life synchronous systems such as all delay-insensitive digital circuits. We then study their corresponding single-step control problems --a restricted form of controller synthesis problem whose solutions can be iterated in appropriate manners to solve all LTL controller synthesis problems. We also consider versions of the controller synthesis problem in which the type of the controller is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions. Thirdly, we study the synthesis of a class of open systems, namely, uninitialized state machines. The sequential synthesis problem, which is closely related to Church's solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. We solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Buechi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. The lower bound proofs require nontrivial generic reductions. AU - Mang, Freddy ID - 4414 TI - Games in open systems verification and synthesis ER - TY - JOUR AB - 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. AU - Coates, Juliet C. AU - de Bono, Mario ID - 6158 IS - 6910 JF - Nature SN - 0028-0836 TI - Antagonistic pathways in neurons exposed to body fluid regulate social feeding in Caenorhabditis elegans VL - 419 ER - TY - JOUR AB - 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. AU - de Bono, Mario AU - Tobin, David M. AU - Davis, M. Wayne AU - Avery, Leon AU - Bargmann, Cornelia I. ID - 6159 IS - 6910 JF - Nature SN - 0028-0836 TI - Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli VL - 419 ER - TY - CONF AB - 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. AU - De Alfaro, Luca AU - Henzinger, Thomas A AU - Stoelinga, Mariëlle ID - 4631 SN - 9783540443070 T2 - Proceedings of the 2nd International Conference on Embedded Software TI - Timed interfaces VL - 2491 ER - TY - CONF AB - 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. AU - Chakrabarti, Arindam AU - De Alfaro, Luca AU - Henzinger, Thomas A AU - Mang, Freddy ID - 4562 SN - 9783540439974 T2 - Proceedings of the 14th International Conference on Computer Aided Verification TI - Synchronous and bidirectional component interfaces VL - 2404 ER - TY - CONF AB - 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. AU - Cassez, Franck AU - Henzinger, Thomas A AU - Raskin, Jean ID - 4565 SN - 9783540433217 T2 - Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control TI - A comparison of control problems for timed and hybrid systems VL - 2289 ER - TY - JOUR AB - 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. AU - Alur, Rajeev AU - Henzinger, Thomas A AU - Kupferman, Orna ID - 4595 IS - 5 JF - Journal of the ACM SN - 0004-5411 TI - Alternating-time temporal logic VL - 49 ER - TY - CONF AB - The sequential synthesis problem, which is closely related to Church’s solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. In this paper we solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Büchi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. We also study the problem of deciding whether a given specification is uninitialized, that is, if its uninitialized and initialized synthesis problems coincide. We show that this problem has, for each specification formalism, the same complexity as the equivalence problem. AU - Henzinger, Thomas A AU - Krishnan, Sriram AU - Kupferman, Orna AU - Mang, Freddy ID - 4471 SN - 9783540438649 T2 - Proceedings of the 29th International Colloquium on Automata, Languages and Programming TI - Synthesis of uninitialized systems VL - 2380 ER - TY - JOUR AB - 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. AU - Henzinger, Thomas A AU - Kupferman, Orna AU - Rajamani, Sriram ID - 4474 IS - 1 JF - Information and Computation SN - 0890-5401 TI - Fair simulation VL - 173 ER - TY - CONF AB - 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. AU - Chakrabarti, Arindam AU - De Alfaro, Luca AU - Henzinger, Thomas A AU - Jurdziński, Marcin AU - Mang, Freddy ID - 4563 SN - 9783540439974 T2 - Proceedings of the 14th International Conference on Computer Aided Verification TI - Interface compatibility checking for software modules VL - 2404 ER - TY - CONF AB - 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. AU - Henzinger, Thomas A AU - Necula, George AU - Jhala, Ranjit AU - Sutre, Grégoire AU - Majumdar, Ritankar AU - Weimer, Westley ID - 4472 SN - 9783540439974 T2 - Proceedings of the 14th International Conference on Computer Aided Verification TI - Temporal safety proofs for systems code VL - 2404 ER - TY - CONF AB - Giotto is a platform-independent language for specifying software for high-performance control applications. In this paper we present a new approach to the compilation of Giotto. Following this approach, the Giotto compiler generates code for a virtual machine, called the E machine, which can be ported to different platforms. The Giotto compiler also checks if the generated E code is time safe for a given platform, that is, if the platform offers sufficient performance to ensure that the E code is executed in a timely fashion that conforms with the Giotto semantics. Time-safety checking requires a schedulability analysis. We show that while for arbitrary E code, the analysis is exponential, for E code generated from typical Giotto programs, the analysis is polynomial. This supports our claim that Giotto identifies a useful fragment of embedded programs. AU - Henzinger, Thomas A AU - Kirsch, Christoph AU - Majumdar, Ritankar AU - Matic, Slobodan ID - 4470 SN - 9783540443070 T2 - Proceedings of the 2nd International Conference on Embedded Software TI - Time-safety checking for embedded programs VL - 2491 ER - TY - CONF AB - The Embedded Machine is a virtual machine that mediates in real time the interaction between software processes and physical processes. It separates the compilation of embedded programs into two phases. The first, platform-independent compiler phase generates E code (code executed by the Embedded Machine), which supervises the timing ---not the scheduling--- of application tasks relative to external events, such as clock ticks and sensor interrupts. E~code is portable and exhibits, given an input behavior, predictable (i.e., deterministic) timing and output behavior. The second, platform-dependent compiler phase checks the time safety of the E code, that is, whether platform performance (determined by the hardware) and platform utilization (determined by the scheduler of the operating system) enable its timely execution. We have used the Embedded Machine to compile and execute high-performance control applications written in Giotto, such as the flight control system of an autonomous model helicopter. AU - Henzinger, Thomas A AU - Kirsch, Christoph ID - 4444 SN - 9781581134636 T2 - Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation TI - The embedded machine: predictable, portable real-time code ER - TY - CONF AB - 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. AU - Henzinger, Thomas A AU - Jhala, Ranjit AU - Majumdar, Ritankar AU - Sutre, Grégoire ID - 4476 SN - 9781581134506 T2 - Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages TI - Lazy abstraction ER - TY - JOUR AB - 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. AU - Henzinger, Thomas A AU - Qadeer, Shaz AU - Rajamani, Sriram AU - Tasiran, Serdar ID - 4473 IS - 1 JF - ACM Transactions on Programming Languages and Systems (TOPLAS) SN - 0164-0925 TI - An assume-guarantee rule for checking simulation VL - 24 ER - TY - CONF AB - Automation control systems typically incorporate legacy code and components that were originally designed to operate independently. Furthermore, they operate under stringent safety and timing constraints. Current design strategies deal with these requirements and characteristics with ad hoc approaches. In particular, when designing control laws, implementation constraints are often ignored or cursorily estimated. Indeed, costly redesigns are needed after a prototype of the control system is built due to missed timing constraints and subtle transient errors. In this paper, we use the concepts of platform-based design, and the Giotto programming language, to develop a methodology for the design of automation control systems that builds in modularity and correct-by-construction procedures. We illustrate our strategy by describing the (successful) application of the methodology to the design of a time-based control system for a rotorcraft Uninhabited Aerial Vehicle (UAV). AU - Horowitz, Benjamin AU - Liebman, Judith AU - Ma, Cedric AU - Koo, T John AU - Henzinger, Thomas A AU - Sangiovanni Vincentelli, Alberto AU - Sastry, Shankar ID - 4423 IS - 1 SN - 1474-6670 T2 - Proceedings of the 15th Triennial World Congress of the International Federation of Automatic Control TI - Embedded software design and system integration for rotorcraft UAV using platforms VL - 15 ER - TY - CONF AB - We demonstrate the feasibility and benefits of Giotto-based control software development by reimplementing the autopilot system of an autonomously flying model helicopter. Giotto offers a clean separation between the platform-independent concerns of software functionality and I/O timing, and the platform-dependent concerns of software scheduling and execution. Functionality code such as code computing control laws can be generated automatically from Simulink models or, as in the case of this project, inherited from a legacy system. I/O timing code is generated automatically from Giotto models that specify real-time requirements such as task frequencies and actuator update rates. We extend Simulink to support the design of Giotto models, and from these models, the automatic generation of Giotto code that supervises the interaction of the functionality code with the physical environment. The Giotto compiler performs a schedulability analysis on the Giotto code, and generates timing code for the helicopter platform. The Giotto methodology guarantees the stringent hard real-time requirements of the autopilot system, and at the same time supports the automation of the software development process in a way that produces a transparent software architecture with predictable behavior and reusable components. AU - Kirsch, Christoph AU - Sanvido, Marco AU - Henzinger, Thomas A AU - Pree, Wolfgang ID - 4421 SN - 9783540443070 T2 - Proceedings of the 2nd International Conference on Embedded Software TI - A Giotto-based helicopter control system VL - 2491 ER - TY - CONF AB - Behavioral properties of open systems can be formalized as objectives in two-player games. Turn-based games model asynchronous interaction between the players (the system and its environment) by interleaving their moves. Concurrent games model synchronous interaction: the players always move simultaneously. Infinitary winning criteria are considered: Büchi, co-Büchi, and more general parity conditions. A generalization of determinacy for parity games to concurrent parity games demands probabilistic (mixed) strategies: either player 1 has a mixed strategy to win with probability 1 (almost-sure winning), or player 2 has a mixed strategy to win with positive probability. This work provides efficient reductions of concurrent probabilistic Büchi and co-Büchi games to turn-based games with Büchi condition and parity winning condition with three priorities, respectively. From a theoretical point of view, the latter reduction shows that one can trade the probabilistic nature of almost-sure winning for a more general parity (fairness) condition. The reductions improve understanding of concurrent games and provide an alternative simple proof of determinacy of concurrent Büchi and co-Büchi games. From a practical point of view, the reductions turn solvers of turn-based games into solvers of concurrent probabilistic games. Thus improvements in the well-studied algorithms for the former carry over immediately to the latter. In particular, a recent improvement in the complexity of solving turn-based parity games yields an improvement in time complexity of solving concurrent probabilistic co-Büchi games from cubic to quadratic. AU - Jurdziński, Marcin AU - Kupferman, Orna AU - Henzinger, Thomas A ID - 4422 SN - 9783540442400 T2 - Proceedings of the 16th International Workshop on Computer Science Logic TI - Trading probability for fairness VL - 2471 ER - TY - CONF AB - An essential problem in component-based design is how to compose components designed in isolation. Several approaches have been proposed for specifying component interfaces that capture behavioral aspects such as interaction protocols, and for verifying interface compatibility. Likewise, several approaches have been developed for synthesizing converters between incompatible protocols. In this paper, we introduce the notion of adaptability as the property that two interfaces have when they can be made compatible by communicating through a converter that meets specified requirements. We show that verifying adaptability and synthesizing an appropriate converter are two faces of the same coin: adaptability can be formalized and solved using a game-theoretic framework, and then the converter can be synthesized as a strategy that always wins the game. Finally we show that this framework can be related to the rectification problem in trace theory. AU - Passerone, Roberto AU - De Alfaro, Luca AU - Henzinger, Thomas A AU - Sangiovanni Vincentelli, Alberto ID - 4413 SN - 9780780376076 T2 - Proceedings of the 11th IEEE/ACM international conference on Computer-aided design TI - Convertibility verification and converter synthesis: Two faces of the same coin ER - TY - JOUR AB - Natural populations are structured spatially into local populations and genetically into diverse ‘genetic backgrounds’ defined by different combinations of selected alleles. If selection maintains genetic backgrounds at constant frequency then neutral diversity is enhanced. By contrast, if background frequencies fluctuate then diversity is reduced. Provided that the population size of each background is large enough, these effects can be described by the structured coalescent process. Almost all the extant results based on the coalescent deal with a single selected locus. Yet we know that very large numbers of genes are under selection and that any substantial effects are likely to be due to the cumulative effects of many loci. Here, we set up a general framework for the extension of the coalescent to multilocus scenarios and we use it to study the simplest model, where strong balancing selection acting on a set of n loci maintains 2n backgrounds at constant frequencies and at linkage equilibrium. Analytical results show that the expected linked neutral diversity increases exponentially with the number of selected loci and can become extremely large. However, simulation results reveal that the structured coalescent approach breaks down when the number of backgrounds approaches the population size, because of stochastic fluctuations in background frequencies. A new method is needed to extend the structured coalescent to cases with large numbers of backgrounds. AU - Barton, Nicholas H AU - Navarro, Arcadio ID - 4262 IS - 2 JF - Genetical Research SN - 0016-6723 TI - Extending the coalescent to multilocus systems: the case of balancing selection VL - 79 ER - TY - JOUR AB - We calculate the fixation probability of a beneficial allele that arises as the result of a unique mutation in an asexual population that is subject to recurrent deleterious mutation at rate U. Our analysis is an extension of previous works, which make a biologically restrictive assumption that selection against deleterious alleles is stronger than that on the beneficial allele of interest. We show that when selection against deleterious alleles is weak, beneficial alleles that confer a selective advantage that is small relative to U have greatly reduced probabilities of fixation. We discuss the consequences of this effect for the distribution of effects of alleles fixed during adaptation. We show that a selective sweep will increase the fixation probabilities of other beneficial mutations arising during some short interval afterward. We use the calculated fixation probabilities to estimate the expected rate of fitness improvement in an asexual population when beneficial alleles arise continually at some low rate proportional to U. We estimate the rate of mutation that is optimal in the sense that it maximizes this rate of fitness improvement. Again, this analysis relaxes the assumption made previously that selection against deleterious alleles is stronger than on beneficial alleles. AU - Johnson, Toby AU - Barton, Nicholas H ID - 4260 IS - 1 JF - Genetics SN - 0016-6731 TI - The effect of deleterious alleles on adaptation in asexual populations VL - 162 ER - TY - JOUR AB - Bayesian inference is becoming a common statistical approach to phylogenetic estimation because, among other reasons, it allows for rapid analysis of large data sets with complex evolutionary models. Conveniently, Bayesian phylogenetic methods use currently available stochastic models of sequence evolution. However, as with other model-based approaches, the results of Bayesian inference are conditional on the assumed model of evolution: inadequate models (models that poorly fit the data) may result in erroneous inferences. In this article, I present a Bayesian phylogenetic method that evaluates the adequacy of evolutionary models using posterior predictive distributions. By evaluating a model's posterior predictive performance, an adequate model can be selected for a Bayesian phylogenetic study. Although I present a single test statistic that assesses the overall (global) performance of a phylogenetic model, a variety of test statistics can be tailored to evaluate specific features (local performance) of evolutionary models to identify sources failure. The method presented here, unlike the likelihood-ratio test and parametric bootstrap, accounts for uncertainty in the phylogeny and model parameters. AU - Bollback, Jonathan P ID - 4349 IS - 7 JF - Molecular Biology and Evolution SN - 0737-4038 TI - Bayesian model adequacy and choice in phylogenetics VL - 19 ER - TY - JOUR AB - We introduce a general recursion for the probability of identity in state of two individuals sampled from a population subject to mutation, migration, and random drift in a two-dimensional continuum. The recursion allows for the interactions induced by density-dependent regulation of the population, which are inevitable in a continuous population. We give explicit series expansions for large neighbourhood size and for low mutation rates respectively and investigate the accuracy of the classical Malécot formula for these general models. When neighbourhood size is small, this formula does not give the identity even over large scales. However, for large neighbourhood size, it is an accurate approximation which summarises the local population structure in terms of three quantities: the effective dispersal rate, σe; the effective population density, ρe; and a local scale, κ, at which local interactions become significant. The results are illustrated by simulations. AU - Barton, Nicholas H AU - Depaulis, Frantz AU - Etheridge, Alison ID - 4263 IS - 1 JF - Theoretical Population Biology SN - 0040-5809 TI - Neutral evolution in spatially continuous populations VL - 61 ER - TY - JOUR AB - Until recently, it was impracticable to identify the genes that are responsible for variation in continuous traits, or to directly observe the effects of their different alleles. Now, the abundance of genetic markers has made it possible to identify quantitative trait loci (QTL) — the regions of a chromosome or, ideally, individual sequence variants that are responsible for trait variation. What kind of QTL do we expect to find and what can our observations of QTL tell us about how organisms evolve? The key to understanding the evolutionary significance of QTL is to understand the nature of inherited variation, not in the immediate mechanistic sense of how genes influence phenotype, but, rather, to know what evolutionary forces maintain genetic variability. AU - Barton, Nicholas H AU - Keightley, Peter ID - 4261 JF - Nature Reviews Genetics SN - 1471-0056 TI - Understanding quantitative genetic variation VL - 3 ER - TY - JOUR AB - Phylogenetic trees can be rooted by a number of criteria. Here, we introduce a Bayesian method for inferring the root of a phylogenetic tree by using one of several criteria: the outgroup, molecular clock, and nonreversible model of DNA substitution. We perform simulation analyses to examine the relative ability of these three criteria to correctly identify the root of the tree. The outgroup and molecular clock criteria were best able to identify the root of the tree, whereas the nonreversible model was able to identify the root only when the substitution process was highly nonreversible. We also examined the performance of the criteria for a tree of four species for which the topology and root position are well supported. Results of the analyses of these data are consistent with the simulation results. AU - Huelsenbeck, John AU - Bollback, Jonathan P AU - Levine, Amy ID - 4347 IS - 1 JF - Systematic Biology SN - 0039-7989 TI - Inferring the root of a phylogenetic tree VL - 51 ER - TY - JOUR AB - This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating MetricIntervalTL formulae into EventClockTL formulae, the two logics being equally expressive. Our proof is structured to yield axiomatizations also for interesting fragments of these logics, such as the linear temporal logic of the real numbers (TLR). AU - Raskin, Jean AU - Schobbens, Pierre AU - Henzinger, Thomas A ID - 4407 IS - 1-2 JF - Theoretical Computer Science SN - 0304-3975 TI - Axioms for real-time logics VL - 274 ER - TY - JOUR AB - We studied the effect of multilocus balancing selection on neutral nucleotide variability at linked sites by simulating a model where diallelic polymorphisms are maintained at an arbitrary number of selected loci by means of symmetric overdominance. Different combinations of alleles define different genetic backgrounds that subdivide the population and strongly affect variability. Several multilocus fitness regimes with different degrees of epistasis and gametic disequilibrium are allowed. Analytical results based on a multilocus extension of the structured coalescent predict that the expected linked neutral diversity increases exponentially with the number of selected loci and can become extremely large. Our simulation results show that although variability increases with the number of genetic backgrounds that are maintained in the population, it is reduced by random fluctuations in the frequencies of those backgrounds and does not reach high levels even in very large populations. We also show that previous results on balancing selection in single-locus systems do not extend to the multilocus scenario in a straightforward way. Different patterns of linkage disequilibrium and of the frequency spectrum of neutral mutations are expected under different degrees of epistasis. Interestingly, the power to detect balancing selection using deviations from a neutral distribution of allele frequencies seems to be diminished under the fitness regime that leads to the largest increase of variability over the neutral case. This and other results are discussed in the light of data from the Mhc. AU - Navarro, Arcadio AU - Barton, Nicholas H ID - 4258 IS - 2 JF - Genetics SN - 0016-6731 TI - The effects of multilocus balancing selection on neutral variability VL - 161 ER - TY - JOUR AB - We extend current multilocus models to describe the effects of migration, recombination, selection, and nonrandom mating on sets of genes in diploids with varied modes of inheritance, allowing us to consider the patterns of nuclear and cytonuclear associations (disequilibria) under various models of migration. We show the relationship between the multilocus notation recently presented by Kirkpatrick, Johnson, and Barton (developed from previous work by Barton and Turelli) and the cytonuclear parameterization of Asmussen, Arnold, and Avise and extend this notation to describe associations between cytoplasmic elements and multiple nuclear genes. Under models with sexual symmetry, both nuclear-nuclear and cytonuclear disequilibria are equivalent. They differ, however, in cases involving some type of sexual asymmetry, which is then reflected in the asymmetric inheritance of cytoplasmic markers. An example given is the case of different migration rates in males and females; simulations using 2, 3, 4, or 5 unlinked autosomal markers with a maternally inherited cytoplasmic marker illustrate how nuclear-nuclear and cytonuclear associations can be used to separately estimate female and male migration rates. The general framework developed here allows us to investigate conditions where associations between loci with different modes of inheritance are not equivalent and to use this nonequivalence to test for deviations from simple models of admixture. AU - Orive, Maria AU - Barton, Nicholas H ID - 4259 IS - 3 JF - Genetics SN - 0016-6731 TI - Associations between cytoplasmic and nuclear loci in hybridizing populations VL - 162 ER - TY - JOUR AB - We have identified widerborst (wdb), a B' regulatory subunit of PP2A, as a conserved component of planar cell polarization mechanisms in both Drosophila and in zebrafish. In Drosophila, wdb acts at two steps during planar polarization of wing epithelial cells. It is required to organize tissue polarity proteins into proximal and distal cortical domains, thus determining wing hair orientation. It is also needed to generate the polarized membrane outgrowth that becomes the wing hair. Widerborst activates the catalytic subunit of PP2A and localizes to the distal side of a planar microtubule web that lies at the level of apical cell junctions. This suggests that polarized PP2A activation along the planar microtubule web is important for planar polarization. In zebrafish, two wdb homologs are required for convergent extension during gastrulation, supporting the conjecture that Drosophila planar cell polarization and vertebrate gastrulation movements are regulated by similar mechanisms. AU - Hannus, Michael AU - Feiguin, Fabian AU - Heisenberg, Carl-Philipp J AU - Eaton, Suzanne ID - 4209 IS - 14 JF - Development SN - 0950-1991 TI - Planar cell polarization requires Widerborst, a B′ regulatory subunit of protein phosphatase 2A VL - 129 ER - TY - JOUR AB - Vertebrate homologues of the Strabismus/van Gogh (stbm/vang) gene have been implicated in patterning and morphogenesis during gastrulation. Recent work shows that stbm/vang is mutated in zebrafish trilobite mutants and that stbm/vang is required for morphogenesis but not patterning during zebrafish gastrulation. AU - Heisenberg, Carl-Philipp J ID - 4207 IS - 19 JF - Current Biology SN - 0960-9822 TI - Wnt signalling: Refocusing on Strabismus VL - 12 ER - TY - JOUR AB - 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. AU - Houart, Corinne AU - Caneparo, Luca AU - Heisenberg, Carl-Philipp J AU - Barth, K Anukampa AU - Take Uchi, Masaya AU - Wilson, Stephen ID - 4194 IS - 2 JF - Neuron SN - 0896-6273 TI - Establishment of the telencephalon during gastrulation by local antagonism of Wnt signaling VL - 35 ER - TY - JOUR AB - 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. AU - Tada, Masazumi AU - Concha, Miguel AU - Heisenberg, Carl-Philipp J ID - 4148 IS - 3 JF - Seminars in Cell & Developmental Biology SN - 1084-9521 TI - Non-canonical Wnt signalling and regulation of gastrulation movements VL - 13 ER - TY - JOUR AB - 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. AU - Heisenberg, Carl-Philipp J AU - Tada, Masazumi ID - 4196 IS - 6 JF - Seminars in Cell & Developmental Biology SN - 1084-9521 TI - Zebrafish gastrulation movements: bridging cell and developmental biology VL - 13 ER - TY - JOUR AB - Recent studies on vertebrate homologues of the van gogh/strabismus (vang/stbm) gene, a key player in planar cell polarity signalling in Drosophila, show that vang/stbm is involved in patterning and morphogenesis during vertebrate gastrulation where it modulates two distinct Wnt signals. AU - Heisenberg, Carl-Philipp J AU - Tada, Masazumi ID - 4199 IS - 4 JF - Current Biology SN - 0960-9822 TI - Wnt signalling: A moving picture emerges from van gogh VL - 12 ER - TY - JOUR AB - 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. AU - Polechova, Jitka AU - Stopka, P. ID - 4139 IS - 8 JF - Canadian Journal of Zoology SN - 0008-4301 TI - Geometry of social relationships in the Old World wood mouse, Apodemus sylvaticus VL - 80 ER - TY - CONF AB - 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. AU - Agarwal, Pankaj AU - Edelsbrunner, Herbert AU - Wang, Yusu ID - 4003 SN - 9780898715132 T2 - Proceedings of the 13th annual ACM-SIAM symposium on Discrete algorithms TI - Computing the writhing number of a polygonal knot ER - TY - JOUR AB - This article is a survey of research areas in which motion plays a pivotal role. The aim of the article is to review current approaches to modeling motion together with related data structures and algorithms, and to summarize the challenges that lie ahead in producing a more unified theory of motion representation that would be useful across several disciplines. AU - Agarwal, Pankaj AU - Guibas, Leonidas AU - Edelsbrunner, Herbert AU - Erickson, Jeff AU - Isard, Michael AU - Har Peled, Sariel AU - Hershberger, John AU - Jensen, Christian AU - Kavraki, Lydia AU - Koehl, Patrice AU - Lin, Ming AU - Manocha, Dinesh AU - Metaxas, Dimitris AU - Mirtich, Brian AU - Mount, David AU - Muthukrishnan, Sankara AU - Pai, Dinesh AU - Sacks, Elisha AU - Snoeyink, Jack AU - Suri, Subhash AU - Wolefson, Ouri ID - 3995 IS - 4 JF - ACM Computing Surveys SN - 0360-0300 TI - Algorithmic issues in modeling motion VL - 34 ER - TY - JOUR AB - We present fast implementations of a hybrid algorithm for reporting box and cube intersections. Our algorithm initially takes a divide-and-conquer approach and switches to simpler algorithms for low numbers of boxes. We use our implementations as engines to solve problems about geometric primitives. We look at two such problems in the category of quality analysis of surface triangulations. AU - Zomorodian, Afra AU - Edelsbrunner, Herbert ID - 4000 IS - 1-2 JF - International Journal of Computational Geometry and Applications SN - 0218-1959 TI - Fast software for box intersections VL - 12 ER - TY - JOUR AB - We present results on a two-step improvement of mesh quality in three-dimensional Delaunay triangulations. The first step refines the triangulation by inserting sinks and eliminates tetrahedra with large circumradius over shortest edge length ratio. The second step assigns weights to the vertices to eliminate slivers. Our experimental findings provide evidence for the practical effectiveness of sliver exudation. AU - Edelsbrunner, Herbert AU - Guoy, Damrong ID - 3998 IS - 3 JF - Engineering with Computers SN - 0177-0667 TI - An experimental study of sliver exudation VL - 18 ER - TY - JOUR AB - The presynaptic Ca2+ signal is a key determinant of transmitter release at chemical synapses. In cortical synaptic terminals, however, little is known about the kinetic properties of the presynaptic Ca2+ channels. To investigate the timing and magnitude of the presynaptic Ca2+ inflow, we performed whole-cell patch-clamp recordings from mossy fiber boutons (MFBs) in rat hippocampus. MFBs showed large high-voltage-activated Ca(2+) currents, with a maximal amplitude of approximately 100 pA at a membrane potential of 0 mV. Both activation and deactivation were fast, with time constants in the submillisecond range at a temperature of approximately 23 degrees C. An MFB action potential (AP) applied as a voltage-clamp command evoked a transient Ca2+ current with an average amplitude of approximately 170 pA and a half-duration of 580 microsec. A prepulse to +40 mV had only minimal effects on the AP-evoked Ca2+ current, indicating that presynaptic APs open the voltage-gated Ca2+ channels very effectively. On the basis of the experimental data, we developed a kinetic model with four closed states and one open state, linked by voltage-dependent rate constants. Simulations of the Ca2+ current could reproduce the experimental data, including the large amplitude and rapid time course of the current evoked by MFB APs. Furthermore, the simulations indicate that the shape of the presynaptic AP and the gating kinetics of the Ca2+ channels are tuned to produce a maximal Ca2+ influx during a minimal period of time. The precise timing and high efficacy of Ca2+ channel activation at this cortical glutamatergic synapse may be important for synchronous transmitter release and temporal information processing. AU - Bischofberger, Josef AU - Geiger, Jörg AU - Jonas, Peter M ID - 3802 IS - 24 JF - Journal of Neuroscience SN - 0270-6474 TI - Timing and efficacy of Ca(2+) channel activation in hippocampal mossy fiber boutons VL - 22 ER - TY - JOUR AB - Hamilton's concept of local mate competition (LMC) is the standard model to explain female-biased sex ratios in solitary Hymenoptera. In social Hymenoptera, however, LMC has remained controversial, mainly because manipulation of sex allocation by workers in response to relatedness asymmetries is an additional powerful mechanism of female bias. Furthermore, the predominant mating systems in the social insects are thought to make LMC unlikely. Nevertheless, several species exist in which dispersal of males is limited and mating occurs in the nest. Some of these species, such as the ant Cardiocondyla obscurior, have evolved dimorphic males, with one morph being specialized for dispersal and the other for fighting with nest-mate males over access to females. Such life history, combining sociality and alternative reproductive tactics in males, provides a unique opportunity to test the power of LMC as a selective force leading to female-biased sex ratios in social Hymenoptera. We show that, in concordance with LMC predictions, an experimental increase in queen number leads to a shift in sex allocation in favour of non-dispersing males, but does not influence the proportion of disperser males. Furthermore, we can assign this change in sex allocation at the colony level to the queens and rule out worker manipulation. AU - Cremer, Sylvia AU - Heinze, Jürgen ID - 3919 IS - 1489 JF - Proceedings of the Royal Society of London Series B Biological Sciences SN - 0962-8452 TI - Adaptive production of fighter males: queens of the ant Cardiocondyla adjust the sex ratio under local mate competition VL - 269 ER - TY - JOUR AB - Males of the ant Cardiocondyla show a dispersal dimorphism of a winged and wingless morph. The loss of flight has lead to morphological reductions in the wingless (ergatoid) males and also affected body size, eye size and pigmentation. As ergatoid males mate exclusively inside the maternal nest, they underlie increased male-male competition and therefore have also evolved additional changes in behaviour and physiology: in contrast to winged males, ergatoid males are highly aggressive towards each other and their spermatogenesis is prolonged compared to all other hymenopteran males. In addition to these two male morphs, we found males with an intermediate appearance. These "intermorphic" males provide a transitional stage between normal males in most investigated morphological and physiological parameters. As they are produced extremely rarely and only in colonies that switch between pure ergatoid to mixed male production, we argue that they likely represent a developmental mistake. Parallels between the determination of male morphs and female castes (queen-worker dimorphism and worker polymorphism) might help to understand how the large potential of phenotypic plasticity in both sexes of social insects is realised during development. AU - Cremer, Sylvia AU - Lautenschläger, Birgit AU - Heinze, Jürgen ID - 3924 IS - 3 JF - Insectes Sociaux SN - 0020-1812 TI - A transitional stage between the ergatoid and winged male morph in the ant Cardiocondyla obscurior VL - 49 ER - TY - JOUR AB - Males of the tropical ant Cardiocondyla obscurior are either wingless and aggressive or winged and docile, and both compete for access to virgin queens in the nest1, 2. Although the fighter males (ergatoids) attack and kill other ergatoids, they tolerate and even attempt to mate with their winged rivals. Here we show that the winged males avoid the aggression of wingless males by mimicking the chemical bouquet of virgin queens, but that their mating success is not reduced as a result. This example of female mimicry by vigorous males is surprising, as in other species it is typically used as a protective strategy by weaker males, and may explain the coexistence and equal mating success of two male morphs. AU - Cremer, Sylvia AU - Sledge, Matthew AU - Heinze, Jürgen ID - 3925 JF - Nature SN - 0028-0836 TI - Chemical mimicry: Male ants disguised by the queen's bouquet VL - 419 ER - TY - JOUR AB - We formalize a notion of topological simplification within the framework of a filtration, which is the history of a growing complex. We classify a topological change that happens during growth as either a feature or noise depending on its lifetime or persistence within the filtration. We give fast algorithms for computing persistence and experimental evidence for their speed and utility. AU - Edelsbrunner, Herbert AU - Letscher, David AU - Zomorodian, Afra ID - 3996 IS - 4 JF - Discrete & Computational Geometry SN - 0179-5376 TI - Topological persistence and simplification VL - 28 ER - TY - JOUR AB - A particular Solid Injector needle, suitable for GC-MS analyses of small specimens, is described together with its application in a study on ants. AU - Turillazzi, Stefano AU - Sledge, Matthew AU - Cremer, Sylvia AU - Heinze, Jürgen ID - 3920 JF - Insect Social Life TI - A method for analysing small-size specimens in GC-MS VL - 4 ER - TY - JOUR AB - Networks of GABAergic interneurons are of critical importance for the generation of gamma frequency oscillations in the brain. To examine the underlying synaptic mechanisms, we made paired recordings from "basket cells" (BCs) in different subfields of hippocampal slices, using transgenic mice that express enhanced green fluorescent protein (EGFP) under the control of the parvalbumin promoter. Unitary inhibitory postsynaptic currents (IPSCs) showed large amplitude and fast time course with mean amplitude-weighted decay time constants of 2.5, 1.2, and 1.8 ms in the dentate gyrus, and the cornu ammonis area 3 (CA3) and 1 (CA1), respectively (33-34 degrees C). The decay of unitary IPSCs at BC-BC synapses was significantly faster than that at BC-principal cell synapses, indicating target cell-specific differences in IPSC kinetics. In addition, electrical coupling was found in a subset of BC-BC pairs. To examine whether an interneuron network with fast inhibitory synapses can act as a gamma frequency oscillator, we developed an interneuron network model based on experimentally determined properties. In comparison to previous interneuron network models, our model was able to generate oscillatory activity with higher coherence over a broad range of frequencies (20-110 Hz). In this model, high coherence and flexibility in frequency control emerge from the combination of synaptic properties, network structure, and electrical coupling. AU - Bartos, Marlene AU - Vida, Imre AU - Frotscher, Michael AU - Meyer, Axel AU - Monyer, Hannah AU - Geiger, Jörg AU - Jonas, Peter M ID - 3800 IS - 20 JF - PNAS SN - 0027-8424 TI - Fast synaptic inhibition promotes synchronized gamma oscillations in hippocampal interneuron networks VL - 99 ER - TY - JOUR AB - Mossy fiber (MF) synapses are key stations for flow of information through the hippocampal formation. A major component of the output of the MF system is directed towards inhibitory interneurons. Recent studies have revealed that the functional properties of MF-interneuron synapses differ substantially from those of MF-CA3 pyramidal neuron synapses. Mossy-fiber-interneuron synapses in the stratum lucidum represent a continuum of functional subtypes, in which the subunit composition of postsynaptic AMPA receptors and NMDA receptors appears to be regulated in a coordinated manner. AU - Bischofberger, Josef AU - Jonas, Peter M ID - 3803 IS - 12 JF - Trends in Neurosciences SN - 0166-2236 TI - TwoB or not twoB: differential transmission at glutamatergic mossy fiber-interneuron synapses in the hippocampus VL - 25 ER - TY - JOUR AB - To examine possible interactions between fast depression and modulation of inhibitory synaptic transmission in the hippocampus, we recorded from pairs of synaptically connected basket cells (BCs) and granule cells (GCs) in the dentate gyrus of rat brain slices at 34 degrees C. Multiple-pulse depression (MPD) was examined in trains of 5 or 10 inhibitory postsynaptic currents (IPSCs) evoked at frequencies of 10-100 Hz under several conditions that inhibit transmitter release: block of voltage-dependent Ca2+ channels by Cd2+ (10 microM), activation of gamma-amino-butyric acid type B receptors (GABA(B)Rs) by baclofen (10 microM) and activation of muscarinic acetylcholine receptors (mAchRs) by carbachol (2 microM). All manipulations led to a substantial inhibition of synaptic transmission, reducing the amplitude of the first IPSC in the train (IPSC1) by 72%, 61% and 29%, respectively. However, MPD was largely preserved under these conditions (0.34 in control versus 0.31, 0.50 and 0.47 in the respective conditions at 50 Hz). Similarly, a theta burst stimulation (TBS) protocol reduced IPSC1 by 54%, but left MPD unchanged (0.40 in control and 0.39 during TBS). Analysis of both fractions of transmission failures and coefficients of variation (CV) of IPSC peak amplitudes suggested that MPD had a presynaptic expression site, independent of release probability. In conclusion, different types of presynaptic modulation of inhibitory synaptic transmission converge on a reduction of synaptic strength, while short-term dynamics are largely unchanged. AU - Hefft, Stefan AU - Kraushaar, Udo AU - Geiger, Jörg AU - Jonas, Peter M ID - 3801 IS - Pt 1 JF - Journal of Physiology SN - 0022-3751 TI - Presynaptic short-term depression is maintained during regulation of transmitter release at a GABAergic synapse in rat hippocampus VL - 539 ER - TY - JOUR AB - GABAergic interneurones are diverse in their morphological and functional properties. Perisomatic inhibitory cells show fast spiking during sustained current injection, whereas dendritic inhibitory cells fire action potentials with lower frequency. We examined functional and molecular properties of K(+) channels in interneurones with horizontal dendrites in stratum oriens-alveus (OA) of the hippocampal CA1 region, which mainly comprise somatostatin-positive dendritic inhibitory cells. Voltage-gated K(+) currents in nucleated patches isolated from OA interneurones consisted of three major components: a fast delayed rectifier K(+) current component that was highly sensitive to external 4-aminopyridine (4-AP) and tetraethylammonium (TEA) (half-maximal inhibitory concentrations < 0.1 mM for both blockers), a slow delayed rectifier K(+) current component that was sensitive to high concentrations of TEA, but insensitive to 4-AP, and a rapidly inactivating A-type K(+) current component that was blocked by high concentrations of 4-AP, but resistant to TEA. The relative contributions of these components to the macroscopic K(+) current were estimated as 57 +/- 5, 25 +/- 6, and 19 +/- 2 %, respectively. Dendrotoxin, a selective blocker of Kv1 channels had only minimal effects on K(+) currents in nucleated patches. Coapplication of the membrane-permeant cAMP analogue 8-(4-chlorophenylthio)-adenosine 3':5'-cyclic monophosphate (cpt-cAMP) and the phosphodiesterase blocker isobutyl-methylxanthine (IBMX) resulted in a selective inhibition of the fast delayed rectifier K(+) current component. This inhibition was absent in the presence of the protein kinase A (PKA) inhibitor H-89, implying the involvement of PKA-mediated phosphorylation. Single-cell reverse transcription-polymerase chain reaction (RT-PCR) analysis revealed a high abundance of Kv3.2 mRNA in OA interneurones, whereas the expression level of Kv3.1 mRNA was markedly lower. Similarly, RT-PCR analysis showed a high abundance of Kv4.3 mRNA, whereas Kv4.2 mRNA was undetectable. This suggests that the fast delayed rectifier K(+) current and the A-type K(+) current component are mediated predominantly by homomeric Kv3.2 and Kv4.3 channels. Selective modulation of Kv3.2 channels in OA interneurones by cAMP is likely to be an important factor regulating the activity of dendritic inhibitory cells in principal neurone-interneurone microcircuits. AU - Lien, Cheng AU - Martina, Marco AU - Schultz, Jobst AU - Ehmke, Heimo AU - Jonas, Peter M ID - 3799 IS - Pt 2 JF - Journal of Physiology SN - 0022-3751 TI - Gating, modulation and subunit composition of voltage-gated K(+) channels in dendritic inhibitory interneurones of rat hippocampus VL - 538 ER - TY - JOUR AB - In 1991, Barton and Turelli developed recursions to describe the evolution of multilocus systems under arbitrary forms of selection. This article generalizes their approach to allow for arbitrary modes of inheritance, including diploidy, polyploidy, sex linkage, cytoplasmic inheritance, and genomic imprinting. The framework is also extended to allow for other deterministic evolutionary forces, including migration and mutation. Exact recursions that fully describe the state of the population are presented; these are implemented in a computer algebra package (available on the Web at http://helios.bto.ed.ac.uk/evolgen). Despite the generality of our framework, it can describe evolutionary dynamics exactly by just two equations. These recursions can be further simplified using a "quasi-linkage equilibrium" (QLE) approximation. We illustrate the methods by finding the effect of natural selection, sexual selection, mutation, and migration on the genetic composition of a population. AU - Kirkpatrick, Mark AU - Johnson, Toby AU - Barton, Nicholas H ID - 3621 IS - 4 JF - Genetics SN - 0016-6731 TI - General models of multilocus evolution VL - 161 ER - TY - JOUR AB - A central problem in biology is determining how genes interact as parts of functional networks. Creation and analysis of synthetic networks, composed of well-characterized genetic elements, provide a framework for theoretical modeling. Here, with the use of a combinatorial method, a library of networks with varying connectivity was generated in Escherichia coli. These networks were composed of genes encoding the transcriptional regulators Lacl, TetR, and lambda Cl, as well as the corresponding promoters. They displayed phenotypic behaviors resembling binary logical circuits, with two chemical “inputs” and a fluorescent protein “output.” Within this simple system, diverse computational functions arose through changes in network connectivity. Combinatorial synthesis provides an alternative approach for studying biological networks, as well as an efficient method for producing diverse phenotypes in vivo. AU - Guet, Calin C AU - Elowitz, Michael AU - Hsing, Weihong AU - Leibler, Stanislas ID - 3757 IS - 5572 JF - Science SN - 0036-8075 TI - Combinatorial synthesis of genetic networks VL - 296 ER - TY - JOUR AB - The use of advanced patch-clamp recording techniques in brain slices, such as simultaneous recording from multiple neurons and recording from dendrites or presynaptic terminals, demands slices of the highest quality. In this context the mechanics of the tissue slicer are an important factor. Ideally, a tissue slicer should generate large-amplitude and high-frequency movements of the cutting blade in a horizontal axis, with minimal vibrations in the vertical axis. We developed a vibroslicer that fulfils these in part conflicting requirements. The oscillator is a permanent-magnet-coil-leaf-spring system. Using an auto-resonant mechano-electrical feedback circuit, large horizontal oscillations (up to 3 mm peak-to-peak) with high frequency (,90 Hz) are generated. To minimize vertical vibrations, an adjustment mechanism was employed that allowed alignment of the cutting edge of the blade with the major axis of the oscillation. A vibroprobe device was used to monitor vertical vibrations during adjustment. The system is based on the shading of the light path between a light-emitting diode (LED) and a photodiode. Vibroprobe monitoring revealed that the vibroslicer, after appropriate adjustment, generated vertical vibrations of <1 µm, significantly less than many commercial tissue slicers. Light- and electron-microscopic analysis of surface layers of slices cut with the vibroslicer showed that cellular elements, dendritic processes and presynaptic terminals are well preserved under these conditions, as required for patch-clamp recording from these structures. AU - Geiger, Jörg AU - Bischofberger, Joseph AU - Vida, Imre AU - Fröbe, Ulrich AU - Pfitzinger, S AU - Weber, H. AU - Haverkampf, Klaus AU - Jonas, Peter M ID - 3497 IS - 3 JF - Pflugers Archiv : European Journal of Physiology SN - 0031-6768 TI - Patch-clamp recording in brain slices with improved slicer technology VL - 443 ER - TY - JOUR AB - Information in neuronal networks is thought to be represented by the rate of discharge and the temporal relationship between the discharging neurons. The discharge frequency of neurons is affected by their afferents and intrinsic properties, and shows great individual variability. The temporal coordination of neurons is greatly facilitated by network oscillations. In the hippocampus, population synchrony fluctuates during theta and gamma oscillations (10-100 ms scale) and can increase almost 10-fold during sharp wave bursts. Despite these large changes in excitability in the sub-second scale, longer-term (minute-scale) firing rates of individual neurons are relatively constant in an unchanging environment. As a result, mean hippocampal output remains stable over time. To understand the mechanisms responsible for this homeostasis, we address the following issues: (i) Can firing rates of single cells be modified? (ii) Once modified, what mechanism(s) can maintain the changes? We show that firing rates of hippocampal pyramidal cells can be altered in a novel environment and by Hebbian pairing of physiological input patterns with postsynaptic burst discharge. We also illustrate a competition between single spikes and the occurrence of spike bursts. Since spike-inducing (suprathreshold) inputs decrease the ability of strong ('teaching') inputs to induce a burst discharge, we propose that the single spike versus burst competition presents a homeostatic regulatory mechanism to maintain synaptic strength and, consequently, firing rate in pyramidal cells. AU - Buzsáki, György AU - Csicsvari, Jozsef L AU - Dragoi, George AU - Harris, Kenneth AU - Henze, D. AU - Hirase, Hajima ID - 3533 IS - 9 JF - Cerebral Cortex SN - 1047-3211 TI - Homeostatic maintenance of neuronal excitability by burst discharges in vivo VL - 12 ER - TY - CONF AB - We give a brief overview of the current understanding of the explosion mechanism of core collapse supernovae. Our main focus is the impact of rotation on the explosion. Recent observations of the polarization of the light emitted by supernova explosions indicate that there are large deviations from spherical symmetry in the very heart of the explosion the origin of which is unknown. We use the new approach of a three dimensional test particle based simulation to simulate the infall phase of a supernova event. The underlying microphysics is simplified to make this computationally possible. A systematic study of the influence of rotation mainly during the infall phase of the collapse of a typical iron core is performed. Indications for significant deviations from spherical symmetry are found in our very rapidly rotating models. © 2002 American Institute of Physics AU - Bollenbach, Mark Tobias AU - Bauer, Wolfgang ID - 3424 SN - 9781510832008 TI - 3d supernovae collapse calculations VL - 644 ER - TY - JOUR AB - Coordination of cell and tissue polarity commonly involves directional signaling [1]. In the Arabidopsis root epidermis, cell polarity is revealed by basal, root tip-oriented, hair outgrowth from hair-forming cells (trichoblasts) [2]. The plant hormone auxin displays polar movements [1, 3] and accumulates at maximum concentration in the root tip [4, 5]. The application of polar auxin transport inhibitors [3] evokes changes in trichoblast polarity only at high concentrations and after long-term application [2, 4]. Thus, it remains open whether components of the auxin transport machinery mediate establishment of trichoblast polarity. Here we report that the presumptive auxin influx carrier AUX1 [6, 7] contributes to apical-basal hair cell polarity. AUX1 function is required for polarity changes induced by exogenous application of the auxin 2,4-D, a preferential influx carrier substrate. Similar to aux1 mutants, the vesicle trafficking inhibitor brefeldin A (BFA) interferes with polar hair initiation, and AUX1 function is required for BFA-mediated polarity changes. Consistently, BFA inhibits membrane trafficking of AUX1, trichoblast hyperpolarization induced by 2,4-D, and alters the distal auxin maximum. Our results identify AUX1 as one component of a novel BFA-sensitive auxin transport pathway polarizing cells toward a hormone maximum. AU - Grebe, Markus AU - Friml, Jirí AU - Swarup, Ranjan AU - Ljung, Karin AU - Sandberg, Göran AU - Terlou, Maarten AU - Palme, Klaus AU - Bennett, Malcolm AU - Scheres, Ben ID - 2988 IS - 4 JF - Current Biology SN - 0960-9822 TI - Cell polarity signaling in Arabidopsis involves a BFA sensitive auxin influx pathway VL - 12 ER - TY - JOUR AB - Single molecule experiments provide insight into the individuality of biological macromolecules, their unique function, reaction pathways, trajectories and molecular interactions. The exceptional signal-to-noise ratio of the atomic force microscope allows individual proteins to be imaged under physiologically relevant conditions at a lateral resolution of 0.5–1 nm and a vertical resolution of 0.1–0.2 nm. Recently, it has become possible to observe single molecule events using this technique. This capability is reviewed on various water-soluble and membrane proteins. Examples of the observation of function, variability, and assembly of single proteins are discussed. Statistical analysis is important to extend conclusions derived from single molecule experiments to protein species. Such approaches allow the classification of protein conformations and movements. Recent developments of probe microscopy techniques allow simultaneous measurement of multiple signals on individual macromolecules, and greatly extend the range of experiments possible for probing biological systems at the molecular level. Biologists exploring molecular mechanisms will benefit from a burgeoning of scanning probe microscopes and of their future combination with molecular biological experiments. AU - Mueller, Daniel AU - Janovjak, Harald L AU - Lehto, Tiina AU - Kuerschner, Lars AU - Anderson, Kurt ID - 3421 IS - 1-3 JF - Progress in Biophysics and Molecular Biology SN - 0079-6107 TI - Observing structure, function and assembly of single proteins by AFM VL - 79 ER - TY - JOUR AB - In contrast to animals, little is known about pattern formation in plants. Physiological and genetic data suggest the involvement of the phytohormone auxin in this process. Here, we characterize a novel member of the PIN family of putative auxin efflux carriers, Arabidopsis PIN4, that is localized in developing and mature root meristems. Atpin4 mutants are defective in establishment and maintenance of endogenous auxin gradients, fail to canalize externally applied auxin, and display various patterning defects in both embryonic and seedling roots. We propose a role for AtPIN4 in generating a sink for auxin below the quiescent center of the root meristem that is essential for auxin distribution and patterning. AU - Friml, Jirí AU - Benková, Eva AU - Blilou, Ikram AU - Wiśniewska, Justyna AU - Hamann, Thorsten AU - Ljung, Karin AU - Woody, Scott AU - Sandberg, Göran AU - Scheres, Ben AU - Jürgens, Gerd AU - Palme, Klaus ID - 2989 IS - 5 JF - Cell SN - 0092-8674 TI - AtPIN4 mediates sink-driven auxin gradients and root patterning in Arabidopsis VL - 108 ER - TY - JOUR AB - Quantitative real-time PCR represents a highly sensitive and powerful technique for the quantitation of nucleic acids. It has a tremendous potential for the high-throughput analysis of gene expression in research and routine diagnostics. However, the major hurdle is not the practical performance of the experiments themselves but rather the efficient evaluation and the mathematical and statistical analysis of the enormous amount of data gained by this technology, as these functions are not included in the software provided by the manufacturers of the detection systems. In this work, we focus on the mathematical evaluation and analysis of the data generated by quantitative real-time PCR, the calculation of the final results, the propagation of experimental variation of the measured values to the final results, and the statistical analysis. We developed a Microsoft Excel-based software application coded in Visual Basic for Applications, called Q-Gene, which addresses these points. Q-Gene manages and expedites the planning, performance, and evaluation of quantitative real-time PCR experiments, as well as the mathematical and statistical analysis, storage, and graphical presentation of the data. The Q-Gene software application is a tool to cope with complex quantitative real-time PCR experiments at a high-throughput scale and considerably expedites and rationalizes the experimental setup, data analysis, and data management while ensuring highest reproducibility. AU - Müller, Patrick AU - Janovjak, Harald L AU - Miserez, Andre AU - Dobbie, Zuzana ID - 3422 IS - 6 JF - Biotechniques SN - 0736-6205 TI - Processing of gene expression data generated by quantitative real-time RT-PCR VL - 32 ER - TY - JOUR AB - The maturation of synaptic structures depends on inductive interactions between axons and their prospective targets. One example of such an interaction is the influence of proprioceptive sensory axons on the differentiation of muscle spindles. We have monitored the expression of three transcription factors, Egr3, Pea3, and Erm, that delineate early muscle spindle development in an assay of muscle spindle-inducing signals. We provide genetic evidence that Neuregulin1 (Nrg1) is required for proprioceptive afferent-evoked induction of muscle spindle differentiation in the mouse. Ig-Nrg1 isoforms are preferentially expressed by proprioceptive sensory neurons and are sufficient to induce muscle spindle differentiation in vivo, whereas CRD-Nrg1 isoforms are broadly expressed in sensory and motor neurons but are not required for muscle spindle induction. AU - Hippenmeyer, Simon AU - Shneider, Neil AU - Birchmeier, Carmen AU - Burden, Steven AU - Jessell, Thomas AU - Arber, Silvia ID - 3140 IS - 6 JF - Neuron SN - 0896-6273 TI - A role for Neuregulin1 signaling in muscle spindle differentiation VL - 36 ER - TY - CONF AU - Bauer, Wolfgang AU - Bollenbach, Mark Tobias AU - Kleine Berkenbusch, Marko AU - Harreis, Holger ID - 3423 T2 - Proceedings of the 18th Winter Workshop on Nuclear Dynamics TI - The percolation interpretation of the nuclear fragmentation phase transition ER - TY - JOUR AB - Long-standing models propose that plant growth responses to light or gravity are mediated by asymmetric distribution of the phytohormone auxin. Physiological studies implicated a specific transport system that relocates auxin laterally, thereby effecting differential growth; however, neither the molecular components of this system nor the cellular mechanism of auxin redistribution on light or gravity perception have been identified. Here, we show that auxin accumulates asymmetrically during differential growth in an efflux-dependent manner. Mutations in the Arabidopsis gene PIN3, a regulator of auxin efflux, alter differential growth. PIN3 is expressed in gravity-sensing tissues, with PIN3 protein accumulating predominantly at the lateral cell surface. PIN3 localizes to the plasma membrane and to vesicles that cycle in an actin-dependent manner. In the root columella, PIN3 is positioned symmetrically at the plasma membrane but rapidly relocalizes laterally on gravity stimulation. Our data indicate that PIN3 is a component of the lateral auxin transport system regulating tropic growth. In addition, actin-dependent relocalization of PIN3 in response to gravity provides a mechanism for redirecting auxin flux to trigger asymmetric growth. AU - Friml, Jirí AU - Wiśniewska, Justyna AU - Benková, Eva AU - Mendgen, Kurt AU - Palme, Klaus ID - 2986 IS - 6873 JF - Nature SN - 0028-0836 TI - Lateral relocation of auxin efflux regulator PIN3 mediates tropism in Arabidopsis VL - 415 ER - TY - JOUR AB - The hydra mutants of Arabidopsis are characterized by a pleiotropic phenotype that shows defective embryonic and seedling cell patterning, morphogenesis, and root growth. We demonstrate that the HYDRA1 gene encodes a Δ8-Δ7 sterol isomerase, whereas HYDRA2 encodes a sterol C14 reductase, previously identified as the FACKEL gene product. Seedlings mutant for each gene are similarly defective in the concentrations of the three major Arabidopsis sterols. Promoter::reporter gene analysis showed misexpression of the auxin-regulated DR5 and ACS1 promoters and of the epidermal cell file-specific GL2 promoter in the mutants. The mutants exhibit enhanced responses to auxin. The phenotypes can be rescued partially by inhibition of auxin and ethylene signaling but not by exogenous sterols or brassinosteroids. We propose a model in which correct sterol profiles are required for regulated auxin and ethylene signaling through effects on membrane function. AU - Souter, Martin AU - Topping, Jennifer AU - Pullen, Margaret AU - Friml, Jirí AU - Palme, Klaus AU - Hackett, Rachel AU - Grierson, Don AU - Lindsey, Keith ID - 2987 IS - 5 JF - Plant Cell SN - 1040-4651 TI - Hydra mutants of Arabidopsis are defective in sterol profiles and auxin and ethylene signaling VL - 14 ER - TY - JOUR AB - Developmental responses to the plant hormone auxin are thought to be mediated by interacting pairs from two protein families: short-lived inhibitory IAA proteins and ARF transcription factors binding to auxin-response elements. Monopteros mutants lacking activating ARF5 and the auxin-insensitive mutant bodenlos fail to initiate the root meristem during early embryogenesis. Here we show that the bodenlos phenotype results from an amino-acid exchange in the conserved degradation domain of IAA12. BODENLOS and MONOPTEROS interact in the yeast two-hybrid assay and the two genes are coexpressed in early embryogenesis, suggesting that BODENLOS inhibits MONOPTEROS action in root meristem initiation. AU - Hamann, Thorsten AU - Benková, Eva AU - Bäurle, Isabel AU - Kientz, Marika AU - Jürgens, Gerd ID - 2866 IS - 13 JF - Genes and Development SN - 0890-9369 TI - The Arabidopsis BODENLOS gene encodes an auxin response protein inhibiting MONOPTEROS-mediated embryo patterning VL - 16 ER - TY - CONF AB - In the last few years, several new algorithms based on graph cuts have been developed to solve energy minimization problems in computer vision. Each of these techniques constructs a graph such that the minimum cut on the graph also minimizes the energy. Yet because these graph constructions are complex and highly specific to a particular energy function, graph cuts have seen limited application to date. In this paper we characterize the energy functions that can be minimized by graph cuts. Our results are restricted to energy functions with binary variables. However, our work generalizes many previous constructions, and is easily applicable to vision problems that involve large numbers of labels, such as stereo, motion, image restoration and scene reconstruction. We present three main results: a necessary condition for any energy function that can be minimized by graph cuts; a sufficient condition for energy functions that can be written as a sum of functions of up to three variables at a time; and a general-purpose construction to minimize such an energy function. Researchers who are considering the use of graph cuts to optimize a particular energy function can use our results to determine if this is possible, and then follow our construction to create the appropriate graph. AU - Kolmogorov, Vladimir AU - Zabih, Ramin ID - 2927 SN - 9783540437468 T2 - Proceedings of the 7th European Conference on Computer Vision TI - Multi-camera scene reconstruction via graph cuts ER - TY - JOUR AB - We define the two dimensional Pauli operator and identify its core for magnetic fields that are regular Borel measures. The magnetic field is generated by a scalar potential hence we bypass the usual A L 2loc condition on the vector potential, which does not allow to consider such singular fields. We extend the Aharonov-Casher theorem for magnetic fields that are measures with finite total variation and we present a counterexample in case of infinite total variation. One of the key technical tools is a weighted L 2 estimate on a singular integral operator. AU - Erdös, László AU - Vougalter, Vitali ID - 2739 IS - 2 JF - Communications in Mathematical Physics SN - 0010-3616 TI - Pauli operator and Aharonov–Casher theorem¶ for measure valued magnetic fields VL - 225 ER - TY - JOUR AB - We consider the long time evolution of a quantum particle weakly interacting with a phonon field. We show that in the weak coupling limit the Wigner distribution of the electron density matrix converges to the solution of the linear Boltzmann equation globally in time. The collision kernel is identified as the sum of an emission and an absorption term that depend on the equilibrium distribution of the free phonon modes. AU - Erdös, László ID - 2738 IS - 5-6 JF - Journal of Statistical Physics SN - 0022-4715 TI - Linear Boltzmann equation as the long time dynamics of an electron weakly coupled to a phonon field VL - 107 ER - TY - JOUR AB - We show that the lowest eigenvalue of the magnetic Schrödinger operator on a line bundle over a compact Riemann surface M is bounded by the L1-norm of the magnetic field B. This implies a similar bound on the multiplicity of the ground state. An example shows that this degeneracy can indeed be comparable with ∫M |B| even in case of the trivial bundle. AU - Erdös, László ID - 2740 IS - 6 JF - Annales de l'Institut Fourier SN - 0373-0956 TI - Spectral shift and multiplicity of the first eigenvalue of the magnetic Schrödinger operator in two dimensions VL - 52 ER - TY - JOUR AB - We derive the time-dependent Schrödinger–Poisson equation as the weak coupling limit of the N-body linear Schrödinger equation with Coulomb potential. AU - Bardos, Claude AU - Erdös, László AU - Golse, François AU - Mauser, Norbert AU - Yau, Horng ID - 2737 IS - 6 JF - Comptes Rendus Mathematique SN - 1631-073X TI - Derivation of the Schrödinger-Poisson equation from the quantum N-body problem VL - 334 ER - TY - JOUR AB - Metabotropic γ-aminobutyric acid receptors (GABABRs) are involved in modulation of synaptic transmission and activity of cerebellar and thalamic neurons. We used subtype-specific antibodies in pre- and postembedding immunohistochemistry combined with three-dimensional reconstruction of labelled profiles and quantification of immunoparticles to reveal the subcellular distribution of pre- and postsynaptic GABABR1a/b and GABABR2 in the rat cerebellum and ventrobasal thalamus. GABABR1a/b and R2 were extensively colocalized in most brain regions including the cerebellum and thalamus. In the cerebellum, immunoreactivity for both subtypes was prevalent in the molecular layer. The most intense immunoreactivity was found in Purkinje cell spines with a high density of immunoparticles at extrasynaptic sites peaking at around 240 nm from glutamatergic synapses between spines and parallel fibre varicosities. This is in contrast to dendrites at sites around GABAergic synapses where sparse and random distribution was found for both subtypes. In addition, more than one-tenth of the synaptic membrane specialization of spine-parallel fibre synapses were labelled at pre- or postsynaptic sites. Weak immunolabelling for both subtypes was also seen in parallel fibres but only rarely in GABAergic axons. In the ventrobasal thalamus, immunolabelling for both receptor subtypes was intense over the dendritic field of thalamocortical cells. Electron microscopy demonstrated an extrasynaptic localization of GABABR1a/b and R2 exclusively in postsynaptic elements. Quantitative analysis further revealed the density of GABABR1a/b around GABAergic synapses was higher than glutamatergic synapses on thalamocortical cell dendrites. The distinct localization of GABABRs relative to synaptic sites in the cerebellum and ventrobasal thalamus suggests that GABABRs differentially regulate activity of different neuronal populations. AU - Kulik, Ákos AU - Nakadate, Kazuhiko AU - Nyíri, Gábor AU - Notomi, Takuya AU - Malitschek, Barbara AU - Bettler, Bernhard AU - Shigemoto, Ryuichi ID - 2624 IS - 2 JF - European Journal of Neuroscience SN - 0953-816X TI - Distinct localization of GABAB receptors relative to synaptic sites in the rat cerebellum and ventrobasal thalamus VL - 15 ER - TY - CHAP AB - We outline the status of rigorous derivations of certain classical evolution equations as limits of Schrödinger dynamics. We explain two recent results jointly with H.T. Yau in more details. The first one is the derivation of the linear Boltzmann equation as the long time limit of the one-body Schrödinger equation with a random potential. The second one is the mean field limit of high density bosons with Coulomb interaction that leads to the nonlinear Hartree equation. AU - Erdös, László ID - 2694 SN - 9783540441113 T2 - Dynamics of Dissipation TI - Scaling limits of Schrödinger quantum mechanics ER - TY - JOUR AB - To understand the possible contribution of metabotropic γ-aminobutyric acid receptors (GABABR) in cortical development, we investigated the expression pattern and the cellular and subcellular localization of the GABABR1 and GABABR2 subtypes in the rat neocortex from embryonic day 14 (E14) to adulthood. At the light microscopic level, both GABABR1 and GABABR2 were detected as early as E14. During prenatal development, both subtypes were expressed highly in the cortical plate. Using double immunofluorescence, GABABR1 colocalized with GABABR2 in neurons of the marginal zone and subplate, indicating that these proteins are coexpressed and could be forming functional GABABRs during prenatal development in vivo. In contrast, only GABABR1 but not GABABR2 was detected in the tangentially migratory cells in the lower intermediate zone. During postnatal development, immunoreactivity for GABABR1 and GABABR2 was distributed mainly in pyramidal cells. Discrete GABABR1-immunopositive cell bodies of interneurons were present throughout the neocortex. In addition, GABABR1 but not GABABR2 was found in identified Cajal-Retzius cells in layer I. At the electron microscopic level, immunoreactivity for GABABR1 and GABABR2 was found in dendritic spines and dendritic shafts at extrasynaptic and perisynaptic sites throughout postnatal development. We further demonstrated the presynaptic localization of GABABR1 and GABABR2, as well as the association of the receptors with asymmetrical synaptic junctions. These results indicate potentially important roles for the GABABRs in the regulation of migratory processes during corticogenesis and in the modulation of synaptic transmission during early development of cortical circuitry. AU - López Bendito, Guillermina AU - Shigemoto, Ryuichi AU - Kulik, Ákos AU - Paulsen, Ole AU - Fairén, Alfonso AU - Luján, Rafael ID - 2622 IS - 11 JF - European Journal of Neuroscience SN - 0953-816X TI - Expression and distribution of metabotropic GABA receptor subtypes GABABR1 and GABABR2 during rat neocortical development VL - 15 ER - TY - JOUR AB - The release properties of glutamatergic nerve terminals are influenced by a number of factors, including the subtype of voltage-dependent calcium channel and the presence of presynaptic autoreceptors. Group III metabotropic glutamate receptors (mGluRs) mediate feedback inhibition of glutamate release by inhibiting Ca2+ channel activity. By imaging Ca2+ in preparations of cerebrocortical nerve terminals, we show that voltage-dependent Ca2+ channels are distributed in a heterogeneous manner in individual nerve terminals. Presynaptic terminals contained only N-type (47.5%; conotoxin GVIA-sensitive), P/Q-type (3.9%; agatoxin IVA-sensitive), or both N- and P/Q-type (42.6%) Ca2+ channels, although the remainder of the terminals (6.1%) were insensitive to these two toxins. In this preparation, two mGluRs with high and low affinity for L(+)-2-amino-4-phosphonobutyrate were identified by immunocytochemistry as mGluR4 and mGluR7, respectively. These receptors were responsible for 22.2 and 24.1% reduction of glutamate release, and they reduced the Ca2+ response in 24.4 and 30.3% of the nerve terminals, respectively. Interestingly, mGluR4 was largely (73.7%) located in nerve terminals expressing both N- and P/Q-type Ca2+ channels, whereas mGluR7 was predominantly (69.9%) located in N-type Ca2+ channel-expressing terminals. This specific coexpression of different group III mGluRs and Ca2+ channels may endow synaptic terminals with distinct release properties and reveals the existence of a high degree of presynaptic heterogeneity. AU - Millán, Carmelo AU - Luján, Rafael AU - Shigemoto, Ryuichi AU - Sánchez Prieto, José ID - 2621 IS - 49 JF - Journal of Biological Chemistry SN - 0021-9258 TI - Subtype-specific expression of Group III metabotropic glutamate receptors and Ca2+ channels in single nerve terminals VL - 277 ER - TY - JOUR AB - An ion channel's function depends largely on its location and density on neurons. Here we used high-resolution immunolocalization to determine the subcellular distribution of the hyperpolarization-activated and cyclic-nucleotide-gated channel subunit 1 (HCN1) in rat brain. Light microscopy revealed graded HCN1 immunoreactivity in apical dendrites of hippocampal, subicular and neocortical layer-5 pyramidal cells. Quantitative comparison of immunogold densities showed a 60-fold increase from somatic to distal apical dendritic membranes. Distal dendritic shafts had 16 times more HCN1 labeling than proximal dendrites of similar diameters. At the same distance from the soma, the density of HCN1 was significantly higher in dendritic shafts than in spines. Our results reveal the complex cell surface distribution of voltage-gated ion-channels, and predict its role in increasing the computational power of single neurons via subcellular domain and input-specific mechanisms. AU - Lörincz, Andrea AU - Notomi, Takuya AU - Tamás, Gábor AU - Shigemoto, Ryuichi AU - Nusser, Zoltán ID - 2620 IS - 11 JF - Nature Neuroscience SN - 1097-6256 TI - Polarized and compartment-dependent distribution of HCN1 in pyramidal cell dendrites VL - 5 ER - TY - JOUR AB - Metabotropic glutamate receptors (mGluRs) from group III reduce glutamate release. Because these receptors reduce cAMP levels, we explored whether this signaling pathway contributes to release inhibition caused by mGluRs with low affinity for L-2-amino-4-phosphonobutyrate (L-AP4). In biochemical experiments with the population of cerebrocortical nerve terminals we find that L-AP4 (1 mM) inhibited the Ca2+dependent-evoked release of glutamate by 25%. This inhibitory effect was largely prevented by the pertussis toxin but was insensitive to inhibitors of protein kinase C bisindolylmaleimide and protein kinase A H-89. Furthermore, this inhibition was associated with reduction in N-type Ca2+ channel activity in the absence of any detectable change in cAMP levels. In the presence of forskolin, however, L-AP4 decreased the levels of cAMP. The activation of this additional signaling pathway was very efficient in counteracting the facilitation of glutamate release induced either by forskolin or the β-adrenergic receptor agonist isoproterenol. Imaging experiments to measure Ca2+ dynamics in single nerve terminals showed that L-AP4 strongly reduced the Ca2+ response in 28% of the nerve terminals. Moreover, immunochemical experiments showed that 25-35% of the nerve terminals that were immunopositive to synaptophysin were also immunoreactive to the low affinity L-AP4-sensitive mGluR7. Then, mGluR7 mediates the inhibition of glutamate release caused by 1 mM L-AP4, primarily by a strong inhibition of Ca2+ channels, although high cAMP uncovers the receptor ability to decrease cAMP. AU - Millán, Carmelo AU - Luján, Rafael AU - Shigemoto, Ryuichi AU - Sánchez Prieto, José ID - 2614 IS - 16 JF - Journal of Biological Chemistry SN - 0021-9258 TI - The inhibition of glutamate release by metabotropic glutamate receptor 7 affects both [Ca2+]c and cAMP. Evidence for a strong reduction of Ca2+ entry in single nerve terminals VL - 277 ER - TY - JOUR AB - In this investigation, we report identification and characterization of a 95 kDa postsynaptic density protein (PSD-95)/discs-large/ ZO-1 (PDZ) domain-containing protein termed tamalin, also recently named GRP1-associated scaffold protein (GRASP), that interacts with group 1 metabotropic glutamate receptors (mGluRs). The yeast two-hybrid system and in vitro pull-down assays indicated that the PDZ domain-containing, amino-terminal half of tamalin directly binds to the class I PDZ-binding motif of group 1 mGluRs. The C-terminal half of tamalin also bound to cytohesins, the members of guanine nucleotide exchange factors (GEFs) specific for the ADP-ribosylation factor (ARF) family of small GTP-binding proteins. Tamalin mRNA is expressed predominantly in the telencephalic region and highly overlaps with the expression of group 1 mGluR mRNAs. Both tamalin and cytohesin-2 were enriched and codistributed with mGluR1a in postsynaptic membrane fractions. Importantly, recombinant and native mGluR1a/tamalin/cytohesin-2 complexes were coimmunoprecipitated from transfected COS-7 cells and rat brain tissue, respectively. Transfection of tamalin and mutant tamalin lacking a cytohesin-binding domain caused an increase and decrease in cell-surface expression of mGluR1a in COS-7 cells, respectively. Furthermore, adenovirus-mediated expression of tamalin and dominant-negative tamalin facilitated and reduced the neuritic distribution of endogenous mGluR5 in cultured hippocampal neurons, respectively. The results indicate that tamalin plays a key role in the association of group 1 mGluRs with the ARF-specific GEF proteins and contributes to intracellular trafficking and the macromolecular organization of group 1 mGluRs at synapses. AU - Kitano, Jun AU - Kimura, Kouji AU - Yamazaki, Yoshimitsu AU - Soda, Takeshi AU - Shigemoto, Ryuichi AU - Nakajima, Yoshiaki AU - Nakanishi, Shigetada ID - 2613 IS - 4 JF - Journal of Neuroscience SN - 0270-6474 TI - Tamalin, a PDZ domain-containing protein, links a protein complex formation of group 1 metabotropic glutamate receptors and the guanine nucleotide exchange factor cytohesins VL - 22 ER - TY - JOUR AB - Neurons in the rat cerebral cortex are enriched in group I metabotropic glutamate receptor (mGluR) subtypes and respond to their activation during development. To understand better the mechanisms by which mGluR1 and mGluR5 mediate these effects, the goal of this study was to elucidate the expression pattern and to determine the cellular and the precise subcellular localization of these two receptor subtypes in the rat neocortex and hippocampus during late prenatal and postnatal development. At the light microscopic level, mGluR1 α and mGluR5 were first detected in the cerebral cortex with different expression levels at embryonic day E18. Thus, mGluR5 had a moderate expression, whereas mGluR1 α was detected as a diffuse and weak labeling. mGluR5 was localized in some Cajal-Retzius cells as well as in other cell types, such as pioneer neurons of the marginal zone. During postnatal development, the distribution of the receptors dramatically changed. From P0 to around P10, mGluR1α was localized in identified, transient Cajal-Retzius cells of neocortex and hippocampus, until these cells disappear. In addition, a population of interneurons localized the receptor from the second/third postnatal week. In contrast, mGluR5 was localized mainly in pyramidal cells and in some interneurons, with a neuropilar staining throughout the cerebral cortex. At the electron microscopic level, the immunoreactivity for both group I mGluR subtypes was expressed postsynaptically. Using immunogold methods, mGluR1α and mGluR5 immunoreactivities were found throughout postnatal development at the edge of postsynaptic specialization of asymmetrical synapses. These results show that the two group I mGluRs have a differential expression pattern in neocortex and hippocampus that may suggest roles for the receptors in the early processing of cortical information and in the control of cortical developmental events. AU - López Bendito, Guillermina AU - Shigemoto, Ryuichi AU - Fairén, Alfonso AU - Luján, Rafael ID - 2616 IS - 6 JF - Cerebral Cortex SN - 1047-3211 TI - Differential distribution of group I metabotropic glutamate receptors during rat cortical development VL - 12 ER - TY - JOUR AB - The release of glutamate and GABA is modulated by presynaptic metabotropic glutamate receptors (mGluRs). We used immunocytochemical methods to define the location of the group III receptor mGluR7a in glutamatergic and GABAergic terminals innervating GABAergic interneurons and pyramidal cells. Immunoreactivity for mGluR7a was localized in the presynaptic active zone of both identified GABAergic and presumed glutamatergic terminals. Terminals innervating dendritic spines showed a variable level of receptor immunoreactivity, ranging from immunonegative to strongly immunopositive. The frequency of strongly mGluR7a positive terminals innervating the soma and dendrites of mGluR1α/somatostatin-expressing interneurons was very high relative to other neurons. On dendrites that received mGluR7a-enriched glutamatergic innervation, at least 80% of GABAergic terminals were immunopositive for mGluR7a. On such dendrites virtually all (95%) vasoactive intestinal polypeptide (VIP) positive (GABAergic) terminals were enriched in mGluR7a. The targets of VIP/mGluR7a-expressing terminals were mainly (88%) mGluR1α-expressing interneurons, which were mostly somatostatin immunopositive. Parvalbumin positive terminals were immunonegative for mGluR7a. Some parvalbumin immunoreactive dendrites received strongly mGluR7a positive terminals. The subcellular location, as well as the cell type and synapse-specific distribution of mGluR7a in isocortical neuronal circuits, is homologous to its distribution in the hippocampus. The specific location of mGluR7a in the presynaptic active zone of both glutamatergic and GABAergic synapses may be related to the proximity of calcium channels and the vesicle fusion machinery. The enrichment of mGluR7a in the main GABAergic, as well as in the glutamatergic, innervation of mGluR1α/somatostatin-expressing interneurons suggests that their activation is under unique regulation by extracellular glutamate. AU - Dalezios, Yannis AU - Luján, Rafael AU - Shigemoto, Ryuichi AU - Roberts, John AU - Somogyi, Péter ID - 2619 IS - 9 JF - Cerebral Cortex SN - 1047-3211 TI - Enrichment of mGluR7a in the Presynaptic active zones of GABAergic and Non-GABAergic terminals on interneurons in the rat somatosensory cortex VL - 12 ER - TY - JOUR AB - Taste-mGluR4, cloned from taste tissues, is a truncated variant of brain-expressed mGluR4a (brain-mGluR4), and is known to be a candidate for the receptor involved in the umami taste sense. Although the expression patterns of taste- and brain-mGluR4 mRNAs have been demonstrated, no mention has so far been made of the expression of these two mGluR4 proteins in taste tissues. The present study examined the expression of taste-mGluR4 and brain-mGluR4 proteins in rat taste tissues by using a specific antibody for mGluR4a which shared a C-terminus of both taste- and brain-mGluR4, for immunoblot analysis and immunohistochemistry. Immunoblot analysis showed that both brain-mGluR4 and taste-mGluR4 were expressed in the taste tissues. Taste-mGluR4 was not detected in the cerebellum. The immunoreactive band for brain-mGluR4 protein was much stronger than that for taste-mGluR4 protein. In the cryosections of fungiform, foliate and circumvallate papillae, the antibody against taste-mGluR4 exhibited intense labeling of the taste pores and taste hairs in all the taste buds of gustatory papillae examined; the immunoreaction to the antibody against brain-mGluR4 was more intense at the same sites of the taste buds. The portions of the taste bud cells below the taste pore and surrounding keratinocytes did not show any immunoreactivities. The results of the present study strongly suggest that, in addition to taste-mGluR4, brain-mGluR4 may function even more importantly than the former as a receptor for glutamate, i.e. the umami taste sensation. AU - Toyono, Takashi AU - Seta, Yuji AU - Sataoka, Shinji AU - Harada, Harumi AU - Morotomi, Takahiko AU - Kawano, Shintaro AU - Shigemoto, Ryuichi AU - Toyoshima, Kuniaki ID - 2615 IS - 1 JF - Archives of Histology and Cytology SN - 0914-9465 TI - Expression of the metabotropic glutamate receptor, mGluR4a, in the taste hairs of taste buds in rat gustatory papillae VL - 65 ER - TY - JOUR AB - The unipolar brush cell (UBC) is a type of glutamatergic interneuron in the granular layer of the cerebellum. The UBC brush and a single mossy fiber (MF) terminal contact each other within a cerebellar glomerulus, forming a giant synapse. Many UBCs receive input from extrinsic MFs, whereas others are innervated by intrinsic mossy terminals formed by the axons of other UBCs. In all mammalian species so far examined, the vestibulocerebellum is enriched of UBCs that are strongly immunoreactive for the calcium binding protein calretinin (CR) in both the somatodendritic and axonal compartment. UBCs have postsynaptic ionotropic glutamate receptors and extrasynaptic metabotropic glutamate receptors that immunocytochemically highlight their somatodendritic compartment and brush, respectively. In this study on the mouse cerebellum, we present evidence that immunoreactivities to CR and mGluR1α define two distinct UBC subsets with partly overlapping distributions in lobule X (the nodulus). In sections double-labeled for CR and mGluR1α, the patterns of distributions of CR+/mGluR1α- UBCs and CR-/mGluR1α+ UBCs differed along the mediolateral and dorsoventral axes of the folium. Moreover, mGluR1α+ UBCs outnumbered CR+ UBCs. Both UBC subsets were mGluR2/3, GluR2/3, and NMDAR1 immunoreactive. The different distribution patterns of the two UBC subsets within lobule X suggest that expression of CR or mGluR1α by UBCs may be afferent-specific and related to the terminal fields of different vestibular MF afferents. AU - Nunzi, Maria AU - Shigemoto, Ryuichi AU - Mugnaini, Enrico ID - 2618 IS - 2 JF - Journal of Comparative Neurology SN - 0021-9967 TI - Differential expression of calretinin and metabotropic glutamate receptor mGluR1α defines subsets of unipolar brush cells in mouse cerebellum VL - 451 ER - TY - CONF AB - Intersection graphs of disks and of line segments, respectively, have been well studied, because of both, practical applications and theoretically interesting properties of these graphs. Despite partial results, the complexity status of the Clique problem for these two graph classes is still open. Here, we consider the Clique problem for intersection graphs of ellipses which in a sense, interpolate between disc and ellipses, and show that it is APX-hard in that case. Moreover, this holds even if for all ellipses, the ratio of the larger over the smaller radius is some prescribed number. To our knowledge, this is the first hardness result for the Clique problem in intersection graphs of objects with finite description complexity. We also describe a simple approximation algorithm for the case of ellipses for which the ratio of radii is bounded. AU - Ambühl, Christoph AU - Wagner, Uli ID - 2421 SN - 9783540001423 T2 - Proceedings of the 13th International Symposium on Algorithms and Computation TI - On the Clique problem in intersection graphs of ellipses VL - 2518 ER - TY - JOUR AB - A commonly used theoretical definition of superfluidity in the ground state of a Bose gas is based on the response of the system to an imposed velocity field or, equivalently, to twisted boundary conditions in a box. We are able to carry out this program in the case of a dilute interacting Bose gas in a trap, and we prove that a gas with repulsive interactions is 100% superfluid in the dilute limit in which the Gross-Pitaevskii equation is exact. This is the first example in an experimentally realistic continuum model in which superfluidity is rigorously verified. AU - Lieb, Élliott AU - Seiringer, Robert AU - Yngvason, Jakob ID - 2353 IS - 13 JF - Physical Review B - Condensed Matter and Materials Physics SN - 0163-1829 TI - Superfluidity in dilute trapped Bose gases VL - 66 ER - TY - JOUR AB - A corner cut in dimension d is a finite subset of N0d that can be separated from its complement in N0d by an affine hyperplane disjoint from N0d. Corner cuts were first investigated by Onn and Sturmfels [Adv. Appl. Math. 23 (1999) 29-48], their original motivation stemmed from computational commutative algebra. Let us write (Nd0k)cut for the set of corner cuts of cardinality k; in the computational geometer's terminology, these are the k-sets of N0d. Among other things, Onn and Sturmfels give an upper bound of O(k2d(d-1)/(d+1)) for the size of (Nd0k)cut when the dimension is fixed. In two dimensions, it is known (see [Corteel et al., Adv. Appl. Math. 23 (1) (1999) 49-53]) that #(Nd0k)cut = Θ(k log k). We will see that in general, for any fixed dimension d, the order of magnitude of #(Nd0k)cut is between kd-1 log k and (k log k)d-1. (It has been communicated to me that the same bounds have been found independently by G. Rémond.) In fact, the elements of (Nd0k)cut correspond to the vertices of a certain polytope, and what our proof shows is that the above upper bound holds for the total number of flags of that polytope. AU - Wagner, Uli ID - 2420 IS - 2 JF - Advances in Applied Mathematics SN - 0196-8858 TI - On the number of corner cuts VL - 29 ER - TY - CHAP AB - Now that the low temperature properties of quantum-mechanical many-body systems (bosons) at low density, ρ, can be examined experimentally it is appropriate to revisit some of the formulas deduced by many authors 4-5 decades ago. For systems with repulsive (i.e. positive) interaction potentials the experimental low temperature state and the ground state are effectively synonymous -- and this fact is used in all modeling. In such cases, the leading term in the energy/particle is 2πℏ2aρ/m where a is the scattering length of the two-body potential. Owing to the delicate and peculiar nature of bosonic correlations (such as the strange N7/5 law for charged bosons), four decades of research failed to establish this plausible formula rigorously. The only previous lower bound for the energy was found by Dyson in 1957, but it was 14 times too small. The correct asymptotic formula has recently been obtained by us and this work will be presented. The reason behind the mathematical difficulties will be emphasized. A different formula, postulated as late as 1971 by Schick, holds in two-dimensions and this, too, will be shown to be correct. With the aid of the methodology developed to prove the lower bound for the homogeneous gas, two other problems have been successfully addressed. One is the proof by us that the Gross-Pitaevskii equation correctly describes the ground state in the `traps' actually used in the experiments. For this system it is also possible to prove complete Bose condensation, as we have shown. Another topic is a proof that Foldy's 1961 theory of a high density Bose gas of charged particles correctly describes its ground state energy. AU - Lieb, Élliott AU - Solovej, Jan AU - Seiringer, Robert AU - Yngvason, Jakob ID - 2338 SN - 9781571461018 T2 - Current Developments in Mathematics, 2001 TI - The ground state of the Bose gas ER - TY - JOUR AB - A new solvent-free composite polymer electrolyte consisting of high-molecular mass polyethylene oxide (PEO) filled with titanium oxide and containing LiI and I2 was developed. The introduction of the inorganic filler (TiO2 Degussa P25) into the polymer matrix produces dramatic morphological changes to the host polymer structure. Upon addition of the inorganic oxide, the surface roughness increases, with respect to the original polymer and in parallel, the fractal dimension decreases. Both the thermograms and the atomic force microscope (AFM) pictures confirm the amorphicity of the composite electrolyte. The polymer sub-units are held together in a parallel orientation, forming straight long chains of about 500 nm in width, along which TiO2 spherical particles of about 20-25 nm in diameter are distributed. The polymer chains separated by the titania particles are arranged in a three-dimensional, mechanically stable network, that creates free space and voids into which the iodide/triodide anions can easily migrate. All solid-state dye-sensitized solar cells fabricated using this composite electrolyte present high efficiencies (typical maximum incident photon to current efficiency (IPCE) as high as 40% at 520 nm and overall conversion efficiency (η) of 0.96% (Voc = 0.67 V, Jsc = 2.050 mA/cm2, FF = 39%) under direct solar irradiation. Further improvement of the photovoltaic performance is expected by optimization of the electrolyte parameters and of the cell assembly. AU - Katsaros, Georgios AU - Stergiopoulos, Thomas AU - Arabatzis, Iannis AU - Papadokostaki, Kyriaki AU - Falaras, Polycarpos ID - 1737 IS - 1-3 JF - Journal of Photochemistry and Photobiology A: Chemistry SN - 1010-6030 TI - A solvent-free composite polymer/inorganic oxide electrolyte for high efficiency solid-state dye-sensitized solar cells VL - 149 ER - TY - JOUR AB - Using the Pauli-Fierz model of non-relativistic quantum electrodynamics, we calculate the binding energy of an electron in the field of a nucleus of charge Z and in presence of the quantized radiation field. We consider the case of small coupling constant α, but fixed Zα and ultraviolet cut-off Λ. We prove that after renormalizing the mass the binding energy has, to leading order in α, a finite limit as Λ goes to infinity; i.e., the cut-off can be removed. The expression for the ground state energy shift thus obtained agrees with Bethe's formula for small values of Zα, but shows a different behavior for bigger values. AU - Hainzl, Christian AU - Seiringer, Robert ID - 2350 IS - 5 JF - Advances in Theoretical and Mathematical Physics SN - 1095-0761 TI - Mass renormalization and energy level shift in non-relativistic QED VL - 6 ER - TY - JOUR AB - We study fitness landscape in the space of protein sequences by relating sets of human pathogenic missense mutations in 32 proteins to amino acid substitutions that occurred in the course of evolution of these proteins. On average, ≈10% of deviations of a nonhuman protein from its human ortholog are compensated pathogenic deviations (CPDs), i.e., are caused by an amino acid substitution that, at this site, would be pathogenic to humans. Normal functioning of a CPD-containing protein must be caused by other, compensatory deviations of the nonhuman species from humans. Together, a CPD and the corresponding compensatory deviation form a Dobzhansky-Muller incompatibility that can be visualized as the corner on a fitness ridge. Thus, proteins evolve along fitness ridges which contain only ≈10 steps between sucessive corners. The fraction of CPDs among all deviations of a protein from its human ortholog does not increase with the evolutionary distance between the proteins, indicating that subtitutions that carry evolving proteins around these corners occur in rapid succession, driven by positive selection. Data on fitness of interspecies hybrids suggest that the compensatory change that makes a CPD fit usually occurs within the same protein. Data on protein structures and on cooccurrence of amino acids at different sites of multiple orthologous proteins often make it possible to provisionally identify the substitution that compensates a partiCUlar CPD. AU - Kondrashov, Alexey AU - Sunyaev, Shamil AU - Kondrashov, Fyodor ID - 885 IS - 23 JF - PNAS SN - 0027-8424 TI - Dobzhansky-Muller incompatibilities in protein evolution VL - 99 ER - TY - JOUR AB - Extending work of Bielawski-Dancer 3 and Konno 14, we develop a theory of toric hyperkähler varieties, which involves toric geometry, matroid theory and convex polyhedra. The framework is a detailed study of semi-projective toric varieties, meaning GIT quotients of affine spaces by torus actions, and specifically, of Lawrence toric varieties, meaning GIT quotients of even-dimensional affine spaces by symplectic torus actions. A toric hyperkähler variety is a complete intersection in a Lawrence toric variety. Both varieties are non-compact, and they share the same cohomology ring, namely, the Stanley-Reisner ring of a matroid modulo a linear system of parameters. Familiar applications of toric geometry to combinatorics, including the Hard Lefschetz Theorem and the volume polynomials of Khovanskii-Pukhlikov 11, are extended to the hyperkähler setting. When the matroid is graphic, our construction gives the toric quiver varieties, in the sense of Nakajima 17. AU - Hausel, Tamas AU - Sturmfels, Bernd ID - 1451 IS - 1 JF - Documenta Mathematica SN - 1431-0635 TI - Toric hyperkähler varieties VL - 7 ER - TY - JOUR AB - Transcription is a slow and expensive process: in eukaryotes, approximately 20 nucleotides can be transcribed per second at the expense of at least two ATP molecules per nucleotide. Thus, at least for highly expressed genes, transcription of long introns, which are particularly common in mammals, is costly. Using data on the expression of genes that encode proteins in Caenorhabditis elegans and Homo sapiens, we show that introns in highly expressed genes are substantially shorter than those in genes that are expressed at low levels. This difference is greater in humans, such that introns are, on average, 14 times shorter in highly expressed genes than in genes with low expression, whereas in C. Elegans the difference in intron length is only twofold. In contrast, the density of introns in a gene does not strongly depend on the level of gene expression. Thus, natural selection appears to favor short introns in highly expressed genes to minimize the cost of transcription and other molecular processes, such as splicing. AU - Castillo Davis, Cristian AU - Mekhedov, Sergei AU - Hartl, Daniel AU - Koonin, Eugene AU - Kondrashov, Fyodor ID - 897 IS - 4 JF - Nature Genetics TI - Selection for short introns in highly expressed genes VL - 31 ER - TY - JOUR AB - BACKGROUND: Gene duplications have a major role in the evolution of new biological functions. Theoretical studies often assume that a duplication per se is selectively neutral and that, following a duplication, one of the gene copies is freed from purifying (stabilizing) selection, which creates the potential for evolution of a new function. RESULTS: In search of systematic evidence of accelerated evolution after duplication, we used data from 26 bacterial, six archaeal, and seven eukaryotic genomes to compare the mode and strength of selection acting on recently duplicated genes (paralogs) and on similarly diverged, unduplicated orthologous genes in different species. We find that the ratio of nonsynonymous to synonymous substitutions (Kn/Ks) in most paralogous pairs is <<1 and that paralogs typically evolve at similar rates, without significant asymmetry, indicating that both paralogs produced by a duplication are subject to purifying selection. This selection is, however, substantially weaker than the purifying selection affecting unduplicated orthologs that have diverged to the same extent as the analyzed paralogs. Most of the recently duplicated genes appear to be involved in various forms of environmental response; in particular, many of them encode membrane and secreted proteins. CONCLUSIONS: The results of this analysis indicate that recently duplicated paralogs evolve faster than orthologs with the same level of divergence and similar functions, but apparently do not experience a phase of neutral evolution. We hypothesize that gene duplications that persist in an evolving lineage are beneficial from the time of their origin, due primarily to a protein dosage effect in response to variable environmental conditions; duplications are likely to give rise to new functions at a later phase of their evolution once a higher level of divergence is reached. AU - Kondrashov, Fyodor AU - Rogozin, Igor AU - Wolf, Yuri AU - Koonin, Eugene ID - 871 IS - 2 JF - Genome Biology SN - 1465-6906 TI - Selection in the evolution of gene duplications VL - 3 ER - TY - JOUR AB - The polymeric ubiquitin (poly-u) genes are composed of tandem 228-bp repeats with no spacer sequences between individual monomer units. Ubiquitin is one of the most conserved proteins known to date, and the individual units within a number of poly-u genes are significantly more similar to each other than would be expected if each unit evolved independently. It has been proposed that the rather striking similarity among poly-u monomers in some lineages is caused by a series of homogenization events. Here we report the sequences of the polyubiquitin-C (Ubc) genes in two mouse strains. Analysis of these sequences, as well as those of the previously reported Chinese hamster and rat poly-u genes, supports the assertion that the homogenization of the ubiquitin-C gene in rodents is due to unequal crossing-over events. The sequence divergence of noncoding DNA was used to estimate the frequency of unequal crossing-over events (6.3 x 10-5 events per generation) in the Ubc gene, as well as to provide evidence of apparent selection in the poly-u gene. AU - Perelygin, Andrey AU - Kondrashov, Fyodor AU - Rogozin, Igor AU - Brinton, Margo ID - 859 IS - 2 JF - Journal of Molecular Evolution SN - 0022-2844 TI - Evolution of the mouse polyubiquitin C gene VL - 55 ER - TY - JOUR AB - Let k⩾5 be an integer, and let x⩾1 be an arbitrary real number. We derive a bound[Formula presented] for the number of positive integers less than or equal to x which can be represented as a sum of two non-negative coprime kth powers, in essentially more than one way. AU - Browning, Timothy D ID - 204 IS - 2 JF - Journal of Number Theory SN - 0022-314X TI - Equal Sums of Two kth Powers VL - 96 ER -