IST PubRep
Not a member yet
752 research outputs found
Sort by
Cell-to-cell variation and specialization in sugar metabolism in clonal bacterial populations
While we have good understanding of bacterial metabolism at the population level, we know little about the metabolic behavior of individual cells: do single cells in clonal populations sometimes specialize on different metabolic pathways? Such metabolic specialization could be driven by stochastic gene expression and could provide individual cells with growth benefits of specialization. We measured the degree of phenotypic specialization in two parallel metabolic pathways, the assimilation of glucose and arabinose. We grew Escherichia coli in chemostats, and used isotope-labeled sugars in combination with nanometer-scale secondary ion mass spectrometry and mathematical modeling to quantify sugar assimilation at the single-cell level. We found large variation in metabolic activities between single cells, both in absolute assimilation and in the degree to which individual cells specialize in the assimilation of different sugars. Analysis of transcriptional reporters indicated that this variation was at least partially based on cell-to-cell variation in gene expression. Metabolic differences between cells in clonal populations could potentially reduce metabolic incompatibilities between different pathways, and increase the rate at which parallel reactions can be performed
Counterexample-guided refinement of template Polyhedra
Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They have been employed in the abstract interpretation of programs and, with particular success, in the reachability analysis of hybrid automata.
While previously, the choice of directions has been left to the user or a heuristic, we present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. We show that for the class of convex hybrid automata, i.e., hybrid automata with (possibly nonlinear) convex constraints on derivatives, such directions always exist and can be found using convex optimization. We embed our method inside a CEGAR loop, thus enabling the time-unbounded reachability analysis of an important and richer class of hybrid automata than was previously possible. We evaluate our method on several benchmarks, demonstrating also its superior efficiency for the special case of linear hybrid automata
Plant biology: Building barriers… in roots
The Casparian strip is an important barrier regulating water and nutrient uptake into root tissues. New research reveals two peptide signals and their co-receptors play critical roles patterning and maintaining barrier integrity
Creating to understand – developmental biology meets engineering in Paris
In November 2016, developmental biologists, synthetic biologists and engineers gathered in Paris for a meeting called ‘Engineering the embryo’. The participants shared an interest in exploring how synthetic systems can reveal new principles of embryonic development, and how the in vitro manipulation and modeling of development using stem cells can be used to integrate ideas and expertise from physics, developmental biology and tissue engineering. As we review here, the conference pinpointed some of the challenges arising at the intersection of these fields, along with great enthusiasm for finding new approaches and collaborations
Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto-Sivashinsky system
Systems such as fluid flows in channels and pipes or the complex Ginzburg-Landau system, defined over periodic domains, exhibit both continuous symmetries, translational and rotational, as well as discrete symmetries under spatial reflections or complex conjugation. The simplest, and very common symmetry of this type is the equivariance of the defining equations under the orthogonal group O(2). We formulate a novel symmetry reduction scheme for such systems by combining the method of slices with invariant polynomial methods, and show how it works by applying it to the Kuramoto-Sivashinsky system in one spatial dimension. As an example, we track a relative periodic orbit through a sequence of bifurcations to the onset of chaos. Within the symmetry-reduced state space we are able to compute and visualize the unstable manifolds of relative periodic orbits, their torus bifurcations, a transition to chaos via torus breakdown, and heteroclinic connections between various relative periodic orbits. It would be very hard to carry through such analysis in the full state space, without a symmetry reduction such as the one we present here
Cell Adhesion and Cell Fate: An Effective Feedback Loop During Zebrafish Gastrulation
Cell-cell contact formation constitutes the first step in the emergence of multicellularity in evolution, thereby allowing the differentiation of specialized cell types. In metazoan development, cell-cell contact formation is thought to influence cell fate specification, and cell fate specification has been implicated in cell-cell contact formation. However, remarkably little is yet known about whether and how the interaction and feedback between cell-cell contact formation and cell fate specification affect development. Here we identify a positive feedback loop between cell-cell contact duration, morphogen signaling and mesendoderm cell fate specification during zebrafish gastrulation. We show that long lasting cell-cell contacts enhance the competence of prechordal plate (ppl) progenitor cells to respond to Nodal signaling, required for proper ppl cell fate specification. We further show that Nodal signalling promotes ppl cell-cell contact duration, thereby generating an effective positive feedback loop between ppl cell-cell contact duration and cell fate specification. Finally, by using a combination of theoretical modeling and experimentation, we show that this feedback loop determines whether anterior axial mesendoderm cells become ppl progenitors or, instead, turn into endoderm progenitors. Our findings reveal that the gene regulatory networks leading to cell fate diversification within the developing embryo are controlled by the interdependent activities of cell-cell signaling and contact formation
(The exact security of) Message Authentication Codes
In this thesis we discuss the exact security of message authentications codes HMAC,
NMAC, and PMAC. NMAC is a mode of operation which turns a fixed input-length keyed
hash function f into a variable input-length function. A practical single-key variant of
NMAC called HMAC is a very popular and widely deployed message authentication code
(MAC). PMAC is a block-cipher based mode of operation, which also happens to be the
most famous fully parallel MAC.
NMAC was introduced by Bellare, Canetti and Krawczyk Crypto’96, who proved it to
be a secure pseudorandom function (PRF), and thus also a MAC, under two assumptions.
Unfortunately, for many instantiations of HMAC one of them has been found to be wrong.
To restore the provable guarantees for NMAC, Bellare [Crypto’06] showed its security
without this assumption.
PMAC was introduced by Black and Rogaway at Eurocrypt 2002. If instantiated with
a pseudorandom permutation over n-bit strings, PMAC constitutes a provably secure
variable input-length PRF. For adversaries making q queries, each of length at most ` (in
n-bit blocks), and of total length σ ≤ q`, the original paper proves an upper bound on
the distinguishing advantage of O(σ 2 /2 n ), while the currently best bound is O(qσ/2 n ). In
this work we show that this bound is tight by giving an attack with advantage Ω(q 2 `/2 n ).
In the PMAC construction one initially XORs a mask to every message block, where the
mask for the ith block is computed as τ i := γ i · L, where L is a (secret) random value,
and γ i is the i-th codeword of the Gray code. Our attack applies more generally to any
sequence of γ i ’s which contains a large coset of a subgroup of GF (2 n ).
As for NMAC, our first contribution is a simpler and uniform proof: If f is an ε-secure
PRF (against q queries) and a δ-non-adaptively secure PRF (against q queries), then
NMAC f is an (ε + `qδ)-secure PRF against q queries of length at most ` blocks each. We
also show that this ε + `qδ bound is basically tight by constructing an f for which an
attack with advantage `qδ exists.
Moreover, we analyze the PRF-security of a modification of NMAC called NI by An and
Bellare that avoids the constant rekeying on multi-block messages in NMAC and allows
for an information-theoretic analysis. We carry out such an analysis, obtaining a tight
`q 2 /2 c bound for this step, improving over the trivial bound of ` 2 q 2 /2 c .
Finally, we investigate, if the security of PMAC can be further improved by using τ i ’s
that are k-wise independent, for k > 1 (the original has k = 1). We observe that the
security of PMAC will not increase in general if k = 2, and then prove that the security
increases to O(q 2 /2 n ), if the k = 4. Due to simple extension attacks, this is the best
bound one can hope for, using any distribution on the masks. Whether k = 3 is already
sufficient to get this level of security is left as an open problem
Timed Network Games
Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertex. The cost of traversing an edge depends on the number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in defining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, the traversal of the network involves an inherent delay, and so sharing and congestion of resources crucially depends on time. We study timed network games , which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. In addition, each edge has a guard, describing time intervals in which the edge can be traversed, forcing the players to spend time on vertices. Unlike earlier work that add a time component to network games, the time in our model is continuous and cannot be discretized. In particular, players have uncountably many strategies, and a game may have uncountably many pure Nash equilibria. We study properties of timed network games with cost-sharing or congestion cost functions: their stability, equilibrium inefficiency, and complexity. In particular, we show that the answer to the question whether we can restrict attention to boundary strategies, namely ones in which edges are traversed only at the boundaries of guards, is mixed
Investigations into cell polarity and trafficking in the plant model Arabidopsis thaliana
The thesis encompasses several topics of plant cell biology which were studied in the model plant Arabidopsis thaliana. Chapter 1 concerns the plant hormone auxin and its polar transport through cells and tissues. The highly controlled, directional transport of auxin is facilitated by plasma membrane-localized transporters. Transporters from the PIN family direct auxin transport due to their polarized localizations at cell membranes. Substantial effort has been put into research on cellular trafficking of PIN proteins, which is thought to underlie their polar distribution. I participated in a forward genetic screen aimed at identifying novel regulators of PIN polarity. The screen yielded several genes which may be involved in PIN polarity regulation or participate in polar auxin transport by other means.
Chapter 2 focuses on the endomembrane system, with particular attention to clathrin-mediated endocytosis. The project started with identification of several proteins that interact with clathrin light chains. Among them, I focused on two putative homologues of auxilin, which in non-plant systems is an endocytotic factor known for uncoating clathrin-coated vesicles in the final step of endocytosis. The body of my work consisted of an in-depth characterization of transgenic A. thaliana lines overexpressing these putative auxilins in an inducible manner. Overexpression of these proteins leads to an inhibition of endocytosis, as documented by imaging of cargoes and clathrin-related endocytic machinery. An extension of this work is an investigation into a concept of homeostatic regulation acting between distinct transport processes in the endomembrane system. With auxilin overexpressing lines, where endocytosis is blocked specifically, I made observations on the mutual relationship between two opposite trafficking processes of secretion and endocytosis.
In Chapter 3, I analyze cortical microtubule arrays and their relationship to auxin signaling and polarized growth in elongating cells. In plants, microtubules are organized into arrays just below the plasma membrane, and it is thought that their function is to guide membrane-docked cellulose synthase complexes. These, in turn, influence cell wall structure and cell shape by directed deposition of cellulose fibres. In elongating cells, cortical microtubule arrays are able to reorient in relation to long cell axis, and these reorientations have been linked to cell growth and to signaling of growth-regulating factors such as auxin or light. In this chapter, I am addressing the causal relationship between microtubule array reorientation, growth, and auxin signaling. I arrive at a model where array reorientation is not guided by auxin directly, but instead is only controlled by growth, which, in turn, is regulated by auxin
Synchronizing the Asynchronous
Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent asynchronous computation threads. We show that specifications and correctness proofs for asynchronous programs can be structured by introducing the fiction, for proof purposes, that intermediate, non-quiescent states of asynchronous operations can be ignored. Then, the task of specification becomes relatively simple and the task of verification can be naturally decomposed into smaller sub-tasks. The sub-tasks iteratively summarize, guided by the structure of an asynchronous program, the atomic effect of non-atomic operations and the synchronous effect of asynchronous operations. This structuring of specifications and proofs corresponds to the introduction of multiple layers of stepwise refinement for asynchronous programs. We present the first proof rule, called synchronization, to reduce asynchronous invocations on a lower layer to synchronous invocations on a higher layer. We implemented our proof method in CIVL and evaluated it on a collection of benchmark programs