@article{11125, abstract = {Although nuclear envelope (NE) assembly is known to require the GTPase Ran, the membrane fusion machinery involved is uncharacterized. NE assembly involves formation of a reticular network on chromatin, fusion of this network into a closed NE and subsequent expansion. Here we show that p97, an AAA-ATPase previously implicated in fusion of Golgi and transitional endoplasmic reticulum (ER) membranes together with the adaptor p47, has two discrete functions in NE assembly. Formation of a closed NE requires the p97–Ufd1–Npl4 complex, not previously implicated in membrane fusion. Subsequent NE growth involves a p97–p47 complex. This study provides the first insights into the molecular mechanisms and specificity of fusion events involved in NE formation.}, author = {HETZER, Martin W and Meyer, Hemmo H. and Walther, Tobias C. and Bilbao-Cortes, Daniel and Warren, Graham and Mattaj, Iain W.}, issn = {1476-4679}, journal = {Nature Cell Biology}, keywords = {Cell Biology}, number = {12}, pages = {1086--1091}, publisher = {Springer Nature}, title = {{Distinct AAA-ATPase p97 complexes function in discrete steps of nuclear assembly}}, doi = {10.1038/ncb1201-1086}, volume = {3}, year = {2001}, } @article{11892, abstract = {We present the first fully dynamic algorithm for maintaining a minimum spanning forest in time 𝑜(𝑛√) per operation. To be precise, the algorithm uses O(n1/3 log n) amortized time per update operation. The algorithm is fairly simple and deterministic. An immediate consequence is the first fully dynamic deterministic algorithm for maintaining connectivity and bipartiteness in amortized time O(n1/3 log n) per update, with O(1) worst case time per query.}, author = {Henzinger, Monika H and King, Valerie}, issn = {1095-7111}, journal = {SIAM Journal on Computing}, number = {2}, pages = {364--374}, publisher = {Society for Industrial & Applied Mathematics}, title = {{Maintaining minimum spanning forests in dynamic graphs}}, doi = {10.1137/s0097539797327209}, volume = {31}, year = {2001}, } @inproceedings{11914, abstract = {Previous studies of the Web graph structure have focused on the graph structure at the level of individual pages. In actuality the Web is a hierarchically nested graph, with domains, hosts and Web sites introducing intermediate levels of affiliation and administrative control. To better understand the growth of the Web we need to understand its macro-structure, in terms of the linkage between Web sites. We approximate this by studying the graph of the linkage between hosts on the Web. This was done based on snapshots of the Web taken by Google in Oct 1999, Aug 2000 and Jun 2001. The connectivity between hosts is represented by a directed graph, with hosts as nodes and weighted edges representing the count of hyperlinks between pages on the corresponding hosts. We demonstrate how such a "hostgraph" can be used to study connectivity properties of hosts and domains over time, and discuss a modified "copy model" to explain observed link weight distributions as a function of subgraph size. We discuss changes in the Web over time in the size and connectivity of Web sites and country domains. We also describe a data mining application of the hostgraph: a related host finding algorithm which achieves a precision of 0.65 at rank 3.}, author = {Bharat, K. and Chang, Bay-Wei and Henzinger, Monika H and Ruhl, M.}, booktitle = {1st IEEE International Conference on Data Mining}, isbn = {0-7695-1119-8}, issn = {15504786}, location = {San Jose, CA, United States}, pages = {51--58}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Who links to whom: Mining linkage between Web sites}}, doi = {10.1109/ICDM.2001.989500}, year = {2001}, } @misc{3507, abstract = {A molecular classification method is based on a space filling description of a molecule. The three dimensional body corresponding to the space filling molecular structure is divided into Voronoi regions to provide a basis for efficiently processing local structural information. A Delaunay triangulation provides a basis for systematically processing information relating to the Voronoi regions into shape descriptors in the form of topological elements. Preferably, additional shape and/or property descriptors are included in the classification method. The classification methods generally are used to identify similarities between molecules that can be used as property predictors for a variety of applications. Generally, the property predictions are the basis for selection of compounds for incorporation into efficacy evaluations.}, author = {Liang, Jie and Edelsbrunner, Herbert}, title = {{Molecular classification for property prediction}}, year = {2001}, } @book{3586, abstract = {The book combines topics in mathematics (geometry and topology), computer science (algorithms), and engineering (mesh generation). The original motivation for these topics was the difficulty faced (both conceptually and in the technical execution) in any attempt to combine elements of combinatorial and of numerical algorithms. Mesh generation is a topic where a meaningful combination of these different approaches to problem solving is inevitable. The book develops methods from both areas that are amenable to combination, and explains recent breakthrough solutions to meshing that fit into this category.The book should be an ideal graduate text for courses on mesh generation. The specific material is selected giving preference to topics that are elementary, attractive, lend themselves to teaching, useful, and interesting.}, author = {Edelsbrunner, Herbert}, isbn = {0-521-79309-2}, pages = {190}, publisher = {Cambridge University Press}, title = {{Geometry and Topology for Mesh Generation}}, doi = {10.1017/CBO9780511530067}, volume = {7}, year = {2001}, } @inproceedings{3447, author = {Krishnendu Chatterjee and Dasgupta, Pallab and Chakrabarti, Partha P}, publisher = {Elsevier}, title = {{Weighted quantified computation tree logic}}, year = {2001}, } @article{8522, abstract = {For diffeomorphisms of smooth compact manifolds, we consider the problem of how fast the number of periodic points with period $n$grows as a function of $n$. In many familiar cases (e.g., Anosov systems) the growth is exponential, but arbitrarily fast growth is possible; in fact, the first author has shown that arbitrarily fast growth is topologically (Baire) generic for $C^2$ or smoother diffeomorphisms. In the present work we show that, by contrast, for a measure-theoretic notion of genericity we call ``prevalence'', the growth is not much faster than exponential. Specifically, we show that for each $\delta > 0$, there is a prevalent set of ( $C^{1+\rho}$ or smoother) diffeomorphisms for which the number of period $n$ points is bounded above by $\operatorname{exp}(C n^{1+\delta})$ for some $C$ independent of $n$. We also obtain a related bound on the decay of the hyperbolicity of the periodic points as a function of $n$. The contrast between topologically generic and measure-theoretically generic behavior for the growth of the number of periodic points and the decay of their hyperbolicity shows this to be a subtle and complex phenomenon, reminiscent of KAM theory.}, author = {Kaloshin, Vadim and Hunt, Brian R.}, issn = {1079-6762}, journal = {Electronic Research Announcements of the American Mathematical Society}, keywords = {General Mathematics}, number = {4}, pages = {17--27}, publisher = {American Mathematical Society}, title = {{A stretched exponential bound on the rate of growth of the number of periodic points for prevalent diffeomorphisms I}}, doi = {10.1090/s1079-6762-01-00090-7}, volume = {7}, year = {2001}, } @article{8521, abstract = {We continue the previous article's discussion of bounds, for prevalent diffeomorphisms of smooth compact manifolds, on the growth of the number of periodic points and the decay of their hyperbolicity as a function of their period $n$. In that article we reduced the main results to a problem, for certain families of diffeomorphisms, of bounding the measure of parameter values for which the diffeomorphism has (for a given period $n$) an almost periodic point that is almost nonhyperbolic. We also formulated our results for $1$-dimensional endomorphisms on a compact interval. In this article we describe some of the main techniques involved and outline the rest of the proof. To simplify notation, we concentrate primarily on the $1$-dimensional case.}, author = {Kaloshin, Vadim and Hunt, Brian R.}, issn = {1079-6762}, journal = {Electronic Research Announcements of the American Mathematical Society}, keywords = {General Mathematics}, number = {5}, pages = {28--36}, publisher = {American Mathematical Society}, title = {{A stretched exponential bound on the rate of growth of the number of periodic points for prevalent diffeomorphisms II}}, doi = {10.1090/s1079-6762-01-00091-9}, volume = {7}, year = {2001}, } @article{8524, abstract = {A number α∈R is diophantine if it is not well approximable by rationals, i.e. for some C,ε>0 and any relatively prime p,q∈Z we have |αq−p|>Cq−1−ε. It is well-known and is easy to prove that almost every α in R is diophantine. In this paper we address a noncommutative version of the diophantine properties. Consider a pair A,B∈SO(3) and for each n∈Z+ take all possible words in A, A -1, B, and B - 1 of length n, i.e. for a multiindex I=(i1,i1,…,im,jm) define |I|=∑mk=1(|ik|+|jk|)=n and \( W_n(A,B ) = \{W_{\cal I}(A,B) = A^{i_1} B^{j_1} \dots A^{i_m} B^{j_m}\}_{|{\cal I|}=n \).¶Gamburd—Jakobson—Sarnak [GJS] raised the problem: prove that for Haar almost every pair A,B∈SO(3) the closest distance of words of length n to the identity, i.e. sA,B(n)=min|I|=n∥WI(A,B)−E∥, is bounded from below by an exponential function in n. This is the analog of the diophantine property for elements of SO(3). In this paper we prove that s A,B (n) is bounded from below by an exponential function in n 2. We also exhibit obstructions to a “simple” proof of the exponential estimate in n.}, author = {Kaloshin, Vadim and Rodnianski, I.}, issn = {1016-443X}, journal = {Geometric And Functional Analysis}, number = {5}, pages = {953--970}, publisher = {Springer Nature}, title = {{Diophantine properties of elements of SO(3)}}, doi = {10.1007/s00039-001-8222-8}, volume = {11}, year = {2001}, } @article{9444, abstract = {Epigenetic silenced alleles of the Arabidopsis SUPERMANlocus (the clark kent alleles) are associated with dense hypermethylation at noncanonical cytosines (CpXpG and asymmetric sites, where X = A, T, C, or G). A genetic screen for suppressors of a hypermethylated clark kent mutant identified nine loss-of-function alleles of CHROMOMETHYLASE3(CMT3), a novel cytosine methyltransferase homolog. These cmt3 mutants display a wild-type morphology but exhibit decreased CpXpG methylation of the SUP gene and of other sequences throughout the genome. They also show reactivated expression of endogenous retrotransposon sequences. These results show that a non-CpG DNA methyltransferase is responsible for maintaining epigenetic gene silencing.}, author = {Lindroth, A. M. and Cao, Xiaofeng and Jackson, James P. and Zilberman, Daniel and McCallum, Claire M. and Henikoff, Steven and Jacobsen, Steven E.}, issn = {1095-9203}, journal = {Science}, keywords = {Multidisciplinary}, number = {5524}, pages = {2077--2080}, publisher = {American Association for the Advancement of Science}, title = {{Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation}}, doi = {10.1126/science.1059745}, volume = {292}, year = {2001}, } @inproceedings{4634, abstract = {A controller is an environment for a system that achieves a particular control objective by providing inputs to the system without constraining the choices of the system. For synchronous systems, where system and controller make simultaneous and interdependent choices, the notion that a controller must not constrain the choices of the system can be formalized by type systems for composability. In a previous paper, we solved the control problem for static and dynamic types: a static type is a dependency relation between inputs and outputs, and composition is well-typed if it does not introduce cyclic dependencies; a dynamic type is a set of static types, one for each state. Static and dynamic types, however, cannot capture many important digital circuits, such as gated clocks, bidirectional buses, and random-access memory. We therefore introduce more general type systems, so-called dependent and bidirectional types, for modeling these situations, and we solve the corresponding control problems. In a system with a dependent type, the dependencies between inputs and outputs are determined gradually through a game of the system against the controller. In a system with a bidirectional type, also the distinction between inputs and outputs is resolved dynamically by such a game. The game proceeds in several rounds. In each round the system and the controller choose to update some variables dependent on variables that have already been updated. The solution of the control problem for dependent and bidirectional types is based on algorithms for solving these games.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy}, booktitle = {Proceedings of the 12th International Conference on on Concurrency Theory}, isbn = {9783540424970}, location = {Aalborg, Denmark}, pages = {566 -- 581}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{The control of synchronous systems, Part II}}, doi = {10.1007/3-540-44685-0_38}, volume = {2154}, year = {2001}, } @inproceedings{4633, abstract = {A procedure for the analysis of state spaces is called symbolic if it manipulates not individual states, but sets of states that are represented by constraints. Such a procedure can be used for the analysis of infinite state spaces, provided termination is guaranteed. We present symbolic procedures, and corresponding termination criteria, for the solution of infinite-state games, which occur in the control and modular verification of infinite-state systems. To characterize the termination of symbolic procedures for solving infinite-state games, we classify these game structures into four increasingly restrictive categories: 1 Class 1 consists of infinite-state structures for which all safety and reachability games can be solved. 2 Class 2 consists of infinite-state structures for which all ω-regular games can be solved. 3 Class 3 consists of infinite-state structures for which all nested positive boolean combinations of ω-regular games can be solved. 4 Class 4 consists of infinite-state structures for which all nested boolean combinations of ω-regular games can be solved. We give a structural characterization for each class, using equivalence relations on the state spaces of games which range from game versions of trace equivalence to a game version of bisimilarity. We provide infinite-state examples for all four classes of games from control problems for hybrid systems. We conclude by presenting symbolic algorithms for the synthesis of winning strategies (“controller synthesis”) for infinitestate games with arbitrary ω-regular objectives, and prove termination over all class-2 structures. This settles, in particular, the symbolic controller synthesis problem for rectangular hybrid systems.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Majumdar, Ritankar}, booktitle = {Proceedings of the 12th International Conference on on Concurrency Theory}, isbn = {9783540424970}, location = {Aalborg, Denmark}, pages = {536 -- 550}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Symbolic algorithms for infinite-state games}}, doi = {10.1007/3-540-44685-0_36}, volume = {2154}, year = {2001}, } @inproceedings{4636, abstract = {Abstract. Dynamic programs, or fixpoint iteration schemes, are useful for solving many problems on state spaces, including model checking on Kripke structures (“verification”), computing shortest paths on weighted graphs (“optimization”), computing the value of games played on game graphs (“control”). For Kripke structures, a rich fixpoint theory is available in the form of the µ-calculus. Yet few connections have been made between different interpretations of fixpoint algorithms. We study the question of when a particular fixpoint iteration scheme ϕ for verifying an ω-regular property Ψ on a Kripke structure can be used also for solving a two-player game on a game graph with winning objective Ψ. We provide a sufficient and necessary criterion for the answer to be affirmative in the form of an extremal-model theorem for games: under a game interpretation, the dynamic program ϕ solves the game with objective Ψ if and only if both (1) under an existential interpretation on Kripke structures, ϕ is equivalent to ∃Ψ, and (2) under a universal interpretation on Kripke structures, ϕ is equivalent to ∀Ψ. In other words, ϕ is correct on all two-player game graphs iff it is correct on all extremal game graphs, where one or the other player has no choice of moves. The theorem generalizes to quantitative interpretations, where it connects two-player games with costs to weighted graphs. While the standard translations from ω-regular properties to the µ-calculus violate (1) or (2), we give a translation that satisfies both conditions. Our construction, therefore, yields fixpoint iteration schemes that can be uniformly applied on Kripke structures, weighted graphs, game graphs, and game graphs with costs, in order to meet or optimize a given ω-regular objective.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Majumdar, Ritankar}, booktitle = {Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science}, isbn = {076951281X}, location = {Boston, MA, USA}, pages = {279 -- 290}, publisher = {IEEE}, title = {{From verification to control: dynamic programs for omega-regular objectives}}, doi = {10.1109/LICS.2001.932504}, year = {2001}, } @inproceedings{4635, abstract = {We show how model checking techniques can be applied to the analysis of connectivity and cost-of-traversal properties of Web sites.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy}, booktitle = {Proceedings of the 10th international conference on World Wide Web}, isbn = {9781581133486}, location = {Hong Kong, Hong Kong}, pages = {86 -- 87}, publisher = {ACM}, title = {{MCWEB: A model-checking tool for web-site debugging}}, year = {2001}, } @inproceedings{4632, abstract = {We present a compositional trace-based model for probabilistic systems. The behavior of a system with probabilistic choice is a stochastic process, namely, a probability distribution on traces, or “bundle.” Consequently, the semantics of a system with both nondeterministic and probabilistic choice is a set of bundles. The bundles of a composite system can be obtained by combining the bundles of the components in a simple mathematical way. Refinement between systems is bundle containment. We achieve assume-guarantee compositionality for bundle semantics by introducing two scoping mechanisms. The first mechanism, which is standard in compositional modeling, distinguishes inputs from outputs and hidden state. The second mechanism, which arises in probabilistic systems, partitions the state into probabilistically independent regions.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Jhala, Ranjit}, booktitle = {Proceedings of the 12th International Conference on on Concurrency Theory}, isbn = {9783540424970}, location = {Aalborg, Denmark}, pages = {351 -- 365}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Compositional methods for probabilistic systems}}, doi = {10.1007/3-540-44685-0_24}, volume = {2154}, year = {2001}, } @inproceedings{4600, abstract = {Model checking is a practical tool for automated debugging of embedded software. In model checking, a high-level description of a system is compared against a logical correctness requirement to discover inconsistencies. Since model checking is based on exhaustive state-space exploration and the size of the state space of a design grows exponentially with the size of the description, scalability remains a challenge. We have thus developed techniques for exploiting modular design structure during model checking, and the model checker jMocha (Java MOdel-CHecking Algorithm) is based on this theme. Instead of manipulating unstructured state-transition graphs, it supports the hierarchical modeling framework of reactive modules. jMocha is a growing interactive software environment for specification, simulation and verification, and is intended as a vehicle for the development of new verification algorithms and approaches. It is written in Java and uses native C-code BDD libraries from VIS. jMocha offers: (1) a GUI that looks familiar to Windows/Java users; (2) a simulator that displays traces in a message sequence chart fashion; (3) requirements verification both by symbolic and enumerative model checking; (4) implementation verification by checking trace containment; (5) a proof manager that aids compositional and assume-guarantee reasoning; and (6) SLANG (Scripting LANGuage) for the rapid and structured development of new verification algorithms. jMocha is available publicly at ; it is a successor and extension of the original Mocha tool that was entirely written in C.}, author = {Alur, Rajeev and De Alfaro, Luca and Grosu, Radu and Henzinger, Thomas A and Kang, Myong and Kirsch, Christoph and Majumdar, Ritankar and Mang, Freddy and Wang, Bow}, booktitle = {Proceedings of the 23rd International Conference on Software Engineering}, isbn = {0769510507}, pages = {835 -- 836}, publisher = {IEEE}, title = {{jMocha: A model-checking tool that exploits design structure}}, doi = {10.1109/ICSE.2001.919196}, year = {2001}, } @article{4599, abstract = {State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic state-space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.}, author = {Alur, Rajeev and Brayton, Robert and Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram}, issn = {0925-9856}, journal = {Formal Methods in System Design}, number = {2}, pages = {97 -- 116}, publisher = {Springer}, title = {{Partial-order reduction in symbolic state-space exploration}}, doi = {10.1023/A:1008767206905}, volume = {18}, year = {2001}, } @inproceedings{4622, abstract = {Conventional type systems specify interfaces in terms of values and domains. We present a light-weight formalism that captures the temporal aspects of software component interfaces. Specifically, we use an automata-based language to capture both input assumptions about the order in which the methods of a component are called, and output guarantees about the order in which the component calls external methods. The formalism supports automatic compatability checks between interface models, and thus constitutes a type system for component interaction. Unlike traditional uses of automata, our formalism is based on an optimistic approach to composition, and on an alternating approach to design refinement. According to the optimistic approach, two components are compatible if there is some environment that can make them work together. According to the alternating approach, one interface refines another if it has weaker input assumptions, and stronger output guarantees. We show that these notions have game-theoretic foundations that lead to efficient algorithms for checking compatibility and refinement.}, author = {De Alfaro, Luca and Henzinger, Thomas A}, booktitle = {Proceedings of the 8th European software engineering conference}, isbn = {9781581133905}, location = {Vienna, Austria}, pages = {109 -- 120}, publisher = {ACM}, title = {{Interface automata}}, doi = {10.1145/503209.503226}, year = {2001}, } @inproceedings{4623, abstract = {We classify component-based models of computation into component models and interface models. A component model specifies for each component howthe component behaves in an arbitrary environment; an interface model specifies for each component what the component expects from the environment. Component models support compositional abstraction, and therefore component-based verification. Interface models support compositional refinement, and therefore componentbased design. Many aspects of interface models, such as compatibility and refinement checking between interfaces, are properly viewed in a gametheoretic setting, where the input and output values of an interface are chosen by different players.}, author = {De Alfaro, Luca and Henzinger, Thomas A}, booktitle = {Proceedings of the 1st International Workshop on Embedded Software}, isbn = {9783540426738}, location = {Tahoe City, CA, USA}, pages = {148 -- 165}, publisher = {ACM}, title = {{Interface theories for component-based design}}, doi = {10.1007/3-540-45449-7_11}, volume = {2211}, year = {2001}, } @inproceedings{4564, abstract = {This paper presents a concept for integrating the embedded programming methodology Giotto and the object-oriented AOCS Framework to create an environment for the rapid development of distributed software for safety-critical embedded control systems with hard real-time requirements of the kind typically found in aerospace applications.}, author = {Brown, Timothy and Pasetti, Alessandro and Pree, Wolfgang and Henzinger, Thomas A and Kirsch, Christoph}, booktitle = {Proceedings of the 20th Digital Avionics Systems Conference}, isbn = {0780370341}, location = {Daytona Beach, FL, USA}, pages = {1 -- 11}, publisher = {IEEE}, title = {{A reusable and platform-independent framework for distributed control systems}}, doi = {10.1109/DASC.2001.964169}, year = {2001}, } @inproceedings{4477, abstract = {The assume-guarantee paradigm is a powerful divide-and-conquer mechanism for decomposing a verification task about a system into subtasks about the individual components of the system. The key to assume-guarantee reasoning is to consider each component not in isolation, but in conjunction with assumptions about the context of the component. Assume-guarantee principles are known for purely concurrent contexts, which constrain the input data of a component, as well as for purely sequential contexts, which constrain the entry configurations of a component. We present a model for hierarchical system design which permits the arbitrary nesting of parallel as well as serial composition, and which supports an assume-guarantee principle for mixed parallel-serial contexts. Our model also supports both discrete and continuous processes, and is therefore well-suited for the modeling and analysis of embedded software systems which interact with real-world environments. Using an example of two cooperating robots, we show refinement between a high-level model which specifies continuous timing constraints and an implementation which relies on discrete sampling.}, author = {Henzinger, Thomas A and Minea, Marius and Prabhu, Vinayak}, booktitle = {Proceedings of the 4th International Workshop on Hybrid Systems}, isbn = {9783540418665}, location = {Rome, Italy}, pages = {275 -- 290}, publisher = {Springer}, title = {{Assume-guarantee reasoning for hierarchical hybrid systems}}, doi = {10.1007/3-540-45351-2_24}, volume = {2034}, year = {2001}, } @inproceedings{4478, abstract = {Giotto is a principled, tool-supported design methodology for implementing embedded control systems on platforms of possibly distributed sensors, actuators, CPUs, and networks. Giotto is based on the principle that time-triggered task invocations plus time-triggered mode switches can form the abstract essence of programming real-time control systems. Giotto consists of a programming language with a formal semantics, and a retargetable compiler and runtime library. Giotto supports the automation of control system design by strictly separating platform-independent functionality and timing concerns from platform-dependent scheduling and communication issues. The time-triggered predictability of Giotto makes it particularly suitable for safety-critical applications with hard real-time constraints. We illustrate the platform-independence and time-triggered execution of Giotto by coordinating a heterogeneous flock of Intel x86 robots and Lego Mindstorms robots.}, author = {Henzinger, Thomas A and Horowitz, Benjamin and Kirsch, Christoph}, booktitle = {Proceedings of the 2nd ACM SIGPLAN workshop on Languages, compilers and tools for embedded systems}, isbn = {9781581134254}, location = {New York, NY, United States}, pages = {64 -- 72}, publisher = {ACM}, title = {{Embedded control systems development with Giotto}}, doi = {10.1145/384197.384208}, year = {2001}, } @inproceedings{4479, abstract = {Giotto provides an abstract programmer’s model for the implementation of embedded control systems with hard real-time constraints. A typical control application consists of periodic software tasks together with a mode switching logic for enabling and disabling tasks. Giotto specifies time-triggered sensor readings, task invocations, and mode switches independent of any implementation platform. Giotto can be annotated with platform constraints such as task-to-host mappings, and task and communication schedules. The annotations are directives for the Giotto compiler, but they do not alter the functionality and timing of a Giotto program. By separating the platform-independent from the platform-dependent concerns, Giotto enables a great deal of flexibility in choosing control platforms as well as a great deal of automation in the validation and synthesis of control software. The time-triggered nature of Giotto achieves timing predictability, which makes Giotto particularly suitable for safety-critical applications.}, author = {Henzinger, Thomas A and Horowitz, Benjamin and Kirsch, Christoph}, booktitle = {Proceedings of the 1st International Workshop on Embedded Software}, isbn = {9783540426738}, location = {Tahoe City, CA, USA}, pages = {166 -- 184}, publisher = {ACM}, title = {{Giotto: A time-triggered language for embedded programming}}, doi = {10.1007/3-540-45449-7_12}, volume = {2211}, year = {2001}, } @inproceedings{4475, abstract = {We provide an overview of the current status of HYTECH, and reflect on some of the lessons learned from our experiences with the tool. HYTECH is a symbolic model checker for mixed discrete-continuous systems that are modeled as automata with piecewise-constant polyhedral differential inclusions. The use of a formal input language and automated procedures for state-space traversal lay the foundation for formally verifying properties of hybrid dynamical systems. We describe some recent experiences analyzing three hybrid systems. We point out the successes and limitations of the tool. The analysis procedure has been extended in a number of ways to address some of the tool's shortcomings. We evaluate these extensions, and conclude with some desiderata for verification tools for hybrid systems.}, author = {Henzinger, Thomas A and Preussig, Joerg and Wong Toi, Howard}, booktitle = {Proceedings of the 40th IEEE Conference on Decision and Control}, isbn = {0780370619}, location = {Orlando, FL, USA}, pages = {2887 -- 2892}, publisher = {IEEE}, title = {{Some lessons from the HYTECH experience}}, doi = {10.1109/.2001.980714}, volume = {3}, year = {2001}, } @proceedings{4449, abstract = {Embedded software is software that interacts with physical processes. As em- bedded systems increasingly permeate our daily lives on all levels, from micros- copic devices to international networks, the cost-efficient development of reliable embedded software is one of the grand challenges in computer science today. The purpose of the workshop is to bring together researchers in all areas of computer science that are traditionally distinct but relevant to embedded software develop- ment, and to incubate a research community in this way. The workshop aims to cover all aspects of the design and implementation of embedded software, inclu- ding operating systems and middleware, programming languages and compilers, modeling and validation, software engineering and programming methodologies, scheduling and execution time analysis, networking and fault tolerance, as well as application areas, such as embedded control, real-time signal processing, and telecommunications.}, editor = {Henzinger, Thomas A}, isbn = {9783540426738}, location = {Tahoe City, CA, USA}, publisher = {ACM}, title = {{EMSOFT: Embedded Software}}, doi = {10.1007/3-540-45449-7}, volume = {2211}, year = {2001}, } @inbook{4278, abstract = {The ability of species to migrate that has interested ecologists for many years. Now that so many species and ecosystems face major environmental change, the ability of species to adapt to these changes by dispersing, migrating, or moving between different patches of habitat can be crucial to ensuring their survivial. This book provides a timely and wide-ranging overview of the study of dispersal and incorporates much of the latest research. The causes, mechanisms, and consequences of dispersal at the individual, population, species and community levels are considered. The potential of new techniques and models for studying dispersal, drawn from molecular biology and demography, is also explored. Perspectives and insights are offered from the fields of evolution, conservation biology and genetics. Throughout the book, theoretical approaches are combined with empirical data, and care has been taken to include examples from as wide a range of species as possible. }, author = {Barton, Nicholas H}, booktitle = {Dispersal}, isbn = {9780198506591}, publisher = {Oxford University Press}, title = {{The evolutionary consequences of gene flow and local adaptation: Future approaches}}, year = {2001}, } @article{4200, abstract = {Zebrafish embryos homozygous for the masterblind (mb1) mutation exhibit a striking phenotype in which the eyes and telencephalon are reduced or absent and diencephalic fates expand to the front of the brain. Here we show that mb1(-/-) embryos carry an amino-acid change at a conserved site in the Wnt pathway scaffolding protein, Axin1. The amino-acid substitution present in the mbl allele abolishes the binding of Axin to Gsk3 and affects Tcf-dependent transcription. Therefore, Gsk3 activity may be decreased in mbl(-/-) embryos and in support of this possibility, overexpression of either wild-type Axin1 or Gsk3 beta can restore eye and telencephalic fates to mb1(-/-) embryos. Our data reveal a crucial role for Axin1-dependent inhibition of the Wnt pathway in the early regional subdivision of the anterior neural plate into telencephalic, diencephalic, and eye-forming territories.}, author = {Heisenberg, Carl-Philipp J and Houart, Corinne and Take Uchi, Masaya and Rauch, Gerd and Young, Neville and Coutinho, Pedro and Masai, Ichiro and Caneparo, Luca and Concha, Miguel and Geisler, Robert and Dale, Trevor and Wilson, Stephen and Stemple, Derek}, issn = {0890-9369}, journal = {Genes and Development}, number = {11}, pages = {1427 -- 1434}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{A mutation in the Gsk3-binding domain of zebrafish Masterblind/Axin1 leads to a fate transformation of telencephalon and eyes to diencephalon}}, doi = {10.1101/gad.194301}, volume = {15}, year = {2001}, } @article{4266, abstract = {Hybridization may influence evolution in a variety of ways. If hybrids are less fit, the geographical range of ecologically divergent populations may be limited, and prezygotic reproductive isolation may be reinforced. If some hybrid genotypes are fitter than one or both parents, at least in some environments, then hybridization could make a positive contribution. Single alleles that are at an advantage in the alternative environment and genetic background will introgress readily, although such introgression may be hard to detect. 'Hybrid speciation', in which fit combinations of alleles are established, is more problematic; its likelihood depends on how divergent populations meet, and on the structure of epistasis. These issues are illustrated using Fisher's model of stabilizing selection on multiple traits, under which reproductive isolation evolves as a side-effect of adaptation in allopatry. This confirms a priori arguments that while recombinant hybrids are less fit on average, some gene combinations may be fitter than the parents, even in the parental environment. Fisher's model does predict heterosis in diploid F1s, asymmetric incompatibility in reciprocal backcrosses, and (when dominance is included) Haldane's Rule. However, heterosis arises only when traits are additive, whereas the latter two patterns require dominance. Moreover, because adaptation is via substitutions of small effect, Fisher's model does not generate the strong effects of single chromosome regions often observed in species crosses.}, author = {Barton, Nicholas H}, issn = {962-1083}, journal = {Molecular Ecology}, number = {3}, pages = {551 -- 568}, publisher = {Wiley-Blackwell}, title = {{The role of hybridization in evolution}}, doi = {10.1046/j.1365-294X.2001.01216.x}, volume = {10}, year = {2001}, } @article{4265, abstract = {The reasons that sex and recombination are so widespread remain elusive. One popular hypothesis is that sex and recombination promote adaptation to a changing environment. The strongest evidence that increased recombination may evolve because recombination promotes adaptation comes from artificially selected populations. Recombination rates have been found to increase as a correlated response to selection on traits unrelated to recombination in several artificial selection experiments and in a comparison of domesticated and nondomesticated mammals. There are, however, several alternative explanations for the increase in recombination in such populations, including two different evolutionary explanations. The first is that the form of selection is epistatic, generating linkage disequilibria among selected loci, which can indirectly favor modifier alleles that increase recombination. The second is that random genetic drift in selected populations tends to generate disequilibria such that beneficial alleles are often found in different individuals; modifier alleles that increase recombination can bring together such favorable alleles and thus may be found in individuals with greater fitness. In this paper, we compare the evolutionary forces acting on recombination in finite populations subject to strong selection, To our surprise, we found that drift accounted for the majority of selection for increased recombination observed in simulations of small to moderately large populations, suggesting that, unless selected populations are large, epistasis plays a secondary role in the evolution of recombination.}, author = {Otto, Sarah and Barton, Nicholas H}, issn = {0014-3820}, journal = {Evolution; International Journal of Organic Evolution}, number = {10}, pages = {1921 -- 1931}, publisher = {Wiley-Blackwell}, title = {{Selection for recombination in small populations}}, doi = {10.1111/j.0014-3820.2001.tb01310.x}, volume = {55}, year = {2001}, } @article{4229, abstract = {Bacteriophage of the family Leviviridae have played an important role in molecular biology where representative species, such as Qβ and MS2, have been studied as model systems for replication, translation, and the role of secondary structure in gene regulation. Using nucleotide sequences from the coat and replicase genes we present the first statistical estimate of phylogeny for the family Leviviridae using maximum-likelihood and Bayesian estimation. Our analyses reveal that the coliphage species are a monophyletic group consisting of two clades representing the genera Levivirus and Allolevivirus. The Pseudomonas species PP7 diverged from its common ancestor with the coliphage prior to the ancient split between these genera and their subsequent diversification. Differences in genome size, gene composition, and gene expression are shown with a high probability to have changed along the lineage leading to the Allolevivirus through gene expansion. The change in genome size of the Allolevivirus ancestor may have catalyzed subsequent changes that led to their current genome organization and gene expression.}, author = {Bollback, Jonathan P and Huelsenbeck, John}, issn = {0022-2844}, journal = {Journal of Molecular Evolution}, number = {2}, pages = {117 -- 128}, publisher = {Springer}, title = {{Phylogeny, genome evolution, and host specificity of single-stranded RNA bacteriophage (Family Leviviridae)}}, doi = {10.1007/s002390010140}, volume = {52}, year = {2001}, } @article{4264, abstract = {The study of speciation has become one of the most active areas of evolutionary biology, and substantial progress has been made in documenting and understanding phenomena ranging from sympatric speciation and reinforcement to the evolutionary genetics of postzygotic isolation. This progress has been driven largely by empirical results, and most useful theoretical work has concentrated on making sense of empirical patterns. Given the complexity of speciation, mathematical theory is subordinate to verbal theory and generalizations about data. Nevertheless, mathematical theory can provide a useful classification of verbal theories; can help determine the biological plausibility of verbal theories; can determine whether alternative mechanisms of speciation are consistent with empirical patterns; and can occasionally provide predictions that go beyond empirical generalizations. We discuss recent examples of progress in each of these areas.}, author = {Turelli, Michael and Barton, Nicholas H and Coyne, Jerry}, issn = {0169-5347}, journal = {Trends in Ecology and Evolution}, number = {7}, pages = {330 -- 343}, publisher = {Cell Press}, title = {{Theory and speciation}}, doi = {10.1016/S0169-5347(01)02177-2}, volume = {16}, year = {2001}, } @inbook{4267, abstract = {The flow of genes from the dense and well-adapted centre of a species' distribution interferes with adaptation to marginal environments, and may sharply limit a species' range. Deterministic models of a linear habitat suggest that populations could in principle adapt to very steep environmental gradients, by increasing their genetic variability. However, random fluctuations in sparse populations reduce this variance, and may be crucial in limiting the species' range.}, author = {Barton, Nicholas H}, booktitle = {Integrating ecology and evolution in a spatial context}, isbn = {9780521840002}, pages = {365 -- 392}, publisher = {Cambridge University Press}, title = {{Adaptation at the edge of a species' range}}, year = {2001}, } @article{4002, abstract = {Shape deformation refers to the continuous change of one geometric object to another. We develop a software tool for planning, analyzing and visualizing deformations between two shapes in R-2. The deformation is generated automatically without any user intervention or specification of feature correspondences. A unique property of the tool is the explicit availability of a two-dimensional shape space, which can be used for designing the deformation either automatically by following constraints and objectives or manually by drawing deformation paths.}, author = {Cheng, Siu and Edelsbrunner, Herbert and Fu, Ping and Lam, Ka}, issn = {0925-7721}, journal = {Computational Geometry: Theory and Applications}, number = {2-3}, pages = {205 -- 218}, publisher = {Elsevier}, title = {{Design and analysis of planar shape deformation}}, doi = {10.1016/S0925-7721(01)00020-7}, volume = {19}, year = {2001}, } @article{4001, abstract = {The construction of shape spaces is studied from a mathematical and a computational viewpoint. A program is outlined reducing the problem to four tasks: the representation of geometry, the canonical deformation of geometry, the measuring of distance in shape space, and the selection of base shapes. The technical part of this paper focuses on the second task: the specification of a deformation mixing two or more shapes in continuously changing proportions. (C) 2001 Elsevier Science B.V All rights reserved.}, author = {Cheng, Ho and Edelsbrunner, Herbert and Fu, Ping}, issn = {0925-7721}, journal = {Computational Geometry: Theory and Applications}, number = {2-3}, pages = {191 -- 204}, publisher = {Elsevier}, title = {{Shape space from deformation}}, doi = {10.1016/S0925-7721(01)00021-9}, volume = {19}, year = {2001}, } @inproceedings{4005, abstract = {This paper describes an algorithm for maintaining an approximating triangulation of a deforming surface in R-3. The triangulation adapts dynamically to changing shape, curvature, and topology of the surface.}, author = {Cheng, Ho and Dey, Tamal and Edelsbrunner, Herbert and Sullivan, John}, booktitle = {Proceedings of the 12th annual ACM-SIAM symposium on Discrete algorithms}, isbn = {9780898714906}, location = {Washington, DC, USA }, pages = {47 -- 56}, publisher = {SIAM}, title = {{Dynamic skin triangulation}}, year = {2001}, } @article{4007, abstract = {This paper describes an algorithm for maintaining an approximating triangulation of a deforming surface in R 3 . The surface is the envelope of an infinite family of spheres defined and controlled by a finite collection of weighted points. The triangulation adapts dynamically to changing shape, curvature, and topology of the surface. }, author = {Cheng, Ho and Dey, Tamal and Edelsbrunner, Herbert and Sullivan, John}, issn = {0179-5376}, journal = {Discrete & Computational Geometry}, number = {4}, pages = {525 -- 568}, publisher = {Springer}, title = {{Dynamic skin triangulation}}, doi = {10.1007/s00454-001-0007-1}, volume = {25}, year = {2001}, } @article{4006, abstract = {The 180 models collected in this paper are produced by sampling and wrapping point sets on tubes. The surfaces are represented as triangulated 2-manifolds and available as st1-files from the author's web site at www.cs.duke.edu/similar toedels. Each tube is obtained by thickening a circle or a smooth torus knot, and for some we use the degrees of freedom in the thickening process to encode meaningful information, such as curvature or torsion.}, author = {Edelsbrunner, Herbert}, issn = {0948-695X}, journal = {Journal of Universal Computer Science}, number = {5}, pages = {379 -- 399}, publisher = {Springer}, title = {{180 wrapped tubes}}, doi = {10.3217/jucs-007-05-0379}, volume = {7}, year = {2001}, } @article{3928, abstract = {Regulated adhesion of leukocytes to the extracellular matrix is essential for transmigration of blood vessels and subsequent migration into the stroma of inflamed tissues. Although beta(2)-integrins play an indisputable role in adhesion of polymorphonuclear granulocytes (PMN) to endothelium, we show here that beta(1)- and beta(3)-integrins but not beta(2)-integrin are essential for the adhesion to and migration on extracellular matrix molecules of the endothelial cell basement membrane and subjacent interstitial matrix. Mouse wild type and beta(2)-integrin null PMN and the progranulocytic cell line 32DC13 were employed in in vitro adhesion and migration assays using extracellular matrix molecules expressed at sites of extravasation in vivo, in particular the endothelial cell laminins 8 and 10. Wild type and beta(2)-integrin null PMN showed the same pattern of ECM binding, indicating that beta(2)-integrins do not mediate specific adhesion of PMN to the extracellular matrix molecules tested; binding was observed to the interstitial matrix molecules, fibronectin and vitronectin, via integrins alpha(5)beta(1) and alpha(v)beta(3), respectively; to laminin 10 via alpha(6)beta(1); but not to laminins 1, 2, and 8, collagen type I and IV, perlecan, or tenascin-C. PMN binding to laminins 1, 2, and 8 could not be induced despite surface expression of functionally active integrin alpha(6)beta(1), a major laminin receptor, demonstrating that expression of alpha(6)beta(1) alone is insufficient for ligand binding and suggesting the involvement of accessory factors. Nevertheless, laminins 1, 8, and 10 supported PMN migration, indicating that differential cellular signaling via laminins is independent of the extent of adhesion. The data demonstrate that adhesive and nonadhesive interactions with components of the endothelial cell basement membrane and subjacent interstitium play decisive roles in controlling PMN movement into sites of inflammation and illustrate that beta(2)-integrins are not essential for such interactions.}, author = {Sixt, Michael K and Hallmann, Rupert and Wendler, Olaf and Scharffetter Kochanek, Karin and Sorokin, Lydia}, issn = {0021-9258}, journal = {Journal of Biological Chemistry}, number = {22}, pages = {18878 -- 18887}, publisher = {American Society for Biochemistry and Molecular Biology}, title = {{Cell adhesion and migration properties of β2-integrin negative polymorphonuclear granulocytes on defined extracellular matrix molecules. Relevance for leukocyte extravasation}}, doi = {10.1074/jbc.M010898200}, volume = {276}, year = {2001}, } @article{3927, abstract = {TNF-alpha has been clearly identified as central mediator of T cell activation-induced acute hepatic injury in mice, e.g., Con A hepatitis. In this model, liver injury depends on both TNFRs, i.e., the 55-kDa TNFR1 as well as the 75-kDa TNFR2. We show in this report that the hepatic TNFRs are not transcriptionally regulated, but are regulated by receptor shedding. TNF directly mediates hepatocellular death by activation of TNFR1 but also induces the expression of inflammatory proteins, such as cytokines and adhesion molecules. Here we provide evidence that resistance of TNFR1(-/-) and TNFR2(-/-) mice against Con A hepatitis is not due to an impaired production of the central mediators TNF and IFN-gamma. Con A injection results in a massive induction of ICAM-1, VCAM-1, and E-selectin in the liver. Lack of either one of both TNFRs did not change adhesion molecule expression in the livers of Con A-treated mice, presumably reflecting the fact that other endothelial cell-activating cytokines up-regulated adhesion molecule expression. However, treatment of TNFR1(-/-) and TNFR2(-/-) mice with murine rTNF revealed a predominant role for TNFR1 for the induction of hepatic adhesion molecule expression. Pretreatment with blocking Abs against E- and P-selectin or of ICAM(-/-) mice with anti-VCAM-1 Abs failed to prevent Con A hepatitis, although accumulation of the critical cell population, i.e., CD4(+) T cells was significantly inhibited. Hence, up-regulation of adhesion molecules during acute hepatitis unlikely contributes to organ injury but rather represents a defense mechanism.}, author = {Wolf, Dominik and Hallmann, Rupert and Sass, Gabriele and Sixt, Michael K and Küsters, Sabine and Fregien, Bastian and Trautwein, Christian and Tiegs, Gisa}, issn = {0022-1767}, journal = {Journal of Immunology}, number = {2}, pages = {1300 -- 1307}, publisher = {American Association of Immunologists}, title = {{TNF-α-induced expression of adhesion molecules in the liver is under the control of TNFR1--relevance for concanavalin A-induced hepatitis}}, doi = {10.4049/jimmunol.166.2.1300}, volume = {166}, year = {2001}, } @article{3930, abstract = {An active involvement of blood-brain barrier endothelial cell basement membranes in development of inflammatory lesions in the central nervous system (CNS) has not been considered to date. Here we investigated the molecular composition and possible function of the extracellular matrix encountered by extravasating T lymphocytes during experimental autoimmune encephalomyelitis (EAE). Endothelial basement membranes contained laminin 8 (alpha4beta1gamma1) and/or 10 (alpha5beta1gamma1) and their expression was influenced by proinflammatory cytokines or angiostatic agents. T cells emigrating into the CNS during EAE encountered two biochemically distinct basement membranes, the endothelial (containing laminins 8 and 10) and the parenchymal (containing laminins 1 and 2) basement membranes. However, inflammatory cuffs occurred exclusively around endothelial basement membranes containing laminin 8, whereas in the presence of laminin 10 no infiltration was detectable. In vitro assays using encephalitogenic T cell lines revealed adhesion to laminins 8 and 10, whereas binding to laminins 1 and 2 could not be induced. Downregulation of integrin alpha6 on cerebral endothelium at sites of T cell infiltration, plus a high turnover of laminin 8 at these sites, suggested two possible roles for laminin 8 in the endothelial basement membrane: one at the level of the endothelial cells resulting in reduced adhesion and, thereby, increased penetrability of the monolayer; and secondly at the level of the T cells providing direct signals to the transmigrating cells.}, author = {Sixt, Michael K and Engelhardt, Britta and Pausch, Friederike and Hallmann, Rupert and Wendler, Olaf and Sorokin, Lydia}, issn = {0021-9525}, journal = {Journal of Cell Biology}, number = {5}, pages = {933 -- 946}, publisher = {Rockefeller University Press}, title = {{Endothelial cell laminin isoforms, laminins 8 and 10, play decisive roles in T cell recruitment across the blood-brain barrier in experimental autoimmune encephalomyelitis}}, doi = {10.1083/jcb.153.5.933 }, volume = {153}, year = {2001}, } @article{3622, abstract = {The extent of genetic variation in fitness and its components and genetic variation's dependence on environmental conditions remain key issues in evolutionary biology. We present measurements of genetic variation in preadult viability in a laboratory-adapted population of Drosophila melanogaster, made at four different densities. By crossing flies heterozygous for a wild-type chromosome and one of two different balancers (TM1, TM2), we measure both heterozygous (TM1/+, TM2/+) and homozygous (+/+) viability relative to a standard genotype (TM1/TM2). Forty wild-type chromosomes were tested, of which 10 were chosen to be homozygous viable. The mean numbers produced varied significantly between chromosome lines, with an estimated between-line variance in loge numbers of 0.013. Relative viabilities also varied significantly across chromosome lines, with a variance in loge homozygous viability of 1.76 and of loge heterozygous viability of 0.165. The between-line variance for numbers emerging increased with density, from 0.009 at lowest density to 0.079 at highest. The genetic variance in relative viability increases with density, but not significantly. Overall, the effects of different chromosomes on relative viability were remarkably consistent across densities and across the two heterozygous genotypes (TM1, TM2). The 10 lines that carried homozygous viable wild-type chromosomes produced significantly more adults than the 30 lethal lines at low density and significantly fewer adults at the highest density. Similarly, there was a positive correlation between heterozygous viability and mean numbers at low density, but a negative correlation at high density.}, author = {Gardner, Michael and Fowler, Kevin and Patridge, Linda and Barton, Nicholas H}, issn = {0014-3820}, journal = {Evolution}, number = {8}, pages = {1609 -- 1620}, publisher = {Wiley-Blackwell}, title = {{Genetic variation for preadult viability in Drosophila melanogaster}}, doi = {10.1111/j.0014-3820.2001.tb00680.x}, volume = {55}, year = {2001}, } @misc{3596, author = {Barton, Nicholas H}, booktitle = {Trends in Genetics}, issn = {0168-9479}, pages = {420 -- 420}, publisher = {Elsevier}, title = {{Mendel and mathematics}}, doi = {10.1016/S0168-9525(01)02315-0}, volume = {17}, year = {2001}, } @article{3546, abstract = {Local versus distant coherence of hippocampal CA1 pyramidal cells was investigated in the behaving rat. Temporal cross-correlation of pyramidal cells revealed a significantly stronger relationship among local (<140 <mu>m) pyramidal neurons compared with distant (>300 mum) neurons during non-theta-associated immobility and sleep but not during theta-associated running and walking. In contrast, cross-correlation between local pyramidal cell-interneuron pairs was significantly stronger than between distant pairs during theta oscillations but were similar during non-theta-associated behaviors. We suggest that network state-dependent functional clustering of neuronal activity emerges because of the differential contribution of the main excitatory inputs, the perforant path, and Schaffer collaterals during theta and non-theta behaviors.}, author = {Hirase, Hajima and Leinekugel, Xavier and Csicsvari, Jozsef L and Czurkó, András and Buzsáki, György}, issn = {0270-6474}, journal = {Journal of Neuroscience}, number = {10}, publisher = {Society for Neuroscience}, title = {{Behavior-dependent states of the hippocampal network affect functional clustering of neurons}}, doi = {10.1523/JNEUROSCI.21-10-j0003.2001}, volume = {21}, year = {2001}, } @article{3540, abstract = {What determines the firing rate of cortical neurons in the absence of external sensory input or motor behavior, such as during sleep? Hero we report that, in a familiar environment, the discharge frequency of simultaneously recorded individual CA1 pyramidal neurons and the coactivation of cell pairs remain highly correlated across sleep-wake-steep sequences. However, both measures were affected when new sets of neurons were activated in a novel environment. Nevertheless, the grand mean firing rate of the whole pyramidal cell population remained constant across behavioral states and testing conditions. The findings suggest that long-term firing patterns of single cells can be modified by experience. We hypothesize that increased firing rates of recently used neurons are associated with a concomitant decrease in the discharge activity of the remaining population, leaving the mean excitability of the hippocampal network unaltered.}, author = {Hirase, Hajima and Leinekugel, Xavier and Czurkó, András and Csicsvari, Jozsef L and Buzsáki, György}, issn = {0027-8424}, journal = {PNAS}, number = {16}, pages = {9386 -- 9390}, publisher = {National Academy of Sciences}, title = {{Firing rates of hippocampal neurons are preserved during subsequent sleep episodes and modified by novel awake experience}}, doi = {10.1073/pnas.161274398}, volume = {98}, year = {2001}, } @article{3494, abstract = {Mutual synaptic interactions between GABAergic interneurons are thought to be of critical importance for the generation of network oscillations and for temporal encoding of information in the hippocampus. However, the functional properties of synaptic transmission between hippocampal interneurons are largely unknown. We have made paired recordings from basket cells (BCs) in the dentate gyrus of rat hippocampal slices, followed by correlated light and electron microscopical analysis. Unitary GABAAreceptor-mediated IPSCs at BC–BC synapses recorded at the soma showed a fast rise and decay, with a mean decay time constant of 2.5 ± 0.2 msec (32°C). Synaptic transmission at BC–BC synapses showed paired-pulse depression (PPD) (32 ± 5% for 10 msec interpulse intervals) and multiple-pulse depression during repetitive stimulation. Detailed passive cable model simulations based on somatodendritic morphology and localization of synaptic contacts further indicated that the conductance change at the postsynaptic site was even faster, decaying with a mean time constant of 1.8 ± 0.6 msec. Sequential triple recordings revealed that the decay time course of IPSCs at BC–BC synapses was approximately twofold faster than that at BC–granule cell synapses, whereas the extent of PPD was comparable. To examine the consequences of the fast postsynaptic conductance change for the generation of oscillatory activity, we developed a computational model of an interneuron network. The model showed robust oscillations at frequencies >60 Hz if the excitatory drive was sufficiently large. Thus the fast conductance change at interneuron–interneuron synapses may promote the generation of high-frequency oscillations observed in the dentate gyrusin vivo. }, author = {Bartos, Marlene and Vida, Imre and Frotscher, Michael and Geiger, Jörg and Jonas, Peter M}, issn = {0270-6474}, journal = {Journal of Neuroscience}, number = {8}, pages = {2687 -- 2698}, publisher = {Society for Neuroscience}, title = {{Rapid signaling at inhibitory synapses in a dentate gyrus interneuron network.}}, doi = {10.1523/JNEUROSCI.21-08-02687.2001}, volume = {21}, year = {2001}, } @article{3496, abstract = {The mossy fiber-CA3 pyramidal neuron synapse is a main component of the hippocampal trisynaptic circuitry. Recent studies, however, suggested that inhibitory interneurons are the major targets of the mossy fiber system. To study the regulation of mossy fiber-interneuron excitation, we examined unitary and compound excitatory postsynaptic currents in dentate gyrus basket cells, evoked by paired recording between granule and basket cells or extracellular stimulation of mossy fiber collaterals. The application of an associative high-frequency stimulation paradigm induced posttetanic potentiation (PTP) followed by homosynaptic long-term potentiation (LTP). Analysis of numbers of failures, coefficient of variation, and paired-pulse modulation indicated that both PTP and LTP were expressed presynaptically. The Ca2+ chelator 1,2-bis(2-aminophenoxy)ethane-N,N,N′,N′-tetraacetic acid (BAPTA) did not affect PTP or LTP at a concentration of 10 mM but attenuated LTP at a concentration of 30 mM. Both forskolin, an adenylyl cyclase activator, and phorbolester diacetate, a protein kinase C stimulator, lead to a long-lasting increase in excitatory postsynaptic current amplitude. H-89, a protein kinase A inhibitor, and bisindolylmaleimide, a protein kinase C antagonist, reduced PTP, whereas only bisindolylmaleimide reduced LTP. These results may suggest a differential contribution of protein kinase A and C pathways to mossy fiber-interneuron plasticity. Interneuron PTP and LTP may provide mechanisms to maintain the balance between synaptic excitation of interneurons and that of principal neurons in the dentate gyrus-CA3 network. }, author = {Alle, Henrik and Jonas, Peter M and Geiger, Jörg}, issn = {0027-8424}, journal = {PNAS}, number = {25}, pages = {14708 -- 14713}, publisher = {National Academy of Sciences}, title = {{PTP and LTP at a hippocampal mossy fiber-interneuron synapse}}, doi = {10.1073/pnas.251610898 }, volume = {98}, year = {2001}, } @article{3495, abstract = {High Ca2+ permeability and its control by voltage-dependent Mg2+ block are defining features of NMDA receptors. These features are lost if the principal NR1 subunit carries an asparagine (N) to arginine (R) substitution in a critical channel site at NR1 position 598. NR1(R) expression from a single allele in gene-targeted NR1+/R mice is lethal soon after birth, precluding analysis of altered synaptic functions later in life. We therefore employed the forebrain specific αCaMKII promoter to drive tTA-mediated tetracyclin sensitive transcription of transgenes for NR1(R) and for lacZ as reporter. Transgene expression was observed in cortex, striatum, hippocampus, amygdala and olfactory bulb and was mosaic in all these forebrain regions. It was highest in olfactory bulb granule cells, in most of which Ca2+ permeability and voltage-dependent Mg2+ block of NMDA receptors were reduced to different extents. This indicates significant impairment of NMDA receptor function by NR1(R) in presence of the wild-type NR1 complement. Indeed, even though NR1(R) mRNA constituted only 18% of the entire NR1 mRNA population in forebrain, the transgenic mice died during adolescence unless transgene expression was suppressed by doxycycline. Thus, glutamate receptor function can be altered in the mouse by regulated NR1(R) transgene expression.}, author = {Jerecic, Jasna and Schulze, Christian and Jonas, Peter M and Sprengel, Rolf and Seeburg, Peter and Bischofberger, Joseph}, issn = {0169-328X}, journal = {Molecular Brain Research}, number = {1-2}, pages = {96 -- 104}, publisher = {Elsevier}, title = {{Impaired NMDA receptor function in mouse olfactory bulb neurons by tetracycline-sensitive NR1 (N598R) expression}}, doi = {10.1016/S0169-328X(01)00221-2}, volume = {94}, year = {2001}, } @article{3517, abstract = {A modular multichannel microdrive ('hyperdrive') is described. The microdrive uses printed circuit board technology and flexible fused silica capillaries. The modular design allows for the fabrication of 4-32 independently movable electrodes or `tetrodes'. The drives are re-usable and re-loading the drive with electrodes is simple. }, author = {Szabo, Imre and Czurkó, András and Csicsvari, Jozsef L and Hirase, Hajima and Leinekugel, Xavier and Buzsáki, György}, issn = {0165-0270}, journal = {Journal of Neuroscience Methods}, number = {1}, pages = {105 -- 110}, publisher = {Elsevier}, title = {{The application of printed circuit board technology for fabrication of multi-channel micro-drives}}, doi = {10.1016/S0165-0270(00)00362-9}, volume = {105}, year = {2001}, } @article{3493, abstract = {Although agonists and competitive antagonists presumably occupy overlapping binding sites on ligand-gated channels, these interactions cannot be identical because agonists cause channel opening whereas antagonists do not. One explanation is that only agonist binding performs enough work on the receptor to cause the conformational changes that lead to gating. This idea is supported by agonist binding rates at GABAA and nicotinic acetylcholine receptors that are slower than expected for a diffusion-limited process, suggesting that agonist binding involves an energy-requiring event. This hypothesis predicts that competitive antagonist binding should require less activation energy than agonist binding. To test this idea, we developed a novel deconvolution-based method to compare binding and unbinding kinetics of GABAA receptor agonists and antagonists in outside-out patches from rat hippocampal neurons. Agonist and antagonist unbinding rates were steeply correlated with affinity. Unlike the agonists, three of the four antagonists tested had binding rates that were fast, independent of affinity, and could be accounted for by diffusion- and dehydration-limited processes. In contrast, agonist binding involved additional energy-requiring steps, consistent with the idea that channel gating is initiated by agonist-triggered movements within the ligand binding site. Antagonist binding does not appear to produce such movements, and may in fact prevent them.}, author = {Jones, M.V and Jonas, Peter M and Sahara, Y. and Westbrook, G.}, issn = {0006-3495}, journal = {Biophysical Journal}, number = {5}, pages = {2660 -- 2670}, publisher = {Biophysical Society}, title = {{Microscopic kinetics and energetics distinguish GABAA receptor agonists from antagonists}}, doi = {10.1016/S0006-3495(01)75909-7 }, volume = {81}, year = {2001}, } @article{2985, abstract = {The elimination voltammetry with linear scan (EVLS) was used to study adenine and cytosine reduction signals at the mercury electrode. In comparison with the linear scan voltammetry (which provides only one unresolved peak), two elimination functions provide good resolution of individual peaks and significant increase of sensitivity. The first elimination function eliminates the kinetic current (Ik) and conserves the diffusion current (Id). The second elimination function eliminates kinetic and charging currents (Ik and Ic) simultaneously and conserves the diffusion current (Id). Both functions give two well-resolved peaks of adenine and cytosine in a wide concentration range, while the linear sweep voltammetry gives badly resolved peaks due to hydrogen evolution. The best resolution of peaks is observed in acetate buffer at pH 3.8 and the detection limit for both substances is 500 nM. The concentration dependence of EVLS peak heights for one substance at the constant concentration of the other substance is linear. The peak potentials differ in these elimination functions. The difference in EVLS peak potentials gives the possibility to evaluate αna. Elimination voltammetry with linear scan contributes to the resolution of cathodic signals of purine and pyrimidine bases at very negative potentials near supporting electrolyte discharge. Copyright © 2001 Elsevier Science B.V.}, author = {Trnková, Libuše and Friml, Jirí and Dračka, Oldřich}, isbn = {1567-5394}, journal = {Bioelectrochemistry}, number = {2}, pages = {131 -- 136}, publisher = {Elsevier}, title = {{Elimination voltammetry of adenine and cytosine mixtures}}, doi = {10.1016/S1567-5394(01)00119-0}, volume = {54}, year = {2001}, }