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.

The Physiology and Computation of Pyramidal Neurons

A variety of neural signals have been measured as correlates to consciousness. In particular, late current sinks in layer 1, distributed activity across the cortex, and feedback processing have all been implicated. What are the physiological underpinnings of these signals? What computational role do they play in the brain? Why do they correlate to consciousness? This thesis begins to answer these questions by focusing on the pyramidal neuron. As the primary communicator of long-range feedforward and feedback signals in the cortex, the pyramidal neuron is set up to play an important role in establishing distributed representations. Additionally, the dendritic extent, reaching layer 1, is well situated to receive feedback inputs and contribute to current sinks in the upper layers. An investigation of pyramidal neuron physiology is therefore necessary to understand how the brain creates, and potentially uses, the neural correlates of consciousness. An important part of this thesis will be in establishing the computational role that dendritic physiology plays. In order to do this, a combined experimental and modeling approach is used.

This thesis beings with single-cell experiments in layer 5 and layer 2/3 pyramidal neurons. In both cases, dendritic nonlinearities are characterized and found to be integral regulators of neural output. Particular attention is paid to calcium spikes and NMDA spikes, which both exist in the apical dendrites, considerable distances from the spike initiation zone. These experiments are then used to create detailed multicompartmental models. These models are used to test hypothesis regarding spatial distribution of membrane channels, to quantify the effects of certain experimental manipulations, and to establish the computational properties of the single cell. We find that the pyramidal neuron physiology can carry out a coincidence detection mechanism. Further abstraction of these models reveals potential mechanisms for spike time control, frequency modulation, and tuning. Finally, a set of experiments are carried out to establish the effect of long-range feedback inputs onto the pyramidal neuron. A final discussion then explores a potential way in which the physiology of pyramidal neurons can establish distributed representations, and contribute to consciousness.

Comment on: Computation of the optical trapping force using an FDTD based technique

In this comment, problems associated with an oversimplified FDTD based model used for trapping force calculation in recent papers "Computation of the optical trapping force using an FDTD based technique" [Opt. Express 13, 3707 (2005)], and "Rigorous time domain simulation of momentum transfer between light and microscopic particles in optical trapping" [Opt. Express 12, 2220 (2004)] are discussed. A more rigorous model using in Poynting vector is also presented.