@article{4355, abstract = {When a beneficial mutation is fixed in a population that lacks recombination, the genetic background linked to that mutation is fixed. As a result, beneficial mutations on different backgrounds experience competition, or "clonal interference," that can cause asexual populations to evolve more slowly than their sexual counterparts. Factors such as a large population size (N) and high mutation rates (mu) increase the number of competing beneficial mutations, and hence are expected to increase the intensity of clonal interference. However, recent theory suggests that, with very large values of Nmu, the severity of clonal interference may instead decline. The reason is that, with large Nmu, genomes including both beneficial mutations are rapidly created by recurrent mutation, obviating the need for recombination. Here, we analyze data from experimentally evolved asexual populations of a bacteriophage and find that, in these nonrecombining populations with very large Nmu, recurrent mutation does appear to ameliorate this cost of asexuality.}, author = {Jonathan Bollback and Huelsenbeck, John P}, journal = {Molecular Biology and Evolution}, number = {6}, pages = {1397 -- 1406}, publisher = {Oxford University Press}, title = {{Clonal interference is alleviated by high mutation rates in large populations}}, doi = {10.1093/molbev/msm056}, volume = {24}, year = {2007}, } @article{4356, abstract = {We used a comparative genomics approach to identify genes that are under positive selection in six strains of Escherichia coli and Shigella flexneri, including five strains that are human pathogens. We find that positive selection targets a wide range of different functions in the E. coli genome, including cell surface proteins such as beta barrel porins, presumably because of the involvement of these genes in evolutionary arms races with other bacteria, phages, and/or the host immune system. Structural mapping of positively selected sites on trans-membrane beta barrel porins reveals that the residues under positive selection occur almost exclusively in the extracellular region of the proteins that are enriched with sites known to be targets of phages, colicins, or the host immune system. More surprisingly, we also find a number of other categories of genes that show very strong evidence for positive selection, such as the enigmatic rhs elements and transposases. Based on structural evidence, we hypothesize that the selection acting on transposases is related to the genomic conflict between transposable elements and the host genome.}, author = {Petersen, Lise and Jonathan Bollback and Dimmic, Matt and Hubisz, Melissa and Nielsen, Rasmus}, journal = {Genome Research}, number = {9}, pages = {1336 -- 1343}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{Genes under positive selection in Escherichia coli}}, doi = {10.1101/gr.6254707}, volume = {17}, year = {2007}, } @inproceedings{4368, author = {Dejan Nickovic and Maler, Oded}, pages = {304 -- 319}, publisher = {Springer}, title = {{AMT: a property-based monitoring tool for analog systems}}, doi = {1567}, year = {2007}, } @inproceedings{4370, author = {Maler, Oded and Dejan Nickovic and Pnueli,Amir}, pages = {95 -- 107}, publisher = {Springer}, title = {{On synthesizing controllers from bounded-response properties}}, doi = {1568}, year = {2007}, } @inproceedings{4394, author = {Bouillaguet,Charles and Kuncak, Viktor and Thomas Wies and Zee,Karen and Rinard,Martin C.}, pages = {74 -- 88}, publisher = {Springer}, title = {{Using First-Order Theorem Provers in the Jahob Data Structure Verification System}}, doi = {1552}, year = {2007}, } @inproceedings{4398, author = {Berdine,Josh and Calcagno,Cristiano and Cook,Byron and Distefano,Dino and O'Hearn,Peter W. and Thomas Wies and Yang,Hongseok}, pages = {178 -- 192}, publisher = {Springer}, title = {{Shape Analysis for Composite Data Structures}}, doi = {1553}, year = {2007}, } @inproceedings{4399, abstract = {A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfaces from program code: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the program to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant program variables. For comparison purposes, we present and implement the three algorithms in a unifying formal setting. While the three algorithms compute the same output and have similar worst-case complexities, their actual running times may differ considerably for a given input program. On the theoretical side, we provide for each of the three algorithms a family of input programs on which that algorithm outperforms the two alternatives. On the practical side, we evaluate the three algorithms experimentally on a variety of Java libraries. }, author = {Beyer, Dirk and Thomas Henzinger and Vasu Singh}, pages = {4 -- 19}, publisher = {Springer}, title = {{Algorithms for interface synthesis}}, doi = {10.1007/978-3-540-73368-3_4}, volume = {4590}, year = {2007}, } @inproceedings{4402, author = {Alur, Rajeev and Pavol Cerny and Chaudhuri,Swarat}, pages = {664 -- 678}, publisher = {Springer}, title = {{Model Checking on Trees with Path Equivalences}}, doi = {1544}, year = {2007}, } @article{4405, abstract = {Background A central goal of Systems Biology is to model and analyze biological signaling pathways that interact with one another to form complex networks. Here we introduce Qualitative networks, an extension of Boolean networks. With this framework, we use formal verification methods to check whether a model is consistent with the laboratory experimental observations on which it is based. If the model does not conform to the data, we suggest a revised model and the new hypotheses are tested in-silico. Results We consider networks in which elements range over a small finite domain allowing more flexibility than Boolean values, and add target functions that allow to model a rich set of behaviors. We propose a symbolic algorithm for analyzing the steady state of these networks, allowing us to scale up to a system consisting of 144 elements and state spaces of approximately 1086 states. We illustrate the usefulness of this approach through a model of the interaction between the Notch and the Wnt signaling pathways in mammalian skin, and its extensive analysis. Conclusion We introduce an approach for constructing computational models of biological systems that extends the framework of Boolean networks and uses formal verification methods for the analysis of the model. This approach can scale to multicellular models of complex pathways, and is therefore a useful tool for the analysis of complex biological systems. The hypotheses formulated during in-silico testing suggest new avenues to explore experimentally. Hence, this approach has the potential to efficiently complement experimental studies in biology.}, author = {Schaub, Marc A and Thomas Henzinger and Fisher, Jasmin}, journal = {BMC Systems Biology}, number = {4}, publisher = {BioMed Central}, title = {{Qualitative networks: A symbolic approach to analyze biological signaling networks}}, doi = {10.1186/1752-0509-1-4}, volume = {1}, year = {2007}, } @inbook{4417, abstract = {Counterexample-guided abstraction refinement (CEGAR) is a powerful technique to scale automatic program analysis techniques to large programs. However, so far it has been used primarily for model checking in the context of predicate abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract counterexample needs to be removed through abstraction refinement, there are often several choices, such as which program location(s) to refine, which abstract domain(s) to use at different locations, and which abstract values to compute. We define several plausible preference orderings on abstraction refinements, such as refining as “late” as possible and as “coarse” as possible. We present generic algorithms for finding refinements that are optimal with respect to the different preference orderings. We also compare the different orderings with respect to desirable properties, including the property if locally optimal refinements compose to a global optimum. Finally, we point out some difficulties with CEGAR for non-powerset domains.}, author = {Manevich, Roman and Field, John and Thomas Henzinger and Ramalingam, Ganesan and Sagiv, Mooly}, booktitle = {Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday}, pages = {273 -- 292}, publisher = {Springer}, title = {{Abstract counterexample-based refinement for powerset domains}}, doi = {10.1007/978-3-540-71322-7_13}, volume = {4444}, year = {2007}, } @article{4446, abstract = {The Embedded Machine is a virtual machine that mediates in real time the interaction between software processes and physical processes. It separates the compilation of embedded programs into two phases. The first phase, the platform-independent compiler phase, generates E code (code executed by the Embedded Machine), which supervises the timing, not the scheduling of, application tasks relative to external events such as clock ticks and sensor interrupts. E code is portable and, given an input behavior, exhibits predictable (i.e., deterministic) timing and output behavior. The second phase, the platform-dependent compiler phase, checks the time safety of the E code, that is, whether platform performance (determined by the hardware) and platform utilization (determined by the scheduler of the operating system) enable its timely execution. We have used the Embedded Machine to compile and execute high-performance control applications written in Giotto, such as the flight control system of an autonomous model helicopter.}, author = {Thomas Henzinger and Kirsch, Christoph M}, journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, number = {393}, publisher = {ACM}, title = {{The embedded machine: Predictable, portable real-time code}}, doi = {10.1145/1286821.1286824}, volume = {29}, year = {2007}, } @inproceedings{4511, abstract = {In the traditional view, a language is a set of words, i.e., a function from words to boolean values. We call this view “qualitative,” because each word either belongs to or does not belong to a language. Let Σ be an alphabet, and let us consider infinite words over Σ. Formally, a qualitative language over Σ is a function A: B . There are many applications of qualitative languages. For example, qualitative languages are used to specify the legal behaviors of systems, and zero-sum objectives of games played on graphs. In the former case, each behavior of a system is either legal or illegal; in the latter case, each outcome of a game is either winning or losing. For defining languages, it is convenient to use finite acceptors (or generators). In particular, qualitative languages are often defined using finite-state machines (so-called ω-automata) whose transitions are labeled by letters from Σ. For example, the states of an ω-automaton may represent states of a system, and the transition labels may represent atomic observables of a behavior. There is a rich and well-studied theory of finite-state acceptors of qualitative languages, namely, the theory of theω-regular languages.}, author = {Thomas Henzinger}, pages = {20 -- 22}, publisher = {Springer}, title = {{Quantitative generalizations of languages}}, doi = {10.1007/978-3-540-73208-2_2}, volume = {4588}, year = {2007}, } @inproceedings{4514, abstract = {Digital technology is increasingly deployed in safety-critical situations. This calls for systematic design and verification methodologies that can cope with three major sources of system complexity: concurrency, real time, and uncertainty. We advocate a two-step process: formal modeling followed by algorithmic analysis (or, “model building” followed by “model checking”). We model the concurrent components of a reactive system as potential collaborators or adversaries in a multi-player game with temporal objectives, such as system safety. The real-time aspect of embedded systems requires models that combine discrete state transitions and continuous state evolutions. Uncertainty in the environment is naturally modeled by probabilistic state changes. As a result, we obtain three orthogonal extensions of the basic state-transition graph model for reactive systems —game graphs, timed graphs, and stochastic graphs— as well as combinations thereof. In this short text, we provide a uniform exposition of the underlying definitions. For verification algorithms, we refer the reader to the literature.}, author = {Thomas Henzinger}, pages = {103 -- 110}, publisher = {Springer}, title = {{Games, time, and probability: Graph models for system design and analysis}}, doi = {10.1007/978-3-540-69507-3_7}, volume = {4362}, year = {2007}, } @article{4529, abstract = {Computational modeling of biological systems is becoming increasingly important in efforts to better understand complex biological behaviors. In this review, we distinguish between two types of biological models—mathematical and computational—which differ in their representations of biological phenomena. We call the approach of constructing computational models of biological systems 'executable biology', as it focuses on the design of executable computer algorithms that mimic biological phenomena. We survey the main modeling efforts in this direction, emphasize the applicability and benefits of executable models in biological research and highlight some of the challenges that executable biology poses for biology and computer science. We claim that for executable biology to reach its full potential as a mainstream biological technique, formal and algorithmic approaches must be integrated into biological research. This will drive biology toward a more precise engineering discipline.}, author = {Fisher, Jasmin and Thomas Henzinger}, journal = {Nature Biotechnology}, pages = {1239 -- 1249}, publisher = {Nature Publishing Group}, title = {{Executable cell biology}}, doi = {10.1038/nbt1356}, volume = {25}, year = {2007}, } @proceedings{4530, abstract = {This book constitutes the refereed proceedings of the 21st International Workshop on Computer Science Logic, CSL 2007, held as the 16th Annual Conference of the EACSL in Lausanne, Switzerland. The 36 revised full papers presented together with the abstracts of six invited lectures are organized in topical sections on logic and games, expressiveness, games and trees, logic and deduction, lambda calculus, finite model theory, linear logic, proof theory, and game semantics.}, author = {Duparc, Jacques and Thomas Henzinger}, booktitle = {CSL: Computer Science Logic}, publisher = {Springer}, title = {{CSL: Computer Science Logic }}, doi = {10.1007/978-3-540-74915-8}, volume = {4646}, year = {2007}, } @article{4531, abstract = {Caenorhabditis elegans vulval development provides an important paradigm for studying the process of cell fate determination and pattern formation during animal development. Although many genes controlling vulval cell fate specification have been identified, how they orchestrate themselves to generate a robust and invariant pattern of cell fates is not yet completely understood. Here, we have developed a dynamic computational model incorporating the current mechanistic understanding of gene interactions during this patterning process. A key feature of our model is the inclusion of multiple modes of crosstalk between the epidermal growth factor receptor (EGFR) and LIN-12/Notch signaling pathways, which together determine the fates of the six vulval precursor cells (VPCs). Computational analysis, using the model-checking technique, provides new biological insights into the regulatory network governing VPC fate specification and predicts novel negative feedback loops. In addition, our analysis shows that most mutations affecting vulval development lead to stable fate patterns in spite of variations in synchronicity between VPCs. Computational searches for the basis of this robustness show that a sequential activation of the EGFR-mediated inductive signaling and LIN-12 / Notch-mediated lateral signaling pathways is key to achieve a stable cell fate pattern. We demonstrate experimentally a time-delay between the activation of the inductive and lateral signaling pathways in wild-type animals and the loss of sequential signaling in mutants showing unstable fate patterns; thus, validating two key predictions provided by our modeling work. The insights gained by our modeling study further substantiate the usefulness of executing and analyzing mechanistic models to investigate complex biological behaviors.}, author = {Fisher, Jasmin and Piterman, Nir and Hajnal, Alex and Thomas Henzinger}, journal = {PLoS Computational Biology}, publisher = {Public Library of Science}, title = {{Predictive modeling of signaling crosstalk during C. elegans vulval development}}, doi = {10.1371/journal.pcbi.0030092}, volume = {3(5):e92}, year = {2007}, } @inproceedings{4537, abstract = {The classical synthesis problem for reactive systems asks, given a proponent process A and an opponent process B, to refine A so that the closed-loop system A parallel to B satisfies a given specification Phi. The solution of this problem requires the computation of a winning strategy for proponent A in a game against opponent B. We define and study the co-synthesis problem, where the proponent A consists itself of two independent processes, A = A(1)parallel to A(2), with specifications Phi(1) and Phi(2), and the goal is to refine both A(1) and A(2) so that A(1)parallel to A(2)parallel to B satisfies Phi(1) boolean AND Phi(2). For example, if the opponent B is a fair scheduler for the two processes A(1) and A(2), and Phi(i) specifies the requirements of mutual exclusion for A(i) (e.g., starvation freedom), then the co-synthesis problem asks for the automatic synthesis of a mutual-exclusion protocol. We show that co-synthesis defined classically, with the processes A(1) and A(2) either collaborating or competing, does not capture desirable solutions. Instead, the proper formulation of co-synthesis is the one where process A, competes with A(2) but not at the price of violating Phi(1), and vice versa. We call this assume-guarantee synthesis and show that it can be solved by computing secure-equilibrium strategies. In particular, from mutual-exclusion requirements the assume-guarantee synthesis algorithm automatically computes Peterson's protocol.}, author = {Krishnendu Chatterjee and Thomas Henzinger}, pages = {261 -- 275}, publisher = {Springer}, title = {{Assume-guarantee synthesis}}, doi = {10.1007/978-3-540-71209-1_21}, volume = {4424}, year = {2007}, } @article{4547, abstract = {We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller that does not see the private state of the plant. Our main results are twofold. First, we give a fixed-point algorithm for computing the set of states from which a player can win with a deterministic observation-based strategy for any omega-regular objective. The fixed point is computed in the lattice of antichains of state sets. This algorithm has the advantages of being directed by the objective and of avoiding an explicit subset construction on the game graph. Second, we give an algorithm for computing the set of states from which a player can win with probability 1 with a randomized observation-based strategy for a Buechi objective. This set is of interest because in the absence of perfect information, randomized strategies are more powerful than deterministic ones. We show that our algorithms are optimal by proving matching lower bounds.}, author = {Krishnendu Chatterjee and Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François}, journal = {Logical Methods in Computer Science}, number = {184}, pages = {1 -- 23}, publisher = {International Federation of Computational Logic}, title = {{Algorithms for omega-regular games with imperfect information}}, doi = {10.2168/LMCS-3(3:4)2007}, volume = {3}, year = {2007}, } @phdthesis{4559, abstract = {We study games played on graphs with omega-regular conditions specified as parity, Rabin, Streett or Muller conditions. These games have applications in the verification, synthesis, modeling, testing, and compatibility checking of reactive systems. Important distinctions between graph games are as follows: (a) turn-based vs. concurrent games, depending on whether at a state of the game only a single player makes a move, or players make moves simultaneously; (b) deterministic vs. stochastic, depending on whether the transition function is a deterministic or a probabilistic function over successor states; and (c) zero-sum vs. non-zero-sum, depending on whether the objectives of the players are strictly conflicting or not. We establish that the decision problem for turn-based stochastic zero-sum games with Rabin, Streett, and Muller objectives are NP-complete, coNP-complete, and PSPACE-complete, respectively, substantially improving the previously known 3EXPTIME bound. We also present strategy improvement style algorithms for turn-based stochastic Rabin and Streett games. In the case of concurrent stochastic zero-sum games with parity objectives we obtain a PSPACE bound, again improving the previously known 3EXPTIME bound. As a consequence, concurrent stochastic zero-sum games with Rabin, Streett, and Muller objectives can be solved in EXPSPACE, improving the previously known 4EXPTIME bound. We also present an elementary and combinatorial proof of the existence of memoryless \epsilon-optimal strategies in concurrent stochastic games with reachability objectives, for all real \epsilon>0, where an \epsilon-optimal strategy achieves the value of the game with in \epsilon against all strategies of the opponent. We also use the proof techniques to present a strategy improvement style algorithm for concurrent stochastic reachability games. We then go beyond \omega-regular objectives and study the complexity of an important class of quantitative objectives, namely, limit-average objectives. In the case of limit-average games, the states of the graph is labeled with rewards and the goal is to maximize the long-run average of the rewards. We show that concurrent stochastic zero-sum games with limit-average objectives can be solved in EXPTIME. Finally, we introduce a new notion of equilibrium, called secure equilibrium, in non-zero-sum games which captures the notion of conditional competitiveness. We prove the existence of unique maximal secure equilibrium payoff profiles in turn-based deterministic games, and present algorithms to compute such payoff profiles. We also show how the notion of secure equilibrium extends the assume-guarantee style of reasoning in the game theoretic framework.}, author = {Krishnendu Chatterjee}, pages = {1 -- 247}, publisher = {University of California, Berkeley}, title = {{Stochastic ω-Regular Games}}, year = {2007}, } @phdthesis{4566, abstract = {Complex system design today calls for compositional design and implementation. However each component is designed with certain assumptions about the environment it is meant to operate in, and delivering certain guarantees if those assumptions are satisfied; numerous inter-component interaction errors are introduced in the manual and error-prone integration process as there is little support in design environments for machine-readably representing these assumptions and guarantees and automatically checking consistency during integration. Based on Interface Automata we propose a framework for compositional design and analysis of systems: a set of domain-specific automata-theoretic type systems for compositional system specification and analysis by behavioral specification of open systems. We focus on three different domains: component-based hardware systems communicating on bidirectional wires. concurrent distributed recursive message-passing software systems, and embedded software system components operating in resource-constrained environments. For these domains we present approaches to formally represent the assumptions and conditional guarantees between interacting open system components. Composition of such components produces new components with the appropriate assumptions and guarantees. We check satisfaction of temporal logic specifications by such components, and the substitutability of one component with another in an arbitrary context. Using this framework one can analyze large systems incrementally without needing extensive summary information to close the system at each stage. Furthermore, we focus only on the inter-component interaction behavior without dealing with the full implementation details of each component. Many of the merits of automata-theoretic model-checking are combined with the compositionality afforded by type-system based techniques. We also present an integer-based extension of the conventional boolean verification framework motivated by our interface formalism for embedded software components. Our algorithms for checking the behavioral compatibility of component interfaces are available in our tool Chic, which can be used as a plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment Ptolemy II. Finally, we address the complementary problem of partitioning a large system into meaningful coherent components by analyzing the interaction patterns between its basic elements. We demonstrate the usefulness of our partitioning approach by evaluating its efficacy in improving unit-test branch coverage for a large software system implemented in C.}, author = {Chakrabarti, Arindam}, pages = {1 -- 244}, publisher = {University of California, Berkeley}, title = {{A framework for compositional design and analysis of systems}}, year = {2007}, } @article{4567, abstract = {BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to BLAST and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use BLAST to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, BLAST determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that BLAST can provide automated, precise, and scalable analysis for C programs.}, author = {Beyer, Dirk and Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S}, journal = {International Journal on Software Tools for Technology Transfer}, number = {5}, pages = {505 -- 525}, publisher = {Springer}, title = {{The software model checker BLAST: Applications to software engineering}}, doi = {10.1007/s10009-007-0044-z}, volume = {9}, year = {2007}, } @inproceedings{4570, abstract = {We consider the minimum-time reachability problem in concurrent two-player timed automaton game structures. We show how to compute the minimum time needed by a player to reach a target location against all possible choices of the opponent. We do not put any syntactic restriction on the game structure, nor do we require any player to guarantee time divergence. We only require players to use receptive strategies which do not block time. The minimal time is computed in part using a fixpoint expression, which we show can be evaluated on equivalence classes of a non-trivial extension of the clock-region equivalence relation for timed automata.}, author = {Brihaye, Thomas and Thomas Henzinger and Prabhu, Vinayak S and Raskin, Jean-François}, pages = {825 -- 837}, publisher = {Springer}, title = {{Minimum-time reachability in timed games}}, doi = {10.1007/978-3-540-73420-8_71}, volume = {4596}, year = {2007}, } @inproceedings{4571, abstract = {The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm -the spurious counterexample- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs-so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.}, author = {Beyer, Dirk and Thomas Henzinger and Majumdar, Ritankar S and Rybalchenko, Andrey}, pages = {300 -- 309}, publisher = {ACM}, title = {{Path invariants}}, doi = {10.1145/1250734.1250769}, year = {2007}, } @inproceedings{4572, abstract = {We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C.}, author = {Beyer, Dirk and Thomas Henzinger and Majumdar, Ritankar S and Rybalchenko, Andrey}, pages = {378 -- 394}, publisher = {Springer}, title = {{Invariant synthesis for combined theories}}, doi = {10.1007/978-3-540-69738-1_27}, volume = {4349}, year = {2007}, } @inproceedings{4573, abstract = {In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this purpose they build and refine reachability trees. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. We designed an algorithm and built a tool that can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. The algorithm and tool take one or more abstract interpreters, such as a predicate abstraction and a shape analysis, and configure their execution and interaction using several parameters. Our experiments show that such customization may lead to dramatic improvements in the precision-efficiency spectrum.}, author = {Beyer, Dirk and Thomas Henzinger and Théoduloz, Grégory}, pages = {504 -- 518}, publisher = {Springer}, title = {{Configurable software verification: Concretizing the convergence of model checking and program analysis}}, doi = {10.1007/978-3-540-73368-3_51}, volume = {4590}, year = {2007}, } @inproceedings{4575, abstract = {We present a case study to illustrate our formalism for the specification and verification of the method-invocation behavior of web-service applications constructed from asynchronously interacting multi-threaded distributed components. Our model is expressive enough to allow the representation of recursion and dynamic thread creation, and yet permits the algorithmic analysis of the following two questions: (1) Does a given service satisfy a safety specification? (2) Can a given service be substituted by a another service in an arbitrary context? Our case study is based on the Amazon.com E-Commerce Services (ECS) platform.}, author = {Beyer, Dirk and Chakrabarti, Arindam and Thomas Henzinger and Seshia, Sanjit A}, pages = {831 -- 838}, publisher = {IEEE}, title = {{An application of web-service interfaces}}, doi = {10.1109/ICWS.2007.32 }, year = {2007}, } @article{3019, abstract = { Directional transport of the phytohormone auxin is established primarily at the point of cellular afflux and is required for the establishment and maintenance of plant polarity. Studies in whole plants and heterologous systems indicate that PIN-FORMED (PIN) and P-glycoprotein (PGP) transport proteins mediate the cellular efflux of natural and synthetic auxins. However, aromatic anion transport resulting from PGP and PIN expression in nonplant systems was also found to lack tha high level of substrate specificity seen in planta. Furthermore, previous reports that PGP19 stabilizes PIN1 on the plasma membrane suggested that PIN-PGP interactions might regulate polar auxin efflux. Hare, we show that PGP1 and PGP19 colocalized with PIN1 in the shoot apax in Arabidopsis thaliana and with PIN1 and PIN2 in root tissues. Specific PGP-PIN interactions were seen in yeast two-hybrid and colmmunoprecipitation assays. PIN-PGP interactions appeared to enhance transport activity and, to a greater extent, substrate/inhibitor specificities when coexpressed in heterologous systems. By contrast, no interactions between PGPs and the AUXIN1 influx carrier were observed. Phenotypes of pin and pgp mutants suggest discrete functional roles in auxin transport, but pin pgp mutants exhibited phenotypes that are both additive and synergistic. These results suggest that PINs and PGPs characterize coordinated, Independent auxin transport mechanisms but also function interactively in a tissue-specific manner.}, author = {Blakeslee, Joshua and Bandyopadhyay, Anindita and Ok, Ran Lee and Mravec, Jozef and Titapiwatanakun, Boosaree and Sauer, Michael and Makam, Srinivas N and Cheng, Yan and Bouchard, Rodolphe and Adamec, Jiří and Geisler, Markus and Nagashima, Akitomo and Sakai, Tatsuya and Martinoia, Enrico and Jirí Friml and Peer, Wendy A and Murphy, Angus S}, journal = {Plant Cell}, number = {1}, pages = {131 -- 147}, publisher = {American Society of Plant Biologists}, title = {{Interactions among PIN FORMED and P glycoprotein auxin transporters in Arabidopsis}}, doi = {10.1105/tpc.106.040782}, volume = {19}, year = {2007}, } @inproceedings{3021, abstract = {Polarized transport of the plant hormone auxin influences multiple growth processes in plants and is regulated by plasma-membrane-localized efflux and uptake carriers. The PGP (P-glycoprotein) ABC transporters (ATP-binding-cassette transporters), PIN (pin-formed) subfamily of major facilitator proteins and members of AUX/LAX families have been shown to independently transport auxin both in planta and in heterologous systems. However, PIN- and PGP-mediated transport in heterologous systems exhibits decreased substrate specificity and inhibitor-sensitivity compared with what is seen in plants and plant cells. To determine whether PIN-PGP interactions enhance transport specificity, we analysed interactions of the representative auxin-transporting PGPs with PIN1 and AUX1 in planta and in heterologous systems. Here, we provide evidence that PINs and PGPs interact and function both independently and co-ordinately to control polar auxin transport and impart transport specificity and directionality. These interactions take place in protein complexes stabilized by PGPs in detergent-resistant microdomains.}, author = {Bandyopadhyay, Anindita and Blakeslee, Joshua and Lee, Ok Ran and Mravec, Jozef and Sauer, Michael and Titapiwatanakun, Boosaree and Makam, Srinivas N and Bouchard, Rodolphe and Geisler, Markus and Martinoia, Enrico and Jirí Friml and Peer, Wendy A and Murphy, Angus S}, number = {1}, pages = {137 -- 141}, publisher = {Portland Press}, title = {{Interactions of PIN and PGP auxin transport mechanisms}}, doi = {10.1042/BST0350137}, volume = {35}, year = {2007}, } @article{3022, abstract = {Endocytosis is an essential process by which eukaryotic cells internalize exogenous material or regulate signaling at the cell surface [1]. Different endocytic pathways are well established in yeast and animals; prominent among them is clathrin-dependent endocytosis [2, 3]. In plants, endocytosis is poorly defined, and no molecular mechanism for cargo internalization has been demonstrated so far [4, 5], although the internalization of receptor-ligand complexes at the plant plasma membrane has recently been shown [6]. Here we demonstrate by means of a green-to-red photoconvertible fluorescent reporter, EosFP [7], the constitutive endocytosis of PIN auxin efflux carriers [8] and their recycling to the plasma membrane. Using a plant clathrin-specific antibody, we show the presence of clathrin at different stages of coated-vesicle formation at the plasma membrane in Arabidopsis. Genetic interference with clathrin function inhibits PIN internalization and endocytosis in general. Furthermore, pharmacological interference with cargo recruitment into the clathrin pathway blocks internalization of PINs and other plasma-membrane proteins. Our data demonstrate that clathrin-dependent endocytosis is operational in plants and constitutes the predominant pathway for the internalization of numerous plasma-membrane-resident proteins including PIN auxin efflux carriers.}, author = {Dhonukshe, Pankaj and Aniento, Fernando and Hwang, Inhwan and Robinson, David G and Mravec, Jozef and Stierhof, York-Dieter and Jirí Friml}, journal = {Current Biology}, number = {6}, pages = {520 -- 527}, publisher = {Cell Press}, title = {{Clathrin-mediated constitutive endocytosis of PIN auxin efflux carriers in Arabidopsis}}, doi = {10.1016/j.cub.2007.01.052}, volume = {17}, year = {2007}, } @article{3023, abstract = {Cytokinesis ensures proper partitioning of the nucleocytoplasmic contents into two daughter cells. It has generally been thought that cytokinesis is accomplished differently in animals and plants because of the differences in the preparatory phases, into the centrosomal or acentrosomal nature of the process, the presence or absence of rigid cell walls, and on the basis of ‘outside‐in’ or ‘inside‐out’ mechanism. However, this long‐standing paradigm needs further reevaluation based on new findings. Recent advances reveal that plant cells, similarly to animal cells, possess astral microtubules that regulate the cell division plane. Furthermore, endocytosis has been found to be important for cytokinesis in animal and plant cells: vesicles containing endocytosed cargo provide material for the cell plate formation in plants and for closure of the midbody channel in animals. Thus, although the preparatory phases of the cell division process differ between plant and animal cells, the later phases show similarities. We unify these findings in a model that suggests a conserved mode of cytokinesis.}, author = {Dhonukshe, Pankaj and Šamaj, Jozef and Baluška, František and Friml, Jirí}, journal = {Bioessays : News and Reviews in Molecular, Cellular and Developmental Biology}, number = {4}, pages = {371 -- 381}, publisher = {Wiley-Blackwell}, title = {{A unifying new model of cytokinesis for the dividing plant and animal cells}}, doi = {10.1002/bies.20559}, volume = {29}, year = {2007}, } @article{3024, abstract = {The plant hormone auxin is frequently observed to be asymmetrically distributed across adjacent cells during crucial stages of growth and development. These auxin gradients depend on polar transport and regulate a wide variety of processes, including embryogenesis, organogenesis, vascular tissue differentiation, root meristem maintenance and tropic growth. Auxin can mediate such a perplexing array of developmental processes by acting as a general trigger for the change in developmental program in cells where it accumulates and by providing vectorial information to the tissues by its polar intercellular flow. In recent years, a wealth of molecular data on the mechanism of auxin transport and its regulation has been generated, providing significant insights into the action of this versatile coordinative signal.}, author = {Vieten, Anne and Sauer, Michael and Brewer, Philip and Friml, Jirí}, journal = {Trends in Plant Science}, number = {4}, pages = {160 -- 168}, publisher = {Cell Press}, title = {{Molecular and cellular aspects of auxin-transport-mediated development}}, doi = {10.1016/j.tplants.2007.03.006}, volume = {12}, year = {2007}, } @article{3025, author = {Sauer, Michael and Balla, Jozef and Luschnig, Christian and Wiśniewska, Justyna and Reinöhl, Vilém and Jirí Friml and Eva Benková}, journal = {Genes and Development}, number = {11}, pages = {1431 -- 1431}, publisher = {Cold Spring Harbor Laboratory Press}, title = {{Erratum: Canalization of auxin flow by Aux/IAA-ARF-dependent feedback regulation of PIN polarity (Genes and Development (2006) 20 (2902-2911))}}, volume = {21}, year = {2007}, } @article{3026, abstract = {In plants, each developmental process integrates a network of signaling events that are regulated by different phytohormones, and interactions among hormonal pathways are essential to modulate their effect. Continuous growth of roots results from the postembryonic activity of cells within the root meristem that is controlled by the coordinated action of several phytohormones, including auxin and ethylene. Although their interaction has been studied intensively, the molecular and cellular mechanisms underlying this interplay are unknown. We show that the effect of ethylene on root growth is largely mediated by the regulation of the auxin biosynthesis and transport-dependent local auxin distribution. Ethylene stimulates auxin biosynthesis and basipetal auxin transport toward the elongation zone, where it activates a local auxin response leading to inhibition of cell elongation. Consistently, in mutants affected in auxin perception or basipetal auxin transport, ethylene cannot activate the auxin response nor regulate the root growth. In addition, ethylene modulates the transcription of several components of the auxin transport machinery. Thus, ethylene achieves a local activation of the auxin signaling pathway and regulates root growth by both stimulating the auxin biosynthesis and by modulating the auxin transport machinery.}, author = {Růžička, Kamil and Ljung, Karin and Vanneste, Steffen and Podhorská, Radka and Beeckman, Tom and Jirí Friml and Eva Benková}, journal = {Plant Cell}, number = {7}, pages = {2197 -- 2212}, publisher = {American Society of Plant Biologists}, title = {{Ethylene regulates root growth through effects on auxin biosynthesis and transport dependent auxin distribution}}, doi = {10.1105/tpc.107.052126}, volume = {19}, year = {2007}, } @article{3027, abstract = {Polar transport of the phytohormone auxin controls numerous growth responses in plants. Molecular characterization of auxin transport in Arabidopsis thaliana has provided important insights into the mechanisms underlying the regulation of auxin distribution. In particular, the control of subcellular localization and expression of PIN-type auxin efflux components appears to be fundamental for orchestrated distribution of the growth regulator throughout the entire plant body. Here we describe the identification of two Arabidopsis loci, MOP2 and MOP3 (for MODULATOR OF PIN), that are involved in control of the steady-state levels of PIN protein. Mutations in both loci result in defects in auxin distribution and polar auxin transport, and cause phenotypes consistent with a reduction of PIN protein levels. Genetic interaction between PIN2 and both MOP loci is suggestive of functional cross-talk, which is further substantiated by findings demonstrating that ectopic PIN up-regulation is compensated in the mop background. Thus, in addition to pathways that control PIN localization and transcription, MOP2 and MOP3 appear to be involved in fine-tuning of auxin distribution via post-transcriptional regulation of PIN expression.}, author = {Malenica, Nenad and Abas, Lindy and Benjamins, René and Kitakura, Saeko and Sigmund, Harald F and Jun, Kim S and Hauser, Marie-Theres and Jirí Friml and Luschnig, Christian}, journal = {Plant Journal}, number = {4}, pages = {537 -- 550}, publisher = {Wiley-Blackwell}, title = {{MODULATOR of PIN genes control steady state levels of Arabidopsis PIN proteins}}, doi = {10.1111/j.1365-313X.2007.03158.x}, volume = {51}, year = {2007}, } @article{3028, abstract = {In plants, cell polarity and tissue patterning are connected by intercellular flow of the phytohormone auxin, whose directional signaling depends on polar subcellular localization of PIN auxin transport proteins. The mechanism of polar targeting of PINs or other cargos in plants is largely unidentified, with the PINOID kinase being the only known molecular component. Here, we identify PP2A phosphatase as an important regulator of PIN apical-basal targeting and auxin distribution. Genetic analysis, localization, and phosphorylation studies demonstrate that PP2A and PINOID both partially colocalize with PINs and act antagonistically on the phosphorylation state of their central hydrophilic loop, hence mediating PIN apical-basal polar targeting. Thus, in plants, polar sorting by the reversible phosphorylation of cargos allows for their conditional delivery to specific intracellular destinations. In the case of PIN proteins, this mechanism enables switches in the direction of intercellular auxin fluxes, which mediate differential growth, tissue patterning, and organogenesis.}, author = {Michniewicz, Marta and Zago, Marcelo K and Abas, Lindy and Weijers, Dolf and Schweighofer, Alois and Meskiene, Irute and Heisler, Marcus G and Ohno, Carolyn and Zhang, Jing and Huang, Fang and Schwab, Rebecca and Weigel, Detlef and Meyerowitz, Elliot M and Luschnig, Christian and Offringa, Remko and Jirí Friml}, journal = {Cell}, number = {6}, pages = {1044 -- 1056}, publisher = {Cell Press}, title = {{Antagonistic regulation of PIN phosphorylation by PP2A and PINOID directs auxin flux}}, doi = {10.1016/j.cell.2007.07.033}, volume = {130}, year = {2007}, } @article{3029, abstract = {In Arabidopsis thaliana, lateral roots are formed from root pericycle cells adjacent to the xylem poles. Lateral root development is regulated antagonistically by the plant hormones auxin and cytokinin. While a great deal is known about how auxin promotes lateral root development, the mechanism of cytokinin repression is still unclear. Elevating cytokinin levels was observed to disrupt lateral root initiation and the regular pattern of divisions that characterizes lateral root development in Arabidopsis. To identify the stage of lateral root development that is sensitive to cytokinins, we targeted the expression of the Agrobacterium tumefaciens cytokinin biosynthesis enzyme isopentenyltransferase to either xylem-pole pericycle cells or young lateral root primordia using GAL4-GFP enhancer trap lines. Transactivation experiments revealed that xylem-pole pericycle cells are sensitive to cytokinins, whereas young lateral root primordia are not. This effect is physiologically significant because transactivation of the Arabidopsis cytokinin degrading enzyme cytokinin oxidase 1 in lateral root founder cells results in increased lateral root formation. We observed that cytokinins perturb the expression of PIN genes in lateral root founder cells and prevent the formation of an auxin gradient that is required to pattern lateral root primordia.}, author = {Laplaze, Laurent and Eva Benková and Casimiro, Ilda and Maes, Lies and Vanneste, Steffen and Swarup, Ranjan and Weijers, Dolf and Calvo, Vanessa and Parizot, Boris and Herrera-Rodriguez, Maria Begoña and Offringa, Remko and Graham, Neil and Doumas, Patrick and Jirí Friml and Bogusz, Didier and Beeckman, Tom and Bennett, Malcolm}, journal = {Plant Cell}, number = {12}, pages = {3889 -- 3900}, publisher = {American Society of Plant Biologists}, title = {{Cytokinins act directly on lateral root founder cells to inhibit root initiation}}, doi = {10.1105/tpc.107.055863}, volume = {19}, year = {2007}, } @article{3144, abstract = {Accumulation of specific proteins at synaptic structures is essential for synapse assembly and function, but mechanisms regulating local protein enrichment remain poorly understood. At the neuromuscular junction (NMJ), subsynaptic nuclei underlie motor axon terminals within extrafusal muscle fibers and are transcriptionally distinct from neighboring nuclei. In this study, we show that expression of the ETS transcription factor Erm is highly concentrated at subsynaptic nuclei, and its mutation in mice leads to severe downregulation of many genes with normally enriched subsynaptic expression. Erm mutant mice display an expansion of the muscle central domain in which acetylcholine receptor (AChR) clusters accumulate, show gradual fragmentation of AChR clusters, and exhibit symptoms of muscle weakness mimicking congenital myasthenic syndrome (CMS). Together, our findings define Erm as an upstream regulator of a transcriptional program selective to subsynaptic nuclei at the NMJ and underscore the importance of transcriptional control of local synaptic protein accumulation.}, author = {Simon Hippenmeyer and Huber, Roland M and Ladle, David R and Murphy, Kenneth and Arber, Silvia}, journal = {Neuron}, number = {5}, pages = {726 -- 740}, publisher = {Elsevier}, title = {{ETS transcription factor Erm controls subsynaptic gene expression in skeletal muscles}}, doi = {10.1016/j.neuron.2007.07.028}, volume = {55}, year = {2007}, } @article{3187, abstract = {Stereo vision has numerous applications in robotics, graphics, inspection and other areas. A prime application, one which has driven work on stereo in our laboratory, is teleconferencing in which the use of a stereo webcam already makes possible various transformations of the video stream. These include digital camera control, insertion of virtual objects, background substitution, and eye-gaze correction [9, 8].}, author = {Blake, Andrew and Criminisi, Antonio and Cross, Geoffrey and Vladimir Kolmogorov and Rother, Carsten}, journal = {Springer Tracts in Advanced Robotics}, pages = {295 -- 304}, publisher = {Springer}, title = {{Fusion of stereo colour and contrast}}, doi = {10.1007/978-3-540-48113-3_27}, volume = {28}, year = {2007}, } @inproceedings{3191, abstract = {The maximum flow algorithm for minimizing energy functions of binary variables has become a standard tool in computer vision. In many cases, unary costs of the energy depend linearly on parameter lambda. In this paper we study vision applications for which it is important to solve the maxflow problem for different lambda's. An example is a weighting between data and regularization terms in image segmentation or stereo: it is desirable to vary it both during training (to learn lambda from ground truth data) and testing (to select best lambda using high-knowledge constraints, e.g. user input). We review algorithmic aspects of this parametric maximum flow problem previously unknown in vision, such as the ability to compute all breakpoints of lambda and corresponding optimal configurations infinite time. These results allow, in particular, to minimize the ratio of some geometric functional, such as flux of a vector field over length (or area). Previously, such functional were tackled with shortest path techniques applicable only in 2D. We give theoretical improvements for "PDE cuts" [5]. We present experimental results for image segmentation, 3D reconstruction, and the cosegmentation problem.}, author = {Vladimir Kolmogorov and Boykov, Yuri and Rother, Carsten}, publisher = {IEEE}, title = {{Applications of parametric maxflow in computer vision}}, doi = {10.1109/ICCV.2007.4408910}, year = {2007}, } @inproceedings{3192, abstract = {Many computer vision applications rely on the efficient optimization of challenging, so-called non-submodular, binary pairwise MRFs. A promising graph cut based approach for optimizing such MRFs known as "roof duality" was recently introduced into computer vision. We study two methods which extend this approach. First, we discuss an efficient implementation of the "probing" technique introduced recently by Boros et al. [5]. It simplifies the MRF while preserving the global optimum. Our code is 400-700 faster on some graphs than the implementation of [5]. Second, we present a new technique which takes an arbitrary input labeling and tries to improve its energy. We give theoretical characterizations of local minima of this procedure. We applied both techniques to many applications, including image segmentation, new view synthesis, superresolution, diagram recognition, parameter learning, texture restoration, and image deconvolution. For several applications we see that we are able to find the global minimum very efficiently, and considerably outperform the original roof duality approach. In comparison to existing techniques, such as graph cut, TRW, BP, ICM, and simulated annealing, we nearly always find a lower energy.}, author = {Rother, Carsten and Vladimir Kolmogorov and Lempitsky, Victor and Szummer, Martin}, publisher = {IEEE}, title = {{Optimizing binary MRFs via extended roof duality}}, doi = {10.1109/CVPR.2007.383203}, year = {2007}, } @article{3193, abstract = {Optimization techniques based on graph cuts have become a standard tool for many vision applications. These techniques allow to minimize efficiently certain energy functions corresponding to pairwise Markov Random Fields (MRFs). Currently, there is an accepted view within the computer vision community that graph cuts can only be used for optimizing a limited class of MRF energies (e.g., submodular functions). In this survey, we review some results that show that graph cuts can be applied to a much larger class of energy functions (in particular, nonsubmodular functions). While these results are well-known in the optimization community, to our knowledge they were not used in the context of computer vision and MRF optimization. We demonstrate the relevance of these results to vision on the problem of binary texture restoration. }, author = {Vladimir Kolmogorov and Rother, Carsten}, journal = {IEEE Transactions on Pattern Analysis and Machine Intelligence}, number = {7}, pages = {1274 -- 1279}, publisher = {IEEE}, title = {{Minimizing nonsubmodular functions with graph cuts - A review}}, doi = {10.1109/TPAMI.2007.1031}, volume = {29}, year = {2007}, } @inproceedings{3218, abstract = {A (k, ℓ)-robust combiner for collision-resistant hash-functions is a construction which from ℓ hash-functions constructs a hash-function which is collision-resistant if at least k of the components are collision-resistant. One trivially gets a (k, ℓ)-robust combiner by concatenating the output of any ℓ - k + 1 of the components, unfortunately this is not very practical as the length of the output of the combiner is quite large. We show that this is unavoidable as no black-box (k, ℓ)-robust combiner whose output is significantly shorter than what can be achieved by concatenation exists. This answers a question of Boneh and Boyen (Crypto'06). }, author = {Krzysztof Pietrzak}, pages = {23 -- 33}, publisher = {Springer}, title = {{Non-trivial black-box combiners for collision-resistant hash-functions don't exist}}, doi = {10.1007/978-3-540-72540-4_2}, volume = {4515}, year = {2007}, } @inproceedings{3219, abstract = {Many aspects of cryptographic security proofs can be seen as the proof that a certain system (e.g. a block cipher) is indistinguishable from an ideal system (e.g. a random permutation), for different types of distinguishers. This paper presents a new generic approach to proving upper bounds on the information-theoretic distinguishing advantage (from an ideal system) for a combined system, assuming upper bounds of certain types for the component systems. For a general type of combination operation of systems, including the XOR of functions or the cascade of permutations, we prove two amplification theorems. The first is a product theorem, in the spirit of XOR-lemmas: The distinguishing advantage of the combination of two systems is at most twice the product of the individual distinguishing advantages. This bound is optimal. The second theorem states that the combination of systems is secure against some strong class of distinguishers, assuming only that the components are secure against some weaker class of distinguishers. A key technical tool of the paper is the proof of a tight two-way correspondence, previously only known to hold in one direction, between the distinguishing advantage of two systems and the probability of winning an appropriately defined game. © International Association for Cryptologic Research 2007.}, author = {Maurer, Ueli M and Krzysztof Pietrzak and Renner, Renato}, pages = {130 -- 149}, publisher = {Springer}, title = {{Indistinguishability amplification}}, doi = {10.1007/978-3-540-74143-5_8}, volume = {4622}, year = {2007}, } @inproceedings{3220, abstract = {We introduce a new primitive called intrusion-resilient secret sharing (IRSS), whose security proof exploits the fact that there exist functions which can be efficiently computed interactively using low communication complexity in k, but not in k-1 rounds. IRSS is a means of sharing a secret message amongst a set of players which comes with a very strong security guarantee. The shares in an IRSS are made artificially large so that it is hard to retrieve them completely, and the reconstruction procedure is interactive requiring the players to exchange k short messages. The adversaries considered can attack the scheme in rounds, where in each round the adversary chooses some player to corrupt and some function, and retrieves the output of that function applied to the share of the corrupted player. This model captures for example computers connected to a network which can occasionally he infected by malicious software like viruses, which can compute any function on the infected machine, but cannot sent out a huge amount of data. Using methods from the bounded-retrieval model, we construct an IRSS scheme which is secure against any computationally unbounded adversary as long as the total amount of information retrieved by the adversary is somewhat less than the length of the shares, and the adversary makes at most k-1 corruption rounds (as described above, where k rounds are necessary for reconstruction). We extend our basic scheme in several ways in order to allow the shares sent by the dealer to be short (the players then blow them up locally) and to handle even stronger adversaries who can learn some of the shares completely. As mentioned, there is an obvious connection between IRSS schemes and the fact that there exist functions with an exponential gap in their communication complexity for k and k-1 rounds. Our scheme implies such a separation which is in several aspects stronger than the previously known ones.}, author = {Dziembowski, Stefan and Krzysztof Pietrzak}, pages = {227 -- 237}, publisher = {IEEE}, title = {{Intrusion resilient secret sharing}}, doi = {10.1109/FOCS.2007.63}, year = {2007}, } @inproceedings{3221, abstract = {We investigate a general class of (black-box) constructions for range extension of weak pseudorandom functions: a construction based on m independent functions F 1,...,F m is given by a set of strings over {1,...,m}*, where for example {〈2〉, 〈1,2〉} corresponds to the function X ↦[F 2(X),F 2(F 1(X))]. All efficient constructions for range expansion of weak pseudorandom functions that we are aware of are of this form. We completely classify such constructions as good, bad or ugly, where the good constructions are those whose security can be proven via a black-box reduction, the bad constructions are those whose insecurity can be proven via a black-box reduction, and the ugly constructions are those which are neither good nor bad. Our classification shows that the range expansion from [10] is optimal, in the sense that it achieves the best possible expansion (2 m  − 1 when using m keys). Along the way we show that for weak quasirandom functions (i.e. in the information theoretic setting), all constructions which are not bad – in particular all the ugly ones – are secure.}, author = {Krzysztof Pietrzak and Sjödin, Johan}, pages = {517 -- 533}, publisher = {Springer}, title = {{Range extension for weak PRFs the good the bad and the ugly}}, doi = {10.1007/978-3-540-72540-4_30}, volume = {4515}, year = {2007}, } @inproceedings{3222, abstract = {Parallel repetition is well known to reduce the error probability at an exponential rate for single- and multi-prover interactive proofs. Bellare, Impagliazzo and Naor (1997) show that this is also true for protocols where the soundness only holds against computationally bounded provers (e.g. interactive arguments) if the protocol has at most three rounds. On the other hand, for four rounds they give a protocol where this is no longer the case: the error probability does not decrease below some constant even if the protocol is repeated a polynomial number of times. Unfortunately, this protocol is not very convincing as the communication complexity of each instance of the protocol grows linearly with the number of repetitions, and for such protocols the error does not even decrease for some types of interactive proofs. Noticing this, Bellare et al. construct (a quite artificial) oracle relative to which a four round protocol exists whose communication complexity does not depend on the number of parallel repetitions. This shows that there is no “black-box” error reduction theorem for four round protocols. In this paper we give the first computationally sound protocol where k-fold parallel repetition does not decrease the error probability below some constant for any polynomial k (and where the communication complexity does not depend on k). The protocol has eight rounds and uses the universal arguments of Barak and Goldreich (2001). We also give another four round protocol relative to an oracle, unlike the artificial oracle of Bellare et al., we just need a generic group. This group can then potentially be instantiated with some real group satisfying some well defined hardness assumptions (we do not know of any candidate for such a group at the moment).}, author = {Krzysztof Pietrzak and Wikström, Douglas}, pages = {86 -- 102}, publisher = {Springer}, title = {{Parallel repetition of computationally sound protocols revisited}}, doi = {10.1007/978-3-540-70936-7_5}, volume = {4392}, year = {2007}, } @inproceedings{3223, abstract = {“Hash then encrypt” is an approach to message authentication, where first the message is hashed down using an ε-universal hash function, and then the resulting k-bit value is encrypted, say with a block-cipher. The security of this scheme is proportional to εq2, where q is the number of MACs the adversary can request. As ε is at least 2−k, the best one can hope for is O(q2/2k) security. Unfortunately, such small ε is not achieved by simple hash functions used in practice, such as the polynomial evaluation or the Merkle-Damg ̊ard construction, where ε grows with the message length L. The main insight of this work comes from the fact that, by using ran- domized message preprocessing via a short random salt p (which must then be sent as part of the authentication tag), we can use the “hash then encrypt” paradigm with suboptimal “practical” ε-universal hash func- tions, and still improve its exact security to optimal O(q2/2k). Specif- ically, by using at most an O(logL)-bit salt p, one can always regain the optimal exact security O(q2/2k), even in situations where ε grows polynomially with L. We also give very simple preprocessing maps for popular “suboptimal” hash functions, namely polynomial evaluation and the Merkle-Damg ̊ard construction. Our results come from a general extension of the classical Carter- Wegman paradigm, which we believe is of independent interest. On a high level, it shows that public randomization allows one to use the potentially much smaller “average-case” collision probability in place of the “worst-case” collision probability ε.}, author = {Dodis, Yevgeniy and Krzysztof Pietrzak}, pages = {414 -- 433}, publisher = {Springer}, title = {{Improving the security of MACs via randomized message preprocessing}}, doi = {10.1007/978-3-540-74619-5_26}, volume = {4593}, year = {2007}, } @article{3305, abstract = {The accumulation of deleterious mutations plays a major role in evolution, and key to this are the interactions between their fitness effects, known as epistasis. Whether mutations tend to interact synergistically (with multiple mutations being more deleterious than would be expected from their individual fitness effects) or antagonistically is important for a variety of evolutionary questions, particularly the evolution of sex. Unfortunately, the experimental evidence on the prevalence and strength of epistasis is mixed and inconclusive. Here we study theoretically whether synergistic or antagonistic epistasis is likely to be favored by evolution and by how much. We find that in the presence of recombination, evolution favors less synergistic or more antagonistic epistasis whenever mutations that change the epistasis in this direction are possible. This is because evolution favors increased buffering against the effects of deleterious mutations. This suggests that we should not expect synergistic epistasis to be widespread in nature and hence that the mutational deterministic hypothesis for the advantage of sex may not apply widely.}, author = {Desai, Michael M and Daniel Weissman and Feldman, Marcus W}, journal = {Genetics}, number = {2}, pages = {1001 -- 10}, publisher = {Genetics Society of America}, title = {{Evolution can favor antagonistic epistasis}}, doi = {10.1534/genetics.107.075812}, volume = {177}, year = {2007}, } @article{3411, abstract = {Mechanical single-molecule techniques offer exciting possibilities to investigate protein folding and stability in native environments at submolecular resolution. By applying a free-energy reconstruction procedure developed by Hummer and Szabo, which is based on a statistical theorem introduced by Jarzynski, we determined the unfolding free energy of the membrane proteins bacteriorhodopsin (BR), halorhodopsin, and the sodium-proton antiporter NhaA. The calculated energies ranged from 290.5kcal/mol for BR to 485.5kcal/mol for NhaA. For the remarkably stable BR, the equilibrium unfolding free energy was independent of pulling rate and temperature ranging between 18 and 42°C. Our experiments also revealed heterogeneous energetic properties in individual transmembrane helices. In halorhodopsin, the stabilization of a short helical segment yielded a characteristic signature in the energy profile. In NhaA, a pronounced peak was observed at a functionally important site in the protein. Since a large variety of single- and multispan membrane proteins can be tackled in mechanical unfolding experiments, our approach provides a basis for systematically elucidating energetic properties of membrane proteins with the resolution of individual secondary-structure elements.}, author = {Preiner, Johannes and Harald Janovjak and Rankl, Christian and Knaus, Helene and Cisneros, David A and Kedrov, Alexej and Kienberger, Ferry and Mueller, Daniel J and Hinterdorfer, Peter}, journal = {Biophysical Journal}, number = {3}, pages = {930 -- 937}, publisher = {Biophysical Society}, title = {{Free energy of membrane protein unfolding derived from single-molecule force measurements}}, doi = {10.1529/biophysj.106.096982}, volume = {93}, year = {2007}, } @misc{3412, abstract = {Molecular interactions are the basic language of biological processes. They establish the forces interacting between the building blocks of proteins and other macromolecules, thus determining their functional roles. Because molecular interactions trigger virtually every biological process, approaches to decipher their language are needed. Single-molecule force spectroscopy (SMFS) has been used to detect and characterize different types of molecular interactions that occur between and within native membrane proteins. The first experiments detected and localized molecular interactions that stabilized membrane proteins, including how these interactions were established during folding of α-helical secondary structure elements into the native protein and how they changed with oligomerization, temperature, and mutations. SMFS also enables investigators to detect and locate molecular interactions established during ligand and inhibitor binding. These exciting applications provide opportunities for studying the molecular forces of life. Further developments will elucidate the origins of molecular interactions encoded in their lifetimes, interaction ranges, interplay, and dynamics characteristic of biological systems.}, author = {Kedrov, Alexej and Harald Janovjak and Sapra, Tanuj K and Mueller, Daniel J}, booktitle = {Annual Review of Biophysics}, pages = {233 -- 260}, publisher = {Annual Reviews}, title = {{Deciphering molecular interactions of native membrane proteins by single-molecule force spectroscopy}}, doi = {10.1146/annurev.biophys.36.040306.132640}, volume = {36}, year = {2007}, } @article{3427, abstract = {We present a general theoretical framework to discuss mechanisms of morphogen transport and gradient formation in a cell layer. Trafficking events on the cellular scale lead to transport on larger scales. We discuss in particular the case of transcytosis where morphogens undergo repeated rounds of internalization into cells and recycling. Based on a description on the cellular scale, we derive effective nonlinear transport equations in one and two dimensions which are valid on larger scales. We derive analytic expressions for the concentration dependence of the effective diffusion coefficient and the effective degradation rate. We discuss the effects of a directional bias on morphogen transport and those of the coupling of the morphogen and receptor kinetics. Furthermore, we discuss general properties of cellular transport processes such as the robustness of gradients and relate our results to recent experiments on the morphogen Decapentaplegic (Dpp) that acts in the wing disk of the fruit fly Drosophila. © 2007 The American Physical Society}, author = {Bollenbach, Mark Tobias and Kruse, Karsten and Pantazis, Periklis and Gonzalez Gaitan, Marcos and Julicher, Frank}, journal = {Physical Review E Statistical Nonlinear and Soft Matter Physics}, number = {1}, publisher = {American Institute of Physics}, title = {{Morphogen transport in epithelia}}, doi = {10.1103/PhysRevE.75.011901}, volume = {75}, year = {2007}, } @inbook{3432, abstract = {Evolution has left its signature on the molecules and morphology of living organisms. Ancestral reconstruction offers an excellent tool for understanding the process of evolution using comparative information. Methods for ancestral reconstruction have generally focused on reconstructing the ancestral states at the internal nodes of a phylogeny. Often, we are not interested in particular nodes of the phylogeny but the whole history of a character. This chapter focuses on a Bayesian method for estimating these histories, or mutational paths, on phylogenies. Mutational path methods differ most notably from other approaches in their ability to estimate not only the ancestral states at the internal nodes of a phylogeny, but also the order and timing of mutational changes across the phylogeny. The chapter provides a concise introduction to the statistical tools needed for sampling mutational paths on a phylogeny.}, author = {Jonathan Bollback and Gardner, Paul P and Nielsen, Rasmus}, booktitle = {Ancestral Sequence Reconstruction}, editor = {Liberles, David A}, pages = {69 -- 79}, publisher = {Oxford University Press}, title = {{Estimating the history of mutations on a phylogeny}}, doi = {10.1093/acprof:oso/9780199299188.003.0006}, year = {2007}, } @article{3436, abstract = {he potential for di? erences between genetic paternity and paternity inferred from behavioral observation has long been recognized. These di? erences are associated with the challenge for females of seeking both genetic and material bene? ts; this challenge is less severe in species with polygynous, non-resource-based mating systems (such as leks) than in those with resource-based systems. We pres- ent the ? rst study of paternity patt erns in a non-resource-based species that does not form true leks. We compared paternity inferred from observed mating behavior to genetically assigned paternity in the Satin Bowerbird (Ptilonorhynchus violaceus) using eight microsatellite markers. Mating behavior was observed and recorded via automated video-cameras positioned at all bowers (29?34 bowers each year) in the study site throughout each mating season. We obtained blood samples and identi- ? ed mothers for 11 chicks in 9 nests. For all chicks, the most likely genetic father had been observed to mate with the mother in the year the chick was sampled. All most likely genetic fathers were assigned with high con? dence and all were bower- holding males. These results demonstrate that genetic paternity can be inferred from observed mating behavior with reasonable con? dence in Satin Bowerbirds. Observed male mating-success is therefore a reliable predictor of reproductive success, and this suggests that high skew in observed male mating-success translates directly to high skew in reproductive success. }, author = {Reynolds, Sheila M and Dryer, Katie and Jonathan Bollback and Uy, J Albert and Patricelli, Gail L and Robson, Timothy and Borgia, Gerald and Braun, Michael J}, journal = {The Auk}, number = {3}, pages = {857 -- 867}, publisher = {University of California Press}, title = {{Behavioral paternity predicts genetic paternity in satin bowerbirds, a species with a non-resource-based mating system}}, doi = {10.1642/0004-8038(2007)124[857:BPPGPI]2.0.CO;2}, volume = {124}, year = {2007}, } @article{3450, author = {Peter Jonas and Buzsáki, György}, journal = {Scholarpedia}, publisher = {Scholarpedia}, title = {{Neural inhibition}}, doi = {10.4249/scholarpedia.3286}, volume = {2}, year = {2007}, } @article{3523, abstract = {On the linear track, the recent firing sequences of CA1 place cells recur during sharp wave/ripple patterns (SWRs) in a reverse temporal order [Foster & Wilson (2006) Nature, 440, 680-683]. We have found similar reverse-order reactivation during SWRs in open-field exploration where the firing sequence of cells varied before each SWR. Both the onset times and the firing patterns of cells showed a tendency for reversed sequences during SWRs. These effects were observed for SWRs that occurred during exploration, but not for those during longer immobility periods. Additionally, reverse reactivation was stronger when it was preceded by higher speed (> 5 cm/s) run periods. The trend for reverse-order SWR reactivation was not significantly different in familiar and novel environments, even though SWR-associated firing rates of both pyramidal cells and interneurons were reduced in novel environments as compared with familiar. During exploration-associated SWRs (eSWR) place cells retain place-selective firing [O'Neill et al. (2006) Neuron, 49, 143-155]. Here, we have shown that each cell's firing onset was more delayed and firing probability more reduced during eSWRs the further the rat was from the middle of the cell's place field; that is, cells receiving less momentary place-related excitatory drive fired later during SWR events. However, even controlling for place field distance, the recent firing of cells was still significantly correlated with SWR reactivation sequences. We therefore propose that both place-related drive and the firing history of cells contribute to reverse reactivation during eSWRs.}, author = {Jozsef Csicsvari and Joseph O'Neill and Allen, Kevin and Senior,Timothy}, journal = {European Journal of Neuroscience}, number = {3}, pages = {704 -- 716}, publisher = {Wiley-Blackwell}, title = {{Place-selective firing contributes to the reverse-order reactivation of CA1 pyramidal cells during sharp waves in open-field exploration}}, doi = {10.1111/j.1460-9568.2007.05684.x}, volume = {26}, year = {2007}, } @inproceedings{3561, abstract = {The main result of this paper is an extension of de Silva's Weak Delaunay Theorem to smoothly embedded curves and surfaces in Euclidean space. Assuming a sufficiently fine sampling, we prove that i + 1 points in the sample span an i-simplex in the restricted Delaunay triangulation iff every subset of the i + 1 points has a weak witness.}, author = {Attali, Dominique and Herbert Edelsbrunner and Mileyko, Yuriy}, pages = {143 -- 150}, publisher = {ACM}, title = {{Weak witnesses for Delaunay triangulations of submanifolds}}, doi = {10.1145/1236246.1236267}, year = {2007}, } @inproceedings{3601, abstract = {In this paper, the multiobjective optimal design of space-based reconfigurable sensor networks with novel adaptive MEMS antennas is investigated by using multiobjective evolutionary algorithms. The non-dominated sorting genetic algorithm II (NSGA-II) is employed to obtain multi-criteria Pareto-optimal solutions, which allows system designers to easily make a reasonable trade-off choice from the set of non-dominated solutions according to their preferences and system requirements. As a case study, a cluster-based satellite sensing network is simulated under multiple objectives. Most importantly, this paper also presents the application of our newly designed adaptive MEMS antennas together with the NSGA-II to the multiobjective optimal design of space-based reconfigurable sensor networks.}, author = {Yang, Erfu and Haridas, Nakul and El-Rayis, Ahmed O and Erdogan, Ahmet T and Arslan, Tughrul and Nicholas Barton}, pages = {27 -- 34}, publisher = {IEEE}, title = {{Multiobjective optimal design of MEMS-based reconfigurable and evolvable sensor networks for space applications}}, doi = {10.1109/AHS.2007.76}, year = {2007}, } @book{3674, abstract = {Evolution permeates all of biology. But researchers in molecular and cellular biology, genetics, developmental biology, microbiology, and neuroscience have only recently begun to think seriously in terms of evolution. The chief reasons for this shift are the growing list of organisms with sequenced genomes; the increasingly sophisticated ways of interpreting those sequences; and the ever more powerful experimental techniques (and wider range of model organisms) with which to ask questions about evolution as well as mechanism. Evolution serves as a primary text for undergraduate and graduate courses in evolution. It is also a text working scientists can use to educate themselves on how evolution affects their fields. It differs from currently available alternatives in containing more molecular biology than is traditionally the case. But this is not at the expense of traditional evolutionary theory. Indeed, a glance at the Table of Contents and the authors' interests reveals the range of material covered in this book. The authors are world-renowned in population genetics, bacterial genomics, paleontology, human genetics, and developmental biology. The integration of molecular biology and evolutionary biology reflects the current direction of much research among evolutionary scientists.}, author = {Barton, Nicholas H and Briggs, Derek and Eisen, Jonathan and Goldstein, David and Patel, Nipam}, publisher = {Wiley-Blackwell}, title = {{Evolution}}, year = {2007}, } @inproceedings{3681, abstract = {The extraction of a parametric global motion from a motion field is a task with several applications in video processing. We present two probabilistic formulations of the problem and carry out optimization using the RAST algorithm, a geometric matching method novel to motion estimation in video. RAST uses an exhaustive and adaptive search of transformation space and thus gives – in contrast to local sampling optimization techniques used in the past – a globally optimal solution. Among other applications, our framework can thus be used as a source of ground truth for benchmarking motion estimation algorithms. Our main contributions are: first, the novel combination of a state-of-the-art MAP criterion for dominant motion estimation with a search procedure that guarantees global optimality. Second, experimental results that illustrate the superior performance of our approach on synthetic flow fields as well as real-world video streams. Third, a significant speedup of the search achieved by extending the model with an additional smoothness prior.}, author = {Ulges, Adrian and Christoph Lampert and Keysers,Daniel and Breuel,Thomas M}, pages = {204 -- 213}, publisher = {Springer}, title = {{Optimal dominant motion estimation using adaptive search of transformation space}}, doi = {10.1007/978-3-540-74936-3_21}, volume = {4713}, year = {2007}, } @techreport{3687, abstract = {Recent years have seen huge advances in object recognition from images. Recognition rates beyond 95% are the rule rather than the exception on many datasets. However, most state-of-the-art methods can only decide if an object is present or not. They are not able to provide information on the object location or extent within in the image. We report on a simple yet powerful scheme that extends many existing recognition methods to also perform localization of object bounding boxes. This is achieved by maximizing the classification score over all possible subrectangles in the image. Despite the impression that this would be computationally intractable, we show that in many situations efficient algorithms exist which solve a generalized maximum subrectangle problem. We show how our method is applicable to a variety object detection frameworks and demonstrate its performance by applying it to the popular bag of visual words model, achieving competitive results on the PASCAL VOC 2006 dataset.}, author = {Blaschko,Matthew B and Hofmann,Thomas and Christoph Lampert}, booktitle = {Unknown}, number = {164}, publisher = {Max-Planck-Institute for Biological Cybernetics}, title = {{Efficient subwindow search for object localization}}, year = {2007}, } @inproceedings{3701, abstract = {The extraction of a parametric global motion from a motion field is a task with several applications in video processing. We present two probabilistic formulations of the problem and carry out optimization using the RAST algorithm, a geometric matching method novel to motion estimation in video. RAST uses an exhaustive and adaptive search of transformation space and thus gives – in contrast to local sampling optimization techniques used in the past – a globally optimal solution. Among other applications, our framework can thus be used as a source of ground truth for benchmarking motion estimation algorithms. Our main contributions are: first, the novel combination of a state-of-the-art MAP criterion for dominant motion estimation with a search procedure that guarantees global optimality. Second, experimental results that illustrate the superior performance of our approach on synthetic flow fields as well as real-world video streams. Third, a significant speedup of the search achieved by extending the model with an additional smoothness prior.}, author = {Ulges, Adrian and Christoph Lampert and Keysers,Daniel and Breuel,Thomas M}, pages = {204 -- 213}, publisher = {Springer}, title = {{Optimal dominant motion estimation using adaptive search of transformation space}}, doi = {10.1007/978-3-540-74936-3_21}, volume = {4713}, year = {2007}, } @article{9524, abstract = {Cytosine methylation is the most common covalent modification of DNA in eukaryotes. DNA methylation has an important role in many aspects of biology, including development and disease. Methylation can be detected using bisulfite conversion, methylation-sensitive restriction enzymes, methyl-binding proteins and anti-methylcytosine antibodies. Combining these techniques with DNA microarrays and high-throughput sequencing has made the mapping of DNA methylation feasible on a genome-wide scale. Here we discuss recent developments and future directions for identifying and mapping methylation, in an effort to help colleagues to identify the approaches that best serve their research interests.}, author = {ZILBERMAN, Daniel and Henikoff, Steven}, issn = {1477-9129}, journal = {Development}, number = {22}, pages = {3959--3965}, publisher = {The Company of Biologists}, title = {{Genome-wide analysis of DNA methylation patterns}}, doi = {10.1242/dev.001131}, volume = {134}, year = {2007}, } @misc{9504, author = {ZILBERMAN, Daniel}, booktitle = {Nature Genetics}, issn = {1546-1718}, number = {4}, pages = {442--443}, publisher = {Nature Publishing Group}, title = {{The human promoter methylome}}, doi = {10.1038/ng0407-442}, volume = {39}, year = {2007}, } @article{9487, abstract = {Cytosine DNA methylation is considered to be a stable epigenetic mark, but active demethylation has been observed in both plants and animals. In Arabidopsis thaliana, DNA glycosylases of the DEMETER (DME) family remove methylcytosines from DNA. Demethylation by DME is necessary for genomic imprinting, and demethylation by a related protein, REPRESSOR OF SILENCING1, prevents gene silencing in a transgenic background. However, the extent and function of demethylation by DEMETER-LIKE (DML) proteins in WT plants is not known. Using genome-tiling microarrays, we mapped DNA methylation in mutant and WT plants and identified 179 loci actively demethylated by DML enzymes. Mutations in DML genes lead to locus-specific DNA hypermethylation. Reintroducing WT DML genes restores most loci to the normal pattern of methylation, although at some loci, hypermethylated epialleles persist. Of loci demethylated by DML enzymes, >80% are near or overlap genes. Genic demethylation by DML enzymes primarily occurs at the 5′ and 3′ ends, a pattern opposite to the overall distribution of WT DNA methylation. Our results show that demethylation by DML DNA glycosylases edits the patterns of DNA methylation within the Arabidopsis genome to protect genes from potentially deleterious methylation.}, author = {Penterman, Jon and ZILBERMAN, Daniel and Huh, Jin Hoe and Ballinger, Tracy and Henikoff, Steven and Fischer, Robert L.}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, number = {16}, pages = {6752--6757}, publisher = {National Academy of Sciences}, title = {{DNA demethylation in the Arabidopsis genome}}, doi = {10.1073/pnas.0701861104}, volume = {104}, year = {2007}, } @inproceedings{2333, author = {Lieb, Élliott H and Robert Seiringer and Solovej, Jan P}, pages = {239 -- 248}, publisher = {American Mathematical Society}, title = {{Ground-state energy of a dilute Fermi gas}}, doi = {10.1090/conm/412}, volume = {412}, year = {2006}, } @inproceedings{2334, author = {Robert Seiringer and Lieb, Élliott H and Yngvason, Jakob}, editor = {Zambrini, Jean-Claude}, publisher = {World Scientific Publishing}, title = {{One-dimensional behavior of dilute, trapped Bose gases in traps}}, doi = {10.1007/s00220-003-0993-3}, year = {2006}, } @misc{2363, abstract = { We prove that the Gross-Pitaevskii equation correctly describes the ground state energy and corresponding one-particle density matrix of rotating, dilute, trapped Bose gases with repulsive two-body interactions. We also show that there is 100% Bose-Einstein condensation. While a proof that the GP equation correctly describes non-rotating or slowly rotating gases was known for some time, the rapidly rotating case was unclear because the Bose (i.e., symmetric) ground state is not the lowest eigenstate of the Hamiltonian in this case. We have been able to overcome this difficulty with the aid of coherent states. Our proof also conceptually simplifies the previous proof for the slowly rotating case. In the case of axially symmetric traps, our results show that the appearance of quantized vortices causes spontaneous symmetry breaking in the ground state. }, author = {Lieb, Élliott H and Robert Seiringer}, booktitle = {Communications in Mathematical Physics}, number = {2}, pages = {505 -- 537}, publisher = {Springer}, title = {{Derivation of the Gross-Pitaevskii equation for rotating Bose gases}}, doi = {10.1007/s00220-006-1524-9}, volume = {264}, year = {2006}, } @article{2364, abstract = {We present an inequality that gives a lower bound on the expectation value of certain two-body interaction potentials in a general state on Fock space in terms of the corresponding expectation value for thermal equilibrium states of non-interacting systems and the difference in the free energy. This bound can be viewed as a rigorous version of first-order perturbation theory for many-body systems at positive temperature. As an application, we give a proof of the first two terms in a high density (and high temperature) expansion of the free energy of jellium with Coulomb interactions, both in the fermionic and bosonic case. For bosons, our method works above the transition temperature (for the non-interacting gas) for Bose-Einstein condensation.}, author = {Robert Seiringer}, journal = {Reviews in Mathematical Physics}, number = {3}, pages = {233 -- 253}, publisher = {World Scientific Publishing}, title = {{A correlation estimate for quantum many-body systems at positive temperature}}, doi = {10.1142/S0129055X06002632}, volume = {18}, year = {2006}, } @article{2365, abstract = {We consider a gas of fermions with non-zero spin at temperature T and chemical potential μ. We show that if the range of the interparticle interaction is small compared to the mean particle distance, the thermodynamic pressure differs to leading order from the corresponding expression for non-interacting particles by a term proportional to the scattering length of the interparticle interaction. This is true for any repulsive interaction, including hard cores. The result is uniform in the temperature as long as T is of the same order as the Fermi temperature, or smaller.}, author = {Robert Seiringer}, journal = {Communications in Mathematical Physics}, number = {3}, pages = {729 -- 757}, publisher = {Springer}, title = {{The thermodynamic pressure of a dilute fermi gas}}, doi = {10.1007/s00220-005-1433-3}, volume = {261}, year = {2006}, } @article{2366, abstract = {Inequalities are derived for power sums of the real part and the modulus of the eigenvalues of a Schrödinger operator with a complex-valued potential.}, author = {Frank, Rupert L and Laptev, Ari and Lieb, Élliott H and Robert Seiringer}, journal = {Letters in Mathematical Physics}, number = {3}, pages = {309 -- 316}, publisher = {Springer}, title = {{Lieb-Thirring inequalities for Schrödinger operators with complex-valued potentials}}, doi = {10.1007/s11005-006-0095-1}, volume = {77}, year = {2006}, } @inbook{2368, abstract = {The recent experimental success in creating Bose-Einstein condensates of alkali atoms, honored by the Nobel prize awards in 2001 [1,5], led to renewed interest in the mathematical description of interacting Bose gases.}, author = {Robert Seiringer}, booktitle = {Large Coulomb Systems}, editor = {Dereziński, Jan and Siedentop, Heinz}, pages = {249 -- 274}, publisher = {Springer}, title = {{Dilute, trapped Bose gases and Bose-Einstein condensation}}, doi = {10.1007/3-540-32579-4_6}, volume = {695}, year = {2006}, } @inbook{2369, abstract = {One of the most remarkable recent developments in the study of ultracold Bose gases is the observation of a reversible transition from a Bose Einstein condensate to a state composed of localized atoms as the strength of a periodic, optical trapping potential is varied. In [1] a model of this phenomenon has been analyzed rigorously. The gas is a hard core lattice gas and the optical lattice is modeled by a periodic potential of strength λ. For small λ and temperature Bose- Einstein condensation (BEC) is proved to occur, while at large λ BEC disappears, even in the ground state, which is a Mott-insulator state with a characteristic gap. The inter-particle interaction is essential for this effect. This contribution gives a pedagogical survey of these results.}, author = {Aizenman, Michael and Lieb, Élliott H and Robert Seiringer and Solovej, Jan P and Yngvason, Jakob}, booktitle = {Mathematical Physics of Quantum Mechanics}, editor = {Asch, Joachim and Joye, Alain}, pages = {199 -- 215}, publisher = {Springer}, title = {{Bose-Einstein condensation as a quantum phase transition in an optical lattice}}, doi = {10.1007/b11573432}, volume = {690}, year = {2006}, } @inbook{2416, author = {Bang-Jensen, Jørgen and Reed, Bruce and Schacht, Bruce and Šámal, Robert and Toft, Bjarne and Uli Wagner}, booktitle = {Topics in Discrete Mathematics}, pages = {613 -- 627}, publisher = {Springer}, title = {{On six problems posed by Jarik Nešetřil}}, doi = {10.1007/3-540-33700-8_30}, volume = {26}, year = {2006}, } @article{2429, abstract = {We show, with an elementary proof, that the number of halving simplices in a set of n points in 4 in general position is O(n4-2/45). This improves the previous bound of O(n4-1/134). Our main new ingredient is a bound on the maximum number of halving simplices intersecting a fixed 2-plane. }, author = {Matoušek, Jiří and Sharir, Micha and Smorodinsky, Shakhar and Uli Wagner}, journal = {Discrete & Computational Geometry}, number = {2}, pages = {177 -- 191}, publisher = {Springer}, title = {{K-sets in four dimensions}}, doi = {10.1007/s00454-005-1200-4}, volume = {35}, year = {2006}, } @article{2430, abstract = {We consider an online version of the conflict-free coloring of a set of points on the line, where each newly inserted point must be assigned a color upon insertion, and at all times the coloring has to be conflict-free, in the sense that in every interval I there is a color that appears exactly once in I. We present deterministic and randomized algorithms for achieving this goal, and analyze their performance, that is, the maximum number of colors that they need to use, as a function of the number n of inserted points. We first show that a natural and simple (deterministic) approach may perform rather poorly, requiring Ω(√̃) colors in the worst case. We then derive two efficient variants of this simple algorithm. The first is deterministic and uses O(log 2 n) colors, and the second is randomized and uses O(log n) colors with high probability. We also show that the O(log 2 n) bound on the number of colors used by our deterministic algorithm is tight on the worst case. We also analyze the performance of the simplest proposed algorithm when the points are inserted in a random order and present an incomplete analysis that indicates that, with high probability, it uses only O(log n) colors. Finally, we show that in the extension of this problem to two dimensions, where the relevant ranges are disks, n colors may be required in the worst case.}, author = {Chent, Ke and Fiat, Amos and Kaplan, Haim and Levy, Meital B and Matoušek, Jiří and Mossel, Elchanan and Pach, János and Sharir, Micha and Smorodinsky, Shakhar and Uli Wagner and Welzl, Emo}, journal = {SIAM Journal on Computing}, number = {5}, pages = {1342 -- 1359}, publisher = {SIAM}, title = {{Online conflict-free coloring for intervals}}, doi = {10.1137/S0097539704446682}, volume = {36}, year = {2006}, } @inproceedings{2431, abstract = {We prove an upper bound, tight up to a factor of 2, for the number of vertices of level at most t in an arrangement of n halfspaces in R , for arbitrary n and d (in particular, the dimension d is not considered constant). This partially settles a conjecture of Eckhoff, Linhart, and Welzl. Up to the factor of 2, the result generalizes McMullen's Upper Bound Theorem for convex polytopes (the case ℓ = O) and extends a theorem of Linhart for the case d ≤ 4. Moreover, the bound sharpens asymptotic estimates obtained by Clarkson and Shor. The proof is based on the h-matrix of the arrangement (a generalization, introduced by Mulmuley, of the h-vector of a convex polytope). We show that bounding appropriate sums of entries of this matrix reduces to a lemma about quadrupels of sets with certain intersection properties, and we prove this lemma, up to a factor of 2, using tools from multilinear algebra. This extends an approach of Alon and Kalai, who used linear algebra methods for an alternative proof of the classical Upper Bound Theorem. The bounds for the entries of the h-matrix also imply bounds for the number of i-dimensional faces, i > 0, at level at most ℓ. Furthermore, we discuss a connection with crossing numbers of graphs that was one of the main motivations for investigating exact bounds that are valid for arbitrary dimensions.}, author = {Uli Wagner}, pages = {635 -- 645}, publisher = {IEEE}, title = {{On a geometric generalization of the Upper Bound Theorem}}, doi = {10.1109/FOCS.2006.53}, year = {2006}, } @article{2657, abstract = {The highest densities of the two metabotropic GABA subunits, GABA B1 and GABAB2, have been reported as occurring around the glutamatergic synapses between Purkinje cell spines and parallel fibre varicosities. In order to determine how this distribution is achieved during development, we investigated the expression pattern and the cellular and subcellular localization of the GABAB1 and GABAB2 subunits in the rat cerebellum during postnatal development. At the light microscopic level, immunoreactivity for the GABAB1 and GABAB2 subunits was very prominent in the developing molecular layer, especially in Purkinje cells. Using double immunofluorescence, we demonstrated that GABAB1 was transiently expressed in glial cells. At the electron microscopic level, immunoreactivity for GABAB receptors was always detected both pre- and postsynaptically. Presynaptically, GABAB1 and GABAB2 were localized in the extrasynaptic membrane of parallel fibres at all ages, and only rarely in GABAergic axons. Postsynaptically, GABAB receptors were localized to the extrasynaptic and perisynaptic plasma membrane of Purkinje cell dendrites and spines throughout development. Quantitative analysis and three-dimensional reconstructions further revealed a progressive developmental movement of the GABAB1 subunit on the surface of Purkinje cells from dendritic shafts to its final destination, the dendritic spines. Together, these results indicate that GABAB receptors undergo dynamic regulation during cerebellar development in association with the establishment and maturation of glutamatergic synapses to Purkinje cells.}, author = {Luján, Rafael and Ryuichi Shigemoto}, journal = {European Journal of Neuroscience}, number = {6}, pages = {1479 -- 1490}, publisher = {Wiley-Blackwell}, title = {{Localization of metabotropic GABA receptor subunits GABAB1 and GABAB2 relative to synaptic sites in the rat developing cerebellum}}, doi = {10.1111/j.1460-9568.2006.04669.x}, volume = {23}, year = {2006}, } @article{2659, abstract = {Transmembrane AMPA receptor regulatory proteins (TARPs), including stargazin/γ-2, are associated with AMPA receptors and participate in their surface delivery and anchoring at the postsynaptic membrane. TARPs may also act as a positive modulator of the AMPA receptor ion channel function; however, little is known about other TARP members except for stargazin/γ-2. We examined the synaptic localization of stargazin/γ-2 and γ-8 by immunoelectron microscopy and biochemical analysis. The analysis of sodium dodecyl sulfate-digested freeze-fracture replica labeling revealed that stargazin/γ-2 was concentrated in the postsynaptic area, whereas γ-8 was distributed both in synaptic and extra-synaptic plasma membranes of the hippocampal neuron. When a synaptic plasma membrane-enriched brain fraction was treated with Triton X-100 and separated by sucrose density gradient ultracentrifugation, a large proportion of NMDA receptor and stargazin/γ-2 was accumulated in raft-enriched fractions, whereas AMPA receptor and γ-8 were distributed in both the raft-enriched fractions and other Triton-insoluble fractions. Phosphorylation of stargazin/γ-2 and γ-8 was regulated by different sets of kinases and phosphatases in cultured cortical neurons. These results suggested that stargazin/γ-2 and γ-8 have distinct roles in postsynaptic membranes under the regulation of different intracellular signaling pathways.}, author = {Inamura, Mihoko and Itakura, Makoto and Okamoto, Hirotsugu and Hoka, Sumio and Mizoguchi, Akira and Fukazawa, Yugo and Ryuichi Shigemoto and Yamamori, Saori and Takahashi, Masami}, journal = {Neuroscience Research}, number = {1}, pages = {45 -- 53}, publisher = {Elsevier}, title = {{ Differential localization and regulation of stargazin-like protein, γ-8 and stargazin in the plasma membrane of hippocampal and cortical neurons}}, doi = {10.1016/j.neures.2006.01.004}, volume = {55}, year = {2006}, } @article{2660, abstract = {Pavlovian fear conditioning, a simple form of associative learning, is thought to involve the induction of associative, NMDA receptor-dependent long-term potentiation (LTP) in the lateral amygdala. Using a combined genetic and electrophysiological approach, we show here that lack of a specific GABAB receptor subtype, GABAB(1a,2), unmasks a nonassociative, NMDA receptor-independent form of presynaptic LTP at cortico-amygdala afferents. Moreover, the level of presynaptic GABA B(1a,2) receptor activation, and hence the balance between associative and nonassociative forms of LTP, can be dynamically modulated by local inhibitory activity. At the behavioral level, genetic loss of GABA B(1a) results in a generalization of conditioned fear to nonconditioned stimuli. Our findings indicate that presynaptic inhibition through GABAB(1a,2) receptors serves as an activity-dependent constraint on the induction of homosynaptic plasticity, which may be important to prevent the generalization of conditioned fear.}, author = {Shaban, Hamdy and Humeau, Yann and Herry, Cyril and Cassasus, Guillaume and Ryuichi Shigemoto and Ciocchi, Stéphane and Barbieri, Samuel and Van Der Putten, Herman V and Kaupmann, Klemens and Bettler, Bernhard and Lüthi, Andreas}, journal = {Nature Neuroscience}, number = {8}, pages = {1028 -- 1035}, publisher = {Nature Publishing Group}, title = {{Generalization of amygdala LTP and conditioned fear in the absence of presynaptic inhibition}}, doi = {10.1038/nn1732}, volume = {9}, year = {2006}, } @article{2661, abstract = {GABAB receptors are the G protein-coupled receptors for the main inhibitory neurotransmitter in the brain, γ-aminobutyric acid (GABA). Molecular diversity in the GABAB system arises from the GABAB1a and GABAB1b subunit isoforms that solely differ in their ectodomains by a pair of sushi repeats that is unique to GABAB1a. Using a combined genetic, physiological, and morphological approach, we now demonstrate that GABAB1 isoforms localize to distinct synaptic sites and convey separate functions in vivo. At hippocampal CA3-to-CA1 synapses, GABAB1a assembles heteroreceptors inhibiting glutamate release, while predominantly GABAB1b mediates postsynaptic inhibition. Electron microscopy reveals a synaptic distribution of GABAB1 isoforms that agrees with the observed functional differences. Transfected CA3 neurons selectively express GABAB1a in distal axons, suggesting that the sushi repeats, a conserved protein interaction motif, specify heteroreceptor localization. The constitutive absence of GABAB1a but not GABAB1b results in impaired synaptic plasticity and hippocampus-dependent memory, emphasizing molecular differences in synaptic GABAB functions.}, author = {Vigot, Réjan and Barbieri, Samuel and Bräuner-Osborne, Hans and Tureček, Rostislav and Ryuichi Shigemoto and Zhang, Yan Ping and Luján, Rafael and Jacobson, Laura H and Biermann, Barbara and Fritschy, Jean-Marc and Vacher, Claire-Marie and Müller, Matthias P and Sansig, Gilles and Guetg, Nicole and Cryan, John F and Kaupmann, Klemens and Gassmann, Martin and Oertner, Thomas G and Bettler, Bernhard}, journal = {Neuron}, number = {4}, pages = {589 -- 601}, publisher = {Elsevier}, title = {{Differential Compartmentalization and Distinct Functions of GABAB Receptor Variants}}, doi = {10.1016/j.neuron.2006.04.014}, volume = {50}, year = {2006}, } @article{2662, abstract = {G-protein-coupled inwardly rectifying K+ channels (Kir3 channels) coupled to metabotropic GABAB receptors are essential for the control of neuronal excitation. To determine the distribution of Kir3 channels and their spatial relationship to GABAB receptors on hippocampal pyramidal cells, we used a high-resolution immunocytochemical approach. Immunoreactivity for the Kir3.2 subunit was most abundant postsynaptically and localized to the extrasynaptic plasma membrane of dendritic shafts and spines of principal cells. Quantitative analysis of immunogold particles for Kir3.2 revealed an enrichment of the protein around putative glutamatergic synapses on dendritic spines, similar to that of GABA B1. Consistent with this observation, a high degree of coclustering of Kir3.2 and GABAB1 was revealed around excitatory synapses by the highly sensitive SDS-digested freeze-fracture replica immunolabeling. In contrast, in dendritic shafts receptors and channels were found to be mainly segregated. These results suggest that Kir3.2-containing K+ channels on dendritic spines preferentially mediate the effect of GABA, whereas channels on dendritic shafts are likely to be activated by other neurotransmitters as well. Thus, Kir3 channels, localized to different subcellular compartments of hippocampal principal cells, appear to be differentially involved in synaptic integration in pyramidal cell dendrites.}, author = {Kulik, Ákos and Vida, Imre and Fukazawa, Yugo and Guetg, Nicole and Kasugai, Yu and Marker, Cheryl L and Rigato, Franck and Bettler, Bernhard and Wickman, Kevin D and Frotscher, Michael and Ryuichi Shigemoto}, journal = {Journal of Neuroscience}, number = {16}, pages = {4289 -- 4297}, publisher = {Society for Neuroscience}, title = {{Compartment-dependent colocalization of Kir3.2-containing K+ channels and GABAB receptors in hippocampal pyramidal cells}}, doi = {10.1523/JNEUROSCI.4178-05.2006}, volume = {26}, year = {2006}, } @article{2663, abstract = {The rocker mice are hereditary ataxic mutants that carry a point mutation in the gene encoding the CaV2.1 (P/Q-type) Ca2+ channel α1 subunit, and show the mildest symptoms among the reported CaV2.1 mutant mice. We studied the basic characteristics of the rocker mutant Ca2+ channel and their impacts on excitatory synaptic transmission in cerebellar Purkinje cells (PCs). In acutely dissociated PC somas, the rocker mutant channel showed a moderate reduction in Ca2+ channel current density, whereas its kinetics and voltage dependency of gating remained nearly normal. Despite the small changes in channel function, synaptic transmission in the parallel fiber (PF)-PC synapses was severely impaired. The climbing fiber inputs onto PCs showed a moderate impairment but could elicit normal complex spikes. Presynaptic function of the PF-PC synapses, however, was unexpectedly almost normal in terms of paired-pulse facilitation, sensitivity to extracellular Ca2+ concentration and glutamate concentration in synaptic clefts. Electron microscopic analyses including freeze-fracture replica labeling revealed that both the number and density of postsynaptic α-amino-3-hydroxy-5-methyl-4-isoxazolepropionic acid (AMPA) receptors substantially decreased without gross structural changes of the PF-PC synapses. We also observed an abnormal arborization of PC dendrites in young adult rocker mice (∼ 1 month old). These lines of evidence suggest that even a moderate dysfunction of CaV2.1 Ca2+ channel can cause substantial changes in postsynaptic molecular composition of the PF-PC synapses and dendritic structure of PCs.}, author = {Kodama, Takashi and Itsukaichi-Nishida, Yuko and Fukazawa, Yugo and Wakamori, Minoru and Miyata, Mariko and Molnár, Elek and Mori, Yasuo and Ryuichi Shigemoto and Imoto, Keiji}, journal = {European Journal of Neuroscience}, number = {11}, pages = {2993 -- 3007}, publisher = {Wiley-Blackwell}, title = {{A CaV2.1 calcium channel mutation rocker reduces the number of postsynaptic AMPA receptors in parallel fiber-Purkinje cell synapses}}, doi = {10.1111/j.1460-9568.2006.05191.x}, volume = {24}, year = {2006}, } @misc{2664, abstract = {Metabotropic glutamate receptors (mGlus) are a family of G-protein-coupled receptors activated by the neurotransmitter glutamate. Molecular cloning has revealed eight different subtypes (mGlu1-8) with distinct molecular and pharmacological properties. Multiplicity in this receptor family is further generated through alternative splicing. mGlus activate a multitude of signalling pathways important for modulating neuronal excitability, synaptic plasticity and feedback regulation of neurotransmitter release. In this review, we summarize anatomical findings (from our work and that of other laboratories) describing their distribution in the central nervous system. Recent evidence regarding the localization of these receptors in peripheral tissues will also be examined. The distinct regional, cellular and subcellular distribution of mGlus in the brain will be discussed in view of their relationship to neurotransmitter release sites and of possible functional implications.}, author = {Ferraguti, Francesco and Ryuichi Shigemoto}, booktitle = {Cell and Tissue Research}, number = {2}, pages = {483 -- 504}, publisher = {Springer}, title = {{Metabotropic glutamate receptors}}, doi = {10.1007/s00441-006-0266-5}, volume = {326}, year = {2006}, } @article{2745, abstract = {We consider the dynamics of N boson systems interacting through a pair potential N -1 V a (x i -x j ) where V a (x)=a -3 V(x/a). We denote the solution to the N-particle Schrödinger equation by Ψ N, t . Recall that the Gross-Pitaevskii (GP) equation is a nonlinear Schrödinger equation and the GP hierarchy is an infinite BBGKY hierarchy of equations so that if u t solves the GP equation, then the family of k-particle density matrices [InlineMediaObject not available: see fulltext.] solves the GP hierarchy. Under the assumption that a = Nε for 0 < ε < 3/5, we prove that as N→∞ the limit points of the k-particle density matrices of Ψ N, t are solutions of the GP hierarchy with the coupling constant in the nonlinear term of the GP equation given by ∫ V (x)dx. The uniqueness of the solutions of this hierarchy remains an open question.}, author = {Elgart, Alexander and László Erdös and Schlein, Benjamin and Yau, Horng-Tzer}, journal = {Archive for Rational Mechanics and Analysis}, number = {2}, pages = {265 -- 283}, publisher = {Springer}, title = {{Gross-Pitaevskii equation as the mean field limit of weakly coupled bosons}}, doi = {10.1007/s00205-005-0388-z}, volume = {179}, year = {2006}, } @inproceedings{2746, abstract = {We consider random Schrödinger equations on Rd or Zd for d ≥ 3 with uncorrelated, identically distributed random potential. Denote by λ the coupling constant and ψt the solution with initial data ψ0.}, author = {László Erdös and Salmhofer, Manfred and Yau, Horng-Tzer}, pages = {233 -- 257}, publisher = {World Scientific Publishing}, title = {{Towards the quantum Brownian motion}}, doi = {10.1007/3-540-34273-7_18}, volume = {690}, year = {2006}, } @article{2747, abstract = {Consider a system of N bosons on the three-dimensional unit torus interacting via a pair potential N 2V(N(x i - x j)) where x = (x i, . . ., x N) denotes the positions of the particles. Suppose that the initial data ψ N,0 satisfies the condition 〈ψ N,0, H 2 Nψ N,0) ≤ C N 2 where H N is the Hamiltonian of the Bose system. This condition is satisfied if ψ N,0 = W Nφ N,t where W N is an approximate ground state to H N and φ N,0 is regular. Let ψ N,t denote the solution to the Schrödinger equation with Hamiltonian H N. Gross and Pitaevskii proposed to model the dynamics of such a system by a nonlinear Schrödinger equation, the Gross-Pitaevskii (GP) equation. The GP hierarchy is an infinite BBGKY hierarchy of equations so that if u t solves the GP equation, then the family of k-particle density matrices ⊗ k |u t?〉 〈 t | solves the GP hierarchy. We prove that as N → ∞ the limit points of the k-particle density matrices of ψ N,t are solutions of the GP hierarchy. Our analysis requires that the N-boson dynamics be described by a modified Hamiltonian that cuts off the pair interactions whenever at least three particles come into a region with diameter much smaller than the typical interparticle distance. Our proof can be extended to a modified Hamiltonian that only forbids at least n particles from coming close together for any fixed n.}, author = {László Erdös and Schlein, Benjamin and Yau, Horng-Tzer}, journal = {Communications on Pure and Applied Mathematics}, number = {12}, pages = {1659 -- 1741}, publisher = {Wiley-Blackwell}, title = {{Derivation of the Gross-Pitaevskii hierarchy for the dynamics of Bose-Einstein condensate}}, doi = {10.1002/cpa.20123}, volume = {59}, year = {2006}, } @article{2791, abstract = {Generally, the motion of fluids is smooth and laminar at low speeds but becomes highly disordered and turbulent as the velocity increases. The transition from laminar to turbulent flow can involve a sequence of instabilities in which the system realizes progressively more complicated states, or it can occur suddenly. Once the transition has taken place, it is generally assumed that, under steady conditions, the turbulent state will persist indefinitely. The flow of a fluid down a straight pipe provides a ubiquitous example of a shear flow undergoing a sudden transition from laminar to turbulent motion. Extensive calculations and experimental studies have shown that, at relatively low flow rates, turbulence in pipes is transient, and is characterized by an exponential distribution of lifetimes. They also suggest that for Reynolds numbers exceeding a critical value the lifetime diverges (that is, becomes infinitely large), marking a change from transient to persistent turbulence. Here we present experimental data and numerical calculations covering more than two decades of lifetimes, showing that the lifetime does not in fact diverge but rather increases exponentially with the Reynolds number. This implies that turbulence in pipes is only a transient event (contrary to the commonly accepted view), and that the turbulent and laminar states remain dynamically connected, suggesting avenues for turbulence control.}, author = {Björn Hof and Westerweel, Jerry and Schneider, Tobias M and Eckhardt, Bruno}, journal = {Nature}, number = {7107}, pages = {59 -- 62}, publisher = {Nature Publishing Group}, title = {{Finite lifetime of turbulence in shear flows}}, doi = {10.1038/nature05089}, volume = {443}, year = {2006}, } @article{2792, abstract = {Transition to turbulence in pipe flow has posed a riddle in fluid dynamics since the pioneering experiments of Reynolds[1]. Although the laminar flow is linearly stable for all flow rates, practical pipe flows become turbulent at large enough flow speeds. Turbulence arises suddenly and fully without distinct steps and without a clear critical point. The complexity of this problem has puzzled mathematicians, physicists and engineers for more than a century and no satisfactory explanation of this problem has been given. In a very recent theoretical approach it has been suggested that unstable solutions of the Navier Stokes equations may hold the key to understanding this problem. In numerical studies such unstable states have been identified as exact solutions for the idealized case of a pipe with periodic boundary conditions[2, 3]. These solutions have the form of waves extending through the entire pipe and travelling in the streamwise direction at a phase speed close to the bulk velocity of the fluid. With the aid of a recently developed high-speed stereoscopic Particle Image Velocimetry (PIV) system, we were able to observe transients of such unstable solutions in turbulent pipe flow[4].}, author = {Björn Hof and van Doorne, Casimir W and Westerweel, Jerry and Nieuwstadt, Frans T}, journal = {Fluid Mechanics and its Applications}, pages = {109 -- 114}, publisher = {Springer}, title = {{Observation of nonlinear travelling waves in turbulent pipe flow}}, doi = {10.1007/1-4020-4159-4_11}, volume = {78}, year = {2006}, } @article{2894, abstract = {IL-10 is a potent anti-inflammatory and immunomodulatory cytokine, exerting major effects in the degree and quality of the immune response. Using a newly generated IL-10 reporter mouse model, which easily allows the study of IL-10 expression from each allele in a single cell, we report here for the first time that IL-10 is predominantly monoallelic expressed in CD4+ T cells. Furthermore, we have compelling evidence that this expression pattern is not due to parental imprinting, allelic exclusion, or strong allelic bias. Instead, our results support a stochastic regulation mechanism, in which the probability to initiate allelic transcription depends on the strength of TCR signaling and subsequent capacity to overcome restrictions imposed by chromatin hypoacetylation. In vivo Ag-experienced T cells show a higher basal probability to transcribe IL-10 when compared with naive cells, yet still show mostly monoallelic IL-10 expression. Finally, statistical analysis on allelic expression data shows transcriptional independence between both alleles. We conclude that CD4+ T cells have a low probability for IL-10 allelic activation resulting in a predominantly monoallelic expression pattern, and that IL-10 expression appears to be stochastically regulated by controlling the frequency of expressing cells, rather than absolute protein levels per cell.}, author = {Calado, Dinis P and Tiago Paixao and Holmberg, Dan and Haury, Matthias}, journal = {Journal of Immunology}, number = {8}, pages = {5358 -- 5364}, publisher = {American Association of Immunologists}, title = {{Stochastic Monoallelic Expression of IL 10 in T Cells}}, doi = {10.4049/jimmunol.177.8.5358 }, volume = {177}, year = {2006}, } @inbook{2921, abstract = {Most binocular stereo algorithms assume that all scene elements are visible from both cameras. Scene elements that are visible from only one camera, known as occlusions, pose an important challenge for stereo. Occlusions are important for segmentation, because they appear near discontinuities. However, stereo algorithms tend to ignore occlusions because of their difficulty. One reason is that occlusions require the input images to be treated symmetrically, which complicates the problem formulation. Worse, certain depth maps imply physically impossible scene configurations, and must be excluded from the output. In this chapter we approach the problem of binocular stereo with occlusions from an energy minimization viewpoint. We begin by reviewing traditional stereo methods that do not handle occlusions. If occlusions are ignored, it is easy to formulate the stereo problem as a pixel labeling problem, which leads to an energy function that is common in early vision. This kind of energy function can he minimized using graph cuts, which is a combinatorial optimization technique that has proven to be very effective for low-level vision problems. Motivated by this, we have designed two graph cut stereo algorithms that are designed to handle occlusions. These algorithms produce promising experimental results on real data with ground truth.}, author = {Vladimir Kolmogorov and Zabih, Ramin}, booktitle = {Handbook of Mathematical Models in Computer Vision}, pages = {423 -- 427}, publisher = {Springer}, title = {{Graph cut algorithms for binocular stereo with occlusions}}, doi = {10.1007/0-387-28831-7_26}, year = {2006}, } @article{8488, abstract = {We demonstrate for different protein samples that three-dimensional HNCO and HNCA correlation spectra may be recorded in a few minutes acquisition time using the band-selective excitation short-transient sequences presented here. This opens new perspectives for the NMR structural investigation of unstable protein samples and real-time site-resolved studies of protein kinetics.}, author = {Schanda, Paul and Van Melckebeke, Hélène and Brutscher, Bernhard}, issn = {0002-7863}, journal = {Journal of the American Chemical Society}, keywords = {Colloid and Surface Chemistry, Biochemistry, General Chemistry, Catalysis}, number = {28}, pages = {9042--9043}, publisher = {American Chemical Society}, title = {{Speeding up three-dimensional protein NMR experiments to a few minutes}}, doi = {10.1021/ja062025p}, volume = {128}, year = {2006}, } @article{8489, abstract = {Structure elucidation of proteins by either NMR or X‐ray crystallography often requires the screening of a large number of samples for promising protein constructs and optimum solution conditions. For large‐scale screening of protein samples in solution, robust methods are needed that allow a rapid assessment of the folding of a polypeptide under diverse sample conditions. Here we present HET‐SOFAST NMR, a highly sensitive new method for semi‐quantitative characterization of the structural compactness and heterogeneity of polypeptide chains in solution. On the basis of one‐dimensional 1H HET‐SOFAST NMR data, obtained on well‐folded, molten globular, partially‐ and completely unfolded proteins, we define empirical thresholds that can be used as quantitative benchmarks for protein compactness. For 15N‐enriched protein samples, two‐dimensional 1H‐15N HET‐SOFAST correlation spectra provide site‐specific information about the structural heterogeneity along the polypeptide chain.}, author = {Schanda, Paul and Forge, Vincent and Brutscher, Bernhard}, issn = {0749-1581}, journal = {Magnetic Resonance in Chemistry}, number = {S1}, pages = {S177--S184}, publisher = {Wiley}, title = {{HET-SOFAST NMR for fast detection of structural compactness and heterogeneity along polypeptide chains}}, doi = {10.1002/mrc.1825}, volume = {44}, year = {2006}, } @article{8490, abstract = {We demonstrate the feasibility of recording 1H–15N correlation spectra of proteins in only one second of acquisition time. The experiment combines recently proposed SOFAST-HMQC with Hadamard-type 15N frequency encoding. This allows site-resolved real-time NMR studies of kinetic processes in proteins with an increased time resolution. The sensitivity of the experiment is sufficient to be applicable to a wide range of molecular systems available at millimolar concentration on a high magnetic field spectrometer.}, author = {Schanda, Paul and Brutscher, Bernhard}, issn = {1090-7807}, journal = {Journal of Magnetic Resonance}, keywords = {Nuclear and High Energy Physics, Biophysics, Biochemistry, Condensed Matter Physics}, number = {2}, pages = {334--339}, publisher = {Elsevier}, title = {{Hadamard frequency-encoded SOFAST-HMQC for ultrafast two-dimensional protein NMR}}, doi = {10.1016/j.jmr.2005.10.007}, volume = {178}, year = {2006}, } @article{8513, author = {Kaloshin, Vadim and Saprykina, Maria}, issn = {1553-5231}, journal = {Discrete & Continuous Dynamical Systems - A}, number = {2}, pages = {611--640}, publisher = {American Institute of Mathematical Sciences (AIMS)}, title = {{Generic 3-dimensional volume-preserving diffeomorphisms with superexponential growth of number of periodic orbits}}, doi = {10.3934/dcds.2006.15.611}, volume = {15}, year = {2006}, } @article{8514, abstract = {We study the extent to which the Hausdorff dimension of a compact subset of an infinite-dimensional Banach space is affected by a typical mapping into a finite-dimensional space. It is possible that the dimension drops under all such mappings, but the amount by which it typically drops is controlled by the ‘thickness exponent’ of the set, which was defined by Hunt and Kaloshin (Nonlinearity12 (1999), 1263–1275). More precisely, let $X$ be a compact subset of a Banach space $B$ with thickness exponent $\tau$ and Hausdorff dimension $d$. Let $M$ be any subspace of the (locally) Lipschitz functions from $B$ to $\mathbb{R}^{m}$ that contains the space of bounded linear functions. We prove that for almost every (in the sense of prevalence) function $f \in M$, the Hausdorff dimension of $f(X)$ is at least $\min\{ m, d / (1 + \tau) \}$. We also prove an analogous result for a certain part of the dimension spectra of Borel probability measures supported on $X$. The factor $1 / (1 + \tau)$ can be improved to $1 / (1 + \tau / 2)$ if $B$ is a Hilbert space. Since dimension cannot increase under a (locally) Lipschitz function, these theorems become dimension preservation results when $\tau = 0$. We conjecture that many of the attractors associated with the evolution equations of mathematical physics have thickness exponent zero. We also discuss the sharpness of our results in the case $\tau > 0$.}, author = {OTT, WILLIAM and HUNT, BRIAN and Kaloshin, Vadim}, issn = {0143-3857}, journal = {Ergodic Theory and Dynamical Systems}, number = {3}, pages = {869--891}, publisher = {Cambridge University Press}, title = {{The effect of projections on fractal sets and measures in Banach spaces}}, doi = {10.1017/s0143385705000714}, volume = {26}, year = {2006}, } @inproceedings{8515, abstract = {We consider the evolution of a set carried by a space periodic incompressible stochastic flow in a Euclidean space. We report on three main results obtained in [8, 9, 10] concerning long time behaviour for a typical realization of the stochastic flow. First, at time t most of the particles are at a distance of order √t away from the origin. Moreover, we prove a Central Limit Theorem for the evolution of a measure carried by the flow, which holds for almost every realization of the flow. Second, we show the existence of a zero measure full Hausdorff dimension set of points, which escape to infinity at a linear rate. Third, in the 2-dimensional case, we study the set of points visited by the original set by time t. Such a set, when scaled down by the factor of t, has a limiting non random shape.}, author = {Kaloshin, Vadim and DOLGOPYAT, D. and KORALOV, L.}, booktitle = {XIVth International Congress on Mathematical Physics}, isbn = {9789812562012}, location = {Lisbon, Portugal}, pages = {290--295}, publisher = {World Scientific}, title = {{Long time behaviour of periodic stochastic flows}}, doi = {10.1142/9789812704016_0026}, year = {2006}, } @article{854, abstract = {Phylogenetic relationships between the extinct woolly mammoth (Mammuthus primigenius), and the Asian (Elephas maximus) and African savanna (Loxodonta africana) elephants remain unresolved. Here, we report the sequence of the complete mitochondrial genome (16,842 base pairs) of a woolly mammoth extracted from permafrost-preserved remains from the Pleistocene epoch - the oldest mitochondrial genome sequence determined to date. We demonstrate that well-preserved mitochondrial genome fragments, as long as ∼1,600-1700 base pairs, can be retrieved from pre-Holocene remains of an extinct species. Phylogenetic reconstruction of the Elephantinae clade suggests that M. primigenius and E. maximus are sister species that diverged soon after their common ancestor split from the L. africana lineage. Low nucleotide diversity found between independently determined mitochondrial genomic sequences of woolly mammoths separated geographically and in time suggests that north-eastern Siberia was occupied by a relatively homogeneous population of M. primigenius throughout the late Pleistocene.}, author = {Rogaev, Evgeny I and Moliaka, Yuri K and Malyarchuk, Boris A and Fyodor Kondrashov and Derenko, Miroslava V and Chumakov, Ilya M and Grigorenko, Anastasia P}, journal = {PLoS Biology}, number = {3}, pages = {0403 -- 0410}, publisher = {Public Library of Science}, title = {{Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus primigenius}}, doi = {10.1371/journal.pbio.0040073}, volume = {4}, year = {2006}, } @article{868, abstract = {Background: The glyoxylate cycle is thought to be present in bacteria, protists, plants, fungi, and nematodes, but not in other Metazoa. However, activity of the glyoxylate cycle enzymes, malate synthase (MS) and isocitrate lyase (ICL), in animal tissues has been reported. In order to clarify the status of the MS and ICL genes in animals and get an insight into their evolution, we undertook a comparative-genomic study. Results: Using sequence similarity searches, we identified MS genes in arthropods, echinoderms, and vertebrates, including platypus and opossum, but not in the numerous sequenced genomes of placental mammals. The regions of the placental mammals' genomes expected to code for malate synthase, as determined by comparison of the gene orders in vertebrate genomes, show clear similarity to the opossum MS sequence but contain stop codons, indicating that the MS gene became a pseudogene in placental mammals. By contrast, the ICL gene is undetectable in animals other than the nematodes that possess a bifunctional, fused ICL-MS gene. Examination of phylogenetic trees of MS and ICL suggests multiple horizontal gene transfer events that probably went in both directions between several bacterial and eukaryotic lineages. The strongest evidence was obtained for the acquisition of the bifunctional ICL-MS gene from an as yet unknown bacterial source with the corresponding operonic organization by the common ancestor of the nematodes. Conclusion: The distribution of the MS and ICL genes in animals suggests that either they encode alternative enzymes of the glyoxylate cycle that are not orthologous to the known MS and ICL or the animal MS acquired a new function that remains to be characterized. Regardless of the ultimate solution to this conundrum, the genes for the glyoxylate cycle enzymes present a remarkable variety of evolutionary events including unusual horizontal gene transfer from bacteria to animals.}, author = {Fyodor Kondrashov and Koonin, Eugene V and Morgunov, Igor G and Finogenova, Tatiana V and Kondrashova, Marie N}, journal = {Biology Direct}, publisher = {BioMed Central}, title = {{Evolution of glyoxylate cycle enzymes in Metazoa Evidence of multiple horizontal transfer events and pseudogene formation}}, doi = {10.1186/1745-6150-1-31}, volume = {1}, year = {2006}, } @article{869, abstract = {The impact of synonymous nucleotide substitutions on fitness in mammals remains controversial. Despite some indications of selective constraint, synonymous sites are often assumed to be neutral, and the rate of their evolution is used as a proxy for mutation rate. We subdivide all sites into four classes in terms of the mutable CpG context, nonCpG, postC, preG, and postCpreG, and compare four-fold synonymous sites and intron sites residing outside transposable elements. The distribution of the rate of evolution across all synonymous sites is trimodal. Rate of evolution at nonCpG synonymous sites, not preceded by C and not followed by G, is ∼10% below that at such intron sites. In contrast, rate of evolution at postCpreG synonymous sites is ∼30% above that at such intron sites. Finally, synonymous and intron postC and preG sites evolve at similar rates. The relationship between the levels of polymorphism at the corresponding synonymous and intron sites is very similar to that between their rates of evolution. Within every class, synonymous sites are occupied by G or C much more often than intron sites, whose nucleotide composition is consistent with neutral mutation-drift equilibrium. These patterns suggest that synonymous sites are under weak selection in favor of G and C, with the average coefficient s∼0.25/Ne∼10-5, where Ne is the effective population size. Such selection decelerates evolution and reduces variability at sites with symmetric mutation, but has the opposite effects at sites where the favored nucleotides are more mutable. The amino-acid composition of proteins dictates that many synonymous sites are CpGprone, which causes them, on average, to evolve faster and to be more polymorphic than intron sites. An average genotype carries ∼107 suboptimal nucleotides at synonymous sites, implying synergistic epistasis in selection against them.}, author = {Fyodor Kondrashov and Ogurtsov, Aleksey Yu and Kondrashov, Alexey S}, journal = {Journal of Theoretical Biology}, number = {4}, pages = {616 -- 626}, publisher = {Elsevier}, title = {{Selection in favor of nucleotides G and C diversifies evolution rates and levels of polymorphism at mammalian synonymous sites}}, doi = {10.1016/j.jtbi.2005.10.020}, volume = {240}, year = {2006}, } @article{873, abstract = {New genes commonly appear through complete or partial duplications of pre-existing genes. Duplications of long DNA segments are constantly produced by rare mutations, may become fixed in a population by selection or random drift, and are subject to divergent evolution of the paralogous sequences after fixation, although gene conversion can impede this process. New data shed some light on each of these processes. Mutations which involve duplications can occur through at least two different mechanisms, backward strand slippage during DNA replication and unequal crossing-over. The background rate of duplication of a complete gene in humans is 10-9-10-10 per generation, although many genes located within hot-spots of large-scale mutation are duplicated much more often. Many gene duplications affect fitness strongly, and are responsible, through gene dosage effects, for a number of genetic diseases. However, high levels of intrapopulation polymorphism caused by presence or absence of long, gene-containing DNA segments imply that some duplications are not under strong selection. The polymorphism to fixation ratios appear to be approximately the same for gene duplications and for presumably selectively neutral nucleotide substitutions, which, according to the McDonald-Kreitman test, is consistent with selective neutrality of duplications. However, this pattern can also be due to negative selection against most of segregating duplications and positive selection for at least some duplications which become fixed. Patterns in post-fixation evolution of duplicated genes do not easily reveal the causes of fixations. Many gene duplications which became fixed recently in a variety of organisms were positively selected because the increased expression of the corresponding genes was beneficial. The effects of gene dosage provide a unified framework for studying all phases of the life history of a gene duplication. Application of well-known methods of evolutionary genetics to accumulating data on new, polymorphic, and fixed duplication will enhance our understanding of the role of natural selection in the evolution by gene duplication.}, author = {Fyodor Kondrashov and Kondrashov, Alexey S}, journal = {Journal of Theoretical Biology}, number = {2}, pages = {141 -- 151}, publisher = {Elsevier}, title = {{Role of selection in fixation of gene duplications}}, doi = {10.1016/j.jtbi.2005.08.033}, volume = {239}, year = {2006}, }