Incremental Control Synthesis for Robotics in the Presence of Temporal Logic Specifications

This thesis presents methods for incrementally constructing controllers in the presence of uncertainty and nonlinear dynamics. The basic setting is motion planning subject to temporal logic specifications. Broadly, two categories of problems are treated. The first is reactive formal synthesis when so-called discrete abstractions are available. The fragment of linear-time temporal logic (LTL) known as GR(1) is used to express assumptions about an adversarial environment and requirements of the controller. Two problems of changes to a specification are posed that concern the two major aspects of GR(1): safety and liveness. Algorithms providing incremental updates to strategies are presented as solutions. In support of these, an annotation of strategies is developed that facilitates repeated modifications. A variety of properties are proven about it, including necessity of existence and sufficiency for a strategy to be winning. The second category of problems considered is non-reactive (open-loop) synthesis in the absence of a discrete abstraction. Instead, the presented stochastic optimization methods directly construct a control input sequence that achieves low cost and satisfies a LTL formula. Several relaxations are considered as heuristics to address the rarity of sampling trajectories that satisfy an LTL formula and demonstrated to improve convergence rates for Dubins car and single-integrators subject to a recurrence task.

Psychobiophysics of transcranial magnetic stimulation

Transcranial magnetic stimulation (TMS) is a technique that stimulates the brain using a magnetic coil placed on the scalp. Since it is applicable to humans non-invasively, directly interfering with neural electrical activity, it is potentially a good tool to study the direct relationship between perceptual experience and neural activity. However, it has been difficult to produce a clear perceptible phenomenon with TMS of sensory areas, especially using a single magnetic pulse. Also, the biophysical mechanisms of magnetic stimulation of single neurons have been poorly understood.

In the psychophysical part of this thesis, perceptual phenomena induced by TMS of the human visual cortex are demonstrated as results of the interactions with visual inputs. We first introduce a method to create a hole, or a scotoma, in a flashed, large-field visual pattern using single-pulse TMS. Spatial aspects of the interactions are explored using the distortion effect of the scotoma depending on the visual pattern, which can be luminance-defined or illusory. Its similarity to the distortion of afterimages is also discussed. Temporal interactions are demonstrated in the filling-in of the scotoma with temporally adjacent visual features, as well as in the effective suppression of transient visual features. Also, paired-pulse TMS is shown to lead to different brightness modulations in transient and sustained visual stimuli.

In the biophysical part, we first develop a biophysical theory to simulate the effect of magnetic stimulation on arbitrary neuronal structure. Computer simulations are performed on cortical neuron models with realistic structure and channels, combined with the current injection that simulates magnetic stimulation. The simulation results account for general and basic characteristics of the macroscopic effects of TMS including our psychophysical findings, such as a long inhibitory effect, dependence on the background activity, and dependence on the direction of the induced electric field.

The perceptual effects and the cortical neuron model presented here provide foundations for the study of the relationship between perception and neural activity. Further insights would be obtained from extension of our model to neuronal networks and psychophysical studies based on predictions of the biophysical model.

Neural representation of auditory temporal structure

Neurons in the songbird forebrain nucleus HVc are highly sensitive to auditory temporal context and have some of the most complex auditory tuning properties yet discovered. HVc is crucial for learning, perceiving, and producing song, thus it is important to understand the neural circuitry and mechanisms that give rise to these remarkable auditory response properties. This thesis investigates these issues experimentally and computationally.

Extracellular studies reported here compare the auditory context sensitivity of neurons in HV c with neurons in the afferent areas of field L. These demonstrate that there is a substantial increase in the auditory temporal context sensitivity from the areas of field L to HVc. Whole-cell recordings of HVc neurons from acute brain slices are described which show that excitatory synaptic transmission between HVc neurons involve the release of glutamate and the activation of both AMPA/kainate and NMDA-type glutamate receptors. Additionally, widespread inhibitory interactions exist between HVc neurons that are mediated by postsynaptic GABA_A receptors. Intracellular recordings of HVc auditory neurons in vivo provides evidence that HV c neurons encode information about temporal structure using a variety of cellular and synaptic mechanisms including syllable-specific inhibition, excitatory post-synaptic potentials with a range of different time courses, and burst-firing, and song-specific hyperpolarization.

The final part of this thesis presents two computational approaches for representing and learning temporal structure. The first method utilizes comput ational elements that are analogous to temporal combination sensitive neurons in HVc. A network of these elements can learn using local information and lateral inhibition. The second method presents a more general framework which allows a network to discover mixtures of temporal features in a continuous stream of input.

Analysis of temporal structure in spike trains of visual cortical area MT

The temporal structure of neuronal spike trains in the visual cortex can provide detailed information about the stimulus and about the neuronal implementation of visual processing. Spike trains recorded from the macaque motion area MT in previous studies (Newsome et al., 1989a; Britten et al., 1992; Zohary et al., 1994) are analyzed here in the context of the dynamic random dot stimulus which was used to evoke them. If the stimulus is incoherent, the spike trains can be highly modulated and precisely locked in time to the stimulus. In contrast, the coherent motion stimulus creates little or no temporal modulation and allows us to study patterns in the spike train that may be intrinsic to the cortical circuitry in area MT. Long gaps in the spike train evoked by the preferred direction motion stimulus are found, and they appear to be symmetrical to bursts in the response to the anti-preferred direction of motion. A novel cross-correlation technique is used to establish that the gaps are correlated between pairs of neurons. Temporal modulation is also found in psychophysical experiments using a modified stimulus. A model is made that can account for the temporal modulation in terms of the computational theory of biological image motion processing. A frequency domain analysis of the stimulus reveals that it contains a repeated power spectrum that may account for psychophysical and electrophysiological observations.

Some neurons tend to fire bursts of action potentials while others avoid burst firing. Using numerical and analytical models of spike trains as Poisson processes with the addition of refractory periods and bursting, we are able to account for peaks in the power spectrum near 40 Hz without assuming the existence of an underlying oscillatory signal. A preliminary examination of the local field potential reveals that stimulus-locked oscillation appears briefly at the beginning of the trial.

Control of dynamical systems with temporal logic specifications

This thesis is motivated by safety-critical applications involving autonomous air, ground, and space vehicles carrying out complex tasks in uncertain and adversarial environments. We use temporal logic as a language to formally specify complex tasks and system properties. Temporal logic specifications generalize the classical notions of stability and reachability that are studied in the control and hybrid systems communities. Given a system model and a formal task specification, the goal is to automatically synthesize a control policy for the system that ensures that the system satisfies the specification. This thesis presents novel control policy synthesis algorithms for optimal and robust control of dynamical systems with temporal logic specifications. Furthermore, it introduces algorithms that are efficient and extend to high-dimensional dynamical systems.

The first contribution of this thesis is the generalization of a classical linear temporal logic (LTL) control synthesis approach to optimal and robust control. We show how we can extend automata-based synthesis techniques for discrete abstractions of dynamical systems to create optimal and robust controllers that are guaranteed to satisfy an LTL specification. Such optimal and robust controllers can be computed at little extra computational cost compared to computing a feasible controller.

The second contribution of this thesis addresses the scalability of control synthesis with LTL specifications. A major limitation of the standard automaton-based approach for control with LTL specifications is that the automaton might be doubly-exponential in the size of the LTL specification. We introduce a fragment of LTL for which one can compute feasible control policies in time polynomial in the size of the system and specification. Additionally, we show how to compute optimal control policies for a variety of cost functions, and identify interesting cases when this can be done in polynomial time. These techniques are particularly relevant for online control, as one can guarantee that a feasible solution can be found quickly, and then iteratively improve on the quality as time permits.

The final contribution of this thesis is a set of algorithms for computing feasible trajectories for high-dimensional, nonlinear systems with LTL specifications. These algorithms avoid a potentially computationally-expensive process of computing a discrete abstraction, and instead compute directly on the system's continuous state space. The first method uses an automaton representing the specification to directly encode a series of constrained-reachability subproblems, which can be solved in a modular fashion by using standard techniques. The second method encodes an LTL formula as mixed-integer linear programming constraints on the dynamical system. We demonstrate these approaches with numerical experiments on temporal logic motion planning problems with high-dimensional (10+ states) continuous systems.

Temporal and spacial control of RNA stability in the early embryo of Drosophila melanogaster

Early embryogenesis in metazoa is controlled by maternally synthesized products. Among these products, the mature egg is loaded with transcripts representing approximately two thirds of the genome. A subset of this maternal RNA pool is degraded prior to the transition to zygotic control of development. This transfer of control of development from maternal to zygotic products is referred to as the midblastula transition (or MBT). It is believed that the degradation of maternal transcripts is required to terminate maternal control of development and to allow zygotic control of development to begin. Until now this process of maternal transcript degradation and the subsequent timing of the MBT has been poorly understood. I have demonstrated that in the early embryo there are two independent RNA degradation pathways, either of which is sufficient for transcript elimination. However, only the concerted action of both pathways leads to elimination of transcripts with the correct timing, at the MBT. The first pathway is maternally encoded, is triggered by egg activation, and is targeted to specific classes of mRNAs through cis-acting elements in the 3' untranslated region (UTR}. The second pathway is activated 2 hr after fertilization and functions together with the maternal pathway to ensure that transcripts are degraded by the MBT. In addition, some transcripts fail to degrade at select subcellular locations adding an element of spatial control to RNA degradation. The spatial control of RNA degradation is achieved by protecting, or masking, transcripts from the degradation machinery. The RNA degradation and protection events are regulated by distinct cis-elements in the 3' untranslated region (UTR). These results provide the first systematic dissection of this highly conserved process in development and demonstrate that RNA degradation is a novel mechanism used for both temporal and spatial control of development.

Electron flow through cytochrome P450

The cytochromes P450 (P450s) are a remarkable class of heme enzymes that catalyze the metabolism of xenobiotics and the biosynthesis of signaling molecules. Controlled electron flow into the thiolate-ligated heme active site allows P450s to activate molecular oxygen and hydroxylate aliphatic C–H bonds via the formation of high-valent metal-oxo intermediates (compounds I and II). Due to the reactive nature and short lifetimes of these intermediates, many of the fundamental steps in catalysis have not been observed directly. The Gray group and others have developed photochemical methods, known as “flash-quench,” for triggering electron transfer (ET) and generating redox intermediates in proteins in the absence of native ET partners. Photo-triggering affords a high degree of temporal precision for the gating of an ET event; the initial ET and subsequent reactions can be monitored on the nanosecond-to-second timescale using transient absorption (TA) spectroscopies. Chapter 1 catalogues critical aspects of P450 structure and mechanism, including the native pathway for formation of compound I, and outlines the development of photochemical processes that can be used to artificially trigger ET in proteins. Chapters 2 and 3 describe the development of these photochemical methods to establish electronic communication between a photosensitizer and the buried P450 heme. Chapter 2 describes the design and characterization of a Ru-P450-BM3 conjugate containing a ruthenium photosensitizer covalently tethered to the P450 surface, and nanosecond-to-second kinetics of the photo-triggered ET event are presented. By analyzing data at multiple wavelengths, we have identified the formation of multiple ET intermediates, including the catalytically relevant compound II; this intermediate is generated by oxidation of a bound water molecule in the ferric resting state enzyme. The work in Chapter 3 probes the role of a tryptophan residue situated between the photosensitizer and heme in the aforementioned Ru-P450 BM3 conjugate. Replacement of this tryptophan with histidine does not perturb the P450 structure, yet it completely eliminates the ET reactivity described in Chapter 2. The presence of an analogous tryptophan in Ru-P450 CYP119 conjugates also is necessary for observing oxidative ET, but the yield of heme oxidation is lower. Chapter 4 offers a basic description of the theoretical underpinnings required to analyze ET. Single-step ET theory is first presented, followed by extensions to multistep ET: electron “hopping.” The generation of “hopping maps” and use of a hopping map program to analyze the rate advantage of hopping over single-step ET is described, beginning with an established rhenium-tryptophan-azurin hopping system. This ET analysis is then applied to the Ru-tryptophan-P450 systems described in Chapter 2; this strongly supports the presence of hopping in Ru-P450 conjugates. Chapter 5 explores the implementation of flash-quench and other phototriggered methods to examine the native reductive ET and gas binding events that activate molecular oxygen. In particular, TA kinetics that demonstrate heme reduction on the microsecond timescale for four Ru-P450 conjugates are presented. In addition, we implement laser flash-photolysis of P450 ferrous–CO to study the rates of CO rebinding in the thermophilic P450 CYP119 at variable temperature. Chapter 6 describes the development and implementation of air-sensitive potentiometric redox titrations to determine the solution reduction potentials of a series of P450 BM3 mutants, which were designed for non-native cyclopropanation of styrene in vivo. An important conclusion from this work is that substitution of the axial cysteine for serine shifts the wild type reduction potential positive by 130 mV, facilitating reduction by biological redox cofactors in the presence of poorly-bound substrates. While this mutation abolishes oxygenation activity, these mutants are capable of catalyzing the cyclopropanation of styrene, even within the confines of an E. coli cell. Four appendices are also provided, including photochemical heme oxidation in ruthenium-modified nitric oxide synthase (Appendix A), general protocols (Appendix B), Chapter-specific notes (Appendix C) and Matlab scripts used for data analysis (Appendix D).

Mechanistic aspects of the Ziegler-Natta polymerization

The isotope effect on propagation rate was determined for four homogeneous ethylene polymerization systems. The catalytic system Cp_2Ti(Et)Cl + EtA1Cl_2 has a k^H_p/k^D_p = 1.035 ± 0.03. This result strongly supports an insertion mechanism which does not involve a hydrogen migration during the rate determining step of propagation (Cossee mechanism). Three metal-alkyl free systems were also studied. The catalyst I_2 (PMe_3)_3Ta(neopentylidene)(H) has a k^H_p/k^D_p = 1.709. It is interpreted as a primary isotope effect involving a non-linear a-hydrogen migration during the rate determining step of propagation (Green mechanism). The lanthanide complexes Cp*_2LuMe•Et_2O and Cp*_2YbMe•Et_2O have a k^H_p/k^D_p = 1.46 and 1.25, respectively. They are interpreted as primary isotope effects due to a partial hydrogen migration during the rate determining step of propagation.

The presence of a precoordination or other intermediate species during the polymerization of ethylene by the mentioned metal-alkyl free catalysts was sought by low temperature NMR spectroscopy. However, no evidence for such species was found. If they exist, their concentrations are very small or their lifetimes are shorter than the NMR time scale.

Two titanocene (alkenyl)chlorides (hexenyl 1 and heptenyl 2 were prepared from titanocene dichloride and a THF solution of the corresponding alkenylmagnesium chloride. They do not cyclize in solution when alone, but cyclization to their respective titanocene(methyl(cycloalkyl) chlorides occurs readily in the presence of a Lewis acid. It is demonstrated that such cyclization occurs with the alkenyl ligand within the coordination sphere of the titanium atom. Cyclization of 1 with EtAlCl_2 at 0°C occurs in less than 95 msec (ethylene insertion time), as shown by the presence of 97% cyclopentyl-capped oligomers when polymerizing ethylene with this system. Some alkyl exchange occurs (3%). Cyclization of 2 is slower under the same reaction conditions and is not complete in 95 msec as shown by the presence of both cyclohexyl-capped oligomers (35%) and odd number α-olefin oligomers (50%). Alkyl exchange is more extensive as evidenced by the even number n-alkanes (15%).

Cyclization of 2-d_1 (titanocene(hept-6-en-1-yl-1-d_1)chloride) with EtA1Cl_2 demonstrated that for this system there is no α-hydrogen participation during said process. The cyclization is believed to occur by a Cossee-type mechanism. There was no evidence for precoordination of the alkenyl double bond during the cyclization process.

From molecules to organs : Microscopy and multi-scale nature of development

Morphogenesis is a phenomenon of intricate balance and dynamic interplay between processes occurring at a wide range of scales (spatial, temporal and energetic). During development, a variety of physical mechanisms are employed by tissues to simultaneously pattern, move, and differentiate based on information exchange between constituent cells, perhaps more than at any other time during an organism's life. To fully understand such events, a combined theoretical and experimental framework is required to assist in deciphering the correlations at both structural and functional levels at scales that include the intracellular and tissue levels as well as organs and organ systems. Microscopy, especially diffraction-limited light microscopy, has emerged as a central tool to capture the spatio-temporal context of life processes. Imaging has the unique advantage of watching biological events as they unfold over time at single-cell resolution in the intact animal. In this work I present a range of problems in morphogenesis, each unique in its requirements for novel quantitative imaging both in terms of the technique and analysis. Understanding the molecular basis for a developmental process involves investigating how genes and their products- mRNA and proteins-function in the context of a cell. Structural information holds the key to insights into mechanisms and imaging fixed specimens paves the first step towards deciphering gene function. The work presented in this thesis starts with the demonstration that the fluorescent signal from the challenging environment of whole-mount imaging, obtained by in situ hybridization chain reaction (HCR), scales linearly with the number of copies of target mRNA to provide quantitative sub-cellular mapping of mRNA expression within intact vertebrate embryos. The work then progresses to address aspects of imaging live embryonic development in a number of species. While processes such as avian cartilage growth require high spatial resolution and lower time resolution, dynamic events during zebrafish somitogenesis require higher time resolution to capture the protein localization as the somites mature. The requirements on imaging are even more stringent in case of the embryonic zebrafish heart that beats with a frequency of ~ 2-2.5 Hz, thereby requiring very fast imaging techniques based on two-photon light sheet microscope to capture its dynamics. In each of the hitherto-mentioned cases, ranging from the level of molecules to organs, an imaging framework is developed, both in terms of technique and analysis to allow quantitative assessment of the process in vivo. Overall the work presented in this thesis combines new quantitative tools with novel microscopy for the precise understanding of processes in embryonic development.