@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{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{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}, } @article{1452, abstract = {In this Note we present pairs of hyperkähler orbifolds which satisfy two different versions of mirror symmetry. On the one hand, we show that their Hodge numbers (or more precisely, stringy E-polynomials) are equal. On the other hand, we show that they satisfy the prescription of Strominger, Yau, and Zaslow (which in the present case goes back to Bershadsky, Johansen, Sadov and Vafa): that a Calabi-Yau and its mirror should fiber over the same real manifold, with special Lagrangian fibers which are tori dual to each other. Our examples arise as moduli spaces of local systems on a curve with structure group SL(n); the mirror is the corresponding space with structure group PGL(n). The special Lagrangian tori come from an algebraically completely integrable Hamiltonian system: the Hitchin system.}, author = {Hausel, Tamas and Thaddeus, Michael}, issn = {0764-4442}, journal = {Comptes Rendus de l'Academie des Sciences - Series I: Mathematics}, number = {4}, pages = {313 -- 318}, publisher = {Elsevier}, title = {{Examples of mirror partners arising from integrable systems}}, doi = {10.1016/S0764-4442(01)02057-2}, volume = {333}, year = {2001}, } @article{1453, abstract = {In this Letter we exhibit a one-parameter family of new Taub-NUT instantons parameterized by a half-line. The endpoint of the half-line will be the reducible Yang-Mills instanton corresponding to the Eguchi-Hanson-Gibbons L2 harmonic 2-form, while at an inner point we recover the Pope-Yuille instanton constructed as a projection of the Levi-Civitá connection onto the positive su(2)+ ⊂ so(4) subalgebra. Our method imitates the Jackiw-Nohl-Rebbi construction originally designed for flat R4. That is we find a one-parameter family of harmonic functions on the Taub-NUT space with a point singularity, rescale the metric and project the obtained Levi-Civitá connection onto the other negative su(2)- ⊂ so(4) part. Our solutions will possess the full U(2) symmetry, and thus provide more solutions to the recently proposed U(2) symmetric ansatz of Kim and Yoon.}, author = {Etesi, Gábor and Hausel, Tamas}, issn = {0370-2693}, journal = {Physics Letters, Section B: Nuclear, Elementary Particle and High-Energy Physics}, number = {1-2}, pages = {189 -- 199}, publisher = {Elsevier}, title = {{Geometric construction of new Yang-Mills instantons over Taub-NUT space}}, doi = {10.1016/S0370-2693(01)00821-8}, volume = {514}, year = {2001}, } @article{1454, abstract = {We address the problem of finding Abelian instantons of finite energy on the Euclidean Schwarzschild manifold. This amounts to construct self-dual L2 harmonic 2-forms on the space. Gibbons found a non-topological L2 harmonic form in the Taub-NUT metric, leading to Abelian instantons with continuous energy. We imitate his construction in the case of the Euclidean Schwarzschild manifold and find a non-topological self-dual L2 harmonic 2-form on it. We show how this gives rise to Abelian instantons and identify them with SU(2)-instantons of Pontryagin number 2n2 found by Charap and Duff in 1977. Using results of Dodziuk and Hitchin we also calculate the full L2 harmonic space for the Euclidean Schwarzschild manifold.}, author = {Etesi, Gábor and Hausel, Tamas}, issn = {0393-0440}, journal = {Journal of Geometry and Physics}, number = {1-2}, pages = {126 -- 136}, publisher = {Elsevier}, title = {{Geometric interpretation of Schwarzschild instantons}}, doi = {10.1016/S0393-0440(00)00040-1}, volume = {37}, 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}, } @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}, } @inbook{3434, abstract = {This chapter contains sections titled: Introduction - History - Developing an Intuition of Likelihood - Method of Maximum Likelihood - Bayesian Inference - Markov Chain Monte Carlo - Assessing Uncertainty of Phylogenies - Hypothesis Testing and Model Choice - Comparative Analysis - Conclusions - References}, author = {Huelsenbeck, John and Bollback, Jonathan P}, booktitle = {Handbook of Statistical Genetics}, editor = {Balding, David and Bishop, Martin and Cannings, Chriss}, isbn = {9781119429142 }, pages = {415 -- 439}, publisher = {Wiley-Blackwell}, title = {{Application of the likelihood function in phylogenetic analysis}}, doi = {10.1002/9780470061619.ch15}, year = {2001}, } @article{3438, abstract = {As a discipline, phylogenetics is becoming transformed by a flood of molecular data. These data allow broad questions to be asked about the history of life, but also present difficult statistical and computational problems. Bayesian inference of phylogeny brings a new perspective to a number of outstanding issues in evolutionary biology, including the analysis of large phylogenetic trees and complex evolutionary models and the detection of the footprint of natural selection in DNA sequences.}, author = {Huelsenbeck, John and Ronquist, Fredrik and Nielsen, Rasmus and Bollback, Jonathan P}, issn = {0036-8075}, journal = {Science}, number = {5550}, pages = {2310 -- 2314}, publisher = {American Association for the Advancement of Science}, title = {{Bayesian inference of phylogeny and its impact on evolutionary biology}}, doi = {10.1126/science.1065889}, volume = {294}, year = {2001}, } @article{3439, abstract = {High molecular weight DNA was extracted from the primary Neotropical malaria vector, Anopheles darlingi from Capanema, Pará, Brazil, to create a small insert genomic library, and then a phagemid library. Enriched sublibraries were constructed from the phagemid library using a microsatellite oligo primed second strand synthesis protocol. The resulting 242 760 individual clones were screened. The mean clone size of the positive clones was 302 bp. Flanking primers were designed for each suitable microsatellite sequence. Eight polymorphic loci were optimized and characterized. The allele size ranges are based on 253 samples of A. darlingi from eastern Amazonian and central Brazil.}, author = {Conn, Jan and Bollback, Jonathan P and Onyabe, David and Robinson, Tessa and Wilkerson, Richard and Povoa, Marinete}, issn = {1471-8278}, journal = {Molecular Ecology Notes}, number = {4}, pages = {223 -- 225}, publisher = {Wiley-Blackwell}, title = {{Isolation of polymorphic microsatellite markers from the malaria vector Anopheles darlingi}}, doi = { 10.1046/j.1471-8278.2001.00078.x}, volume = {1}, year = {2001}, } @article{3440, abstract = {Several methods have been proposed to infer the states at the ancestral nodes on a phylogeny. These methods assume a specific tree and set of branch lengths when estimating the ancestral character state. Inferences of the ancestral states, then, are conditioned on the tree and branch lengths being true. We develop a hierarchical Bayes method for inferring the ancestral states on a tree. The method integrates over uncertainty in the tree, branch lengths, and substitution model parameters by using Markov chain Monte Carlo. We compare the hierarchical Bayes inferences of ancestral states with inferences of ancestral states made under the assumption that a specific tree is correct. We find that the methods are correlated, but that accommodating uncertainty in parameters of the phylogenetic model can make inferences of ancestral states even more uncertain than they would be in an empirical Bayes analysis. }, author = {Huelsenbeck, John and Bollback, Jonathan P}, issn = {0039-7989}, journal = {Systematic Biology}, number = {3}, pages = {351 -- 366}, publisher = {Oxford University Press}, title = {{Empirical and hierarchical Bayesian estimation of ancestral states}}, doi = {10.1080/10635150119871}, volume = {50}, 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{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{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{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{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}, } @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}, } @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}, }