Design, specification, and synthesis of aircraft electric power systems control logic

Cyber-physical systems integrate computation, networking, and physical processes. Substantial research challenges exist in the design and verification of such large-scale, distributed sensing, ac- tuation, and control systems. Rapidly improving technology and recent advances in control theory, networked systems, and computer science give us the opportunity to drastically improve our approach to integrated flow of information and cooperative behavior. Current systems rely on text-based spec- ifications and manual design. Using new technology advances, we can create easier, more efficient, and cheaper ways of developing these control systems. This thesis will focus on design considera- tions for system topologies, ways to formally and automatically specify requirements, and methods to synthesize reactive control protocols, all within the context of an aircraft electric power system as a representative application area.

This thesis consists of three complementary parts: synthesis, specification, and design. The first section focuses on the synthesis of central and distributed reactive controllers for an aircraft elec- tric power system. This approach incorporates methodologies from computer science and control. The resulting controllers are correct by construction with respect to system requirements, which are formulated using the specification language of linear temporal logic (LTL). The second section addresses how to formally specify requirements and introduces a domain-specific language for electric power systems. A software tool automatically converts high-level requirements into LTL and synthesizes a controller.

The final sections focus on design space exploration. A design methodology is proposed that uses mixed-integer linear programming to obtain candidate topologies, which are then used to synthesize controllers. The discrete-time control logic is then verified in real-time by two methods: hardware and simulation. Finally, the problem of partial observability and dynamic state estimation is ex- plored. Given a set placement of sensors on an electric power system, measurements from these sensors can be used in conjunction with control logic to infer the state of the system.

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.

Signal transduction, regulation, and developmental logic of EGFR signalling in C. elegans

RTKs-mediated signaling systems and the pathways with which they interact (e.g., those initiated by G protein-mediated signaling) involve a highly cooperative network that sense a large number of cellular inputs and then integrate, amplify, and process this information to orchestrate an appropriate set of cellular responses. The responses include virtually all aspects of cell function, from the most fundamental (proliferation, differentiation) to the most specialized (movement, metabolism, chemosensation). The basic tenets of RTK signaling system seem rather well established. Yet, new pathways and even new molecular players continue to be discovered. Although we believe that many of the essential modules of RTK signaling system are rather well understood, we have relatively little knowledge of the extent of interaction among these modules and their overall quantitative importance.

My research has encompassed the study of both positive and negative signaling by RTKs in C. elegans. I identified the C. elegans S0S-1 gene and showed that it is necessary for multiple RAS-mediated developmental signals. In addition, I demonstrated that there is a SOS-1-independent signaling during RAS-mediated vulval differentiation. By assessing signal outputs from various triple mutants, I have concluded that this SOS-1-independent signaling is not mediated by PTP-2/SHP-2 or the removal of inhibition by GAP-1/ RasGAP and it is not under regulation by SLI-1/Cb1. I speculate that there is either another exchange factor for RASor an as yet unidentified signaling pathway operating during RAS-mediated vulval induction in C. elegans.

In an attempt to uncover the molecular mechanisms of negative regulation of EGFR signaling by SLI-1/Cb1, I and two other colleagues codiscovered that RING finger domain of SLI-1 is partially dispensable for activity. This structure-function analysis shows that there is an ubiquitin protein ligase-independent activity for SLI-1 in regulating EGFR signaling. Further, we identified an inhibitory tyrosine of LET-23/ EGFR requiring sli-1(+)for its effects: removal of this tyrosine closely mimics loss of sli-1 but not loss of other negative regulator function.

By comparative analysis of two RTK pathways with similar signaling mechanisms, I have found that clr-1, a previously identified negative regulator of egl-15 mediated FGFR signaling, is also involved in let-23 EGFR signaling. The success of this approach promises a similar reciprocal test and could potentially extend to the study of other signaling pathways with similar signaling logic.

Finally, by correlating the developmental expression of lin-3 EGF to let-23 EGFR signaling activity, I demonstrated the existence of reciprocal EGF signaling in coordinating the morphogenesis of epithelia. This developmental logic of EGF signaling could provide a basis to understand a universal mechanism for organogenesis.

The logic of receptor-ligand interactions in the Notch signaling pathway

The Notch signaling pathway enables neighboring cells to coordinate developmental fates in diverse processes such as angiogenesis, neuronal differentiation, and immune system development. Although key components and interactions in the Notch pathway are known, it remains unclear how they work together to determine a cell's signaling state, defined as its quantitative ability to send and receive signals using particular Notch receptors and ligands. Recent work suggests that several aspects of the system can lead to complex signaling behaviors: First, receptors and ligands interact in two distinct ways, inhibiting each other in the same cell (in cis) while productively interacting between cells (in trans) to signal. The ability of a cell to send or receive signals depends strongly on both types of interactions. Second, mammals have multiple types of receptors and ligands, which interact with different strengths, and are frequently co-expressed in natural systems. Third, the three mammalian Fringe proteins can modify receptor-ligand interaction strengths in distinct and ligand-specific ways. Consequently, cells can exhibit non-intuitive signaling states even with relatively few components.

In order to understand what signaling states occur in natural processes, and what types of signaling behaviors they enable, this thesis puts forward a quantitative and predictive model of how the Notch signaling state is determined by the expression levels of receptors, ligands, and Fringe proteins. To specify the parameters of the model, we constructed a set of cell lines that allow control of ligand and Fringe expression level, and readout of the resulting Notch activity. We subjected these cell lines to an assay to quantitatively assess the levels of Notch ligands and receptors on the surface of individual cells. We further analyzed the dependence of these interactions on the level and type of Fringe expression. We developed a mathematical modeling framework that uses these data to predict the signaling states of individual cells from component expression levels. These methods allow us to reconstitute and analyze a diverse set of Notch signaling configurations from the bottom up, and provide a comprehensive view of the signaling repertoire of this major signaling pathway.

Isotope shift measurements using k x-rays in Sn, Sm, and W

Electronic Kαl x-ray isotope shifts have been measured for Sn 116-124, Sm 148-154, W 182-184, W 184-186, and W 182-186 using a curved crystal Cauchois spectrometer. The analysis of the measurements has included the electrostatic volume effect, screening by the transition electron as well as the non-transition electrons, normal and specific mass shifts, dynamical nuclear qudrupole polarization, and a radiative correction effect of the electron magnetic moment in the nuclear charge radii are obtained. Where other experimental data are available, the agreement with the present measurements is satisfactory. Comparisons with several nuclear model predictions yield only partial agreement.

Experimental study study of antiproton-proton annihilation into a pair of charged Pi-Mesons or K-Mesons for incident antiproton mementa in the range from 0.72 GeV/c to 2.62 GeV/c

The cross sections for the two antiproton-proton annihilation-in-flight modes,

ˉp + p → π⁺ + π^-

ˉp + p → k⁺ + k^-

were measured for fifteen laboratory antiproton beam momenta ranging from 0.72 to 2.62 GeV/c. No magnets were used to determine the charges in the final state. As a result, the angular distributions were obtained in the form [dσ/dΩ (Θ_C.M.) + dσ/dΩ (π – Θ_C.M.)] for 45 ≲ Θ_C.M. ≲ 135°.

A hodoscope-counter system was used to discriminate against events with final states having more than two particles and antiproton-proton elastic scattering events. One spark chamber was used to record the track of each of the two charged final particles. A total of about 40,000 pictures were taken. The events were analyzed by measuring the laboratory angle of the track in each chamber. The value of the square of the mass of the final particles was calculated for each event assuming the reaction

ˉp + p → a pair of particles with equal masses.

About 20,000 events were found to be either annihilation into π ^±-pair or k ^±-pair events. The two different charged meson pair modes were also distinctly separated.

The average differential cross section of ˉp + p → π⁺ + π^- varied from ~ 25 µb/sr at antiproton beam momentum 0.72 GeV/c (total energy in center-of-mass system, √s = 2.0 GeV) to ~ 2 µb/sr at beam momentum 2.62 GeV/c (√s = 2.64 GeV). The most striking feature in the angular distribution was a peak at Θ_C.M. = 90° (cos Θ_C.M. = 0) which increased with √s and reached a maximum at √s ~ 2.1 GeV (beam momentum ~ 1.1 GeV/c). Then it diminished and seemed to disappear completely at √s ~ 2.5 GeV (beam momentum ~ 2.13 GeV/c). A valley in the angular distribution occurred at cos Θ_C.M. ≈ 0.4. The differential cross section then increased as cos Θ_C.M. approached 1.

The average differential cross section for ˉp + p → k⁺ + k^- was about one third of that of the π^±-pair mode throughout the energy range of this experiment. At the lower energies, the angular distribution, unlike that of the π^±-pair mode, was quite isotropic. However, a peak at Θ_C.M. = 90° seemed to develop at √s ~ 2.37 GeV (antiproton beam momentum ~ 1.82 GeV/c). No observable change was seen at that energy in the π^±-pair cross section.

The possible connection of these features with the observed meson resonances at 2.2 GeV and 2.38 GeV, and its implications, were discussed.

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.

Thermodynamic and kinetic behavior of an argon plasma jet. Decomposition of nitric oxide between 1300 - 1750 degrees K in an argon plasma

In the first part of the study, an RF coupled, atmospheric pressure, laminar plasma jet of argon was investigated for thermodynamic equilibrium and some rate processes.

Improved values of transition probabilities for 17 lines of argon I were developed from known values for 7 lines. The effect of inhomogeneity of the source was pointed out.

The temperatures, T, and the electron densities, n_e , were determined spectroscopically from the population densities of the higher excited states assuming the Saha-Boltzmann relationship to be valid for these states. The axial velocities, v_z, were measured by tracing the paths of particles of boron nitride using a three-dimentional mapping technique. The above quantities varied in the following ranges: 10¹² ˂ n_e ˂ 10¹⁵ particles/cm³, 3500 ˂ T ˂ 11000 °K, and 200 ˂ v_z ˂ 1200 cm/sec.

The absence of excitation equilibrium for the lower excitation population including the ground state under certain conditions of T and n_e was established and the departure from equilibrium was examined quantitatively. The ground state was shown to be highly underpopulated for the decaying plasma.

Rates of recombination between electrons and ions were obtained by solving the steady-state equation of continuity for electrons. The observed rates were consistent with a dissociative-molecular ion mechanism with a steady-state assumption for the molecular ions.

In the second part of the study, decomposition of NO was studied in the plasma at lower temperatures. The mole fractions of NO denoted by x_NO were determined gas-chromatographically and varied between 0.0012 ˂ x_NO ˂ 0.0055. The temperatures were measured pyrometrically and varied between 1300 ˂ T ˂ 1750°K. The observed rates of decomposition were orders of magnitude greater than those obtained by the previous workers under purely thermal reaction conditions. The overall activation energy was about 9 kcal/g mol which was considerably lower than the value under thermal conditions. The effect of excess nitrogen was to reduce the rate of decomposition of NO and to increase the order of the reaction with respect to NO from 1.33 to 1.85. The observed rates were consistent with a chain mechanism in which atomic nitrogen and oxygen act as chain carriers. The increased rates of decomposition and the reduced activation energy in the presence of the plasma could be explained on the basis of the observed large amount of atomic nitrogen which was probably formed as the result of reactions between excited atoms and ions of argon and the molecular nitrogen.

An investigation of the reaction negative K¯p → K¯π⁺ at P_(lab) = 2 Gev/c

The reaction K^-p→K^-π⁺n has been studied for incident kaon momenta of 2.0 GeV/c. A sample of 19,881 events was obtained by a measurement of film taken as part of the K-63 experiment in the Berkeley 72 inch bubble chamber.

Based upon our analysis, we have reached four conclusions. (1) The magnitude of the extrapolated Kπ cross section differs by a factor of 2 from the P-wave unitarity prediction and the K⁺n results; this is probably due to absorptive effects. (2) Fits to the moments yield precise values for the Kπ S-wave which agree with other recent statistically accurate experiments. (3) An anomalous peak is present in our backward K^-p→(π+n) K^- u-distribution. (4) We find a non-linear enhancement due to interference similiar to the one found by Bland et al. (Bland 1966).

Inelastic K+p reactions at incident momenta from 1.37 GeV/c to 2.17 GeV/c

A number of recent experiments have suggested the possibility of a highly inelastic resonance in K⁺p scattering. To study the inelastic K⁺p reactions, a 400 K exposure has been taken at the L.R.L. 25 inch bubble chamber. The data are spread over seven K⁺ momenta between 1.37 and 2.17 GeV/c.

Cross-sections have been measured for the reaction K⁺p → pK°π+ which is dominated by the quasi-two body channels K∆ and K*N. Both these channels are strongly peripheral, as at other momenta. The decay of the ∆ is in good agreement with the predictions of the rho-photon analogy of Stodolsky and Sakurai. The data on the K*p channel show evidence of both pseudo scalar and vector exchange.

Cross-sections for the final state pK⁺π+π- shows a strong contribution from the quasi-two body channel K*∆. This reaction is also very peripheral even at threshold. The decay angular distributions indicate the reaction is dominated as at higher momenta by a pion exchange mechanism. The data are also in good agreement with the quark model predictions of Bialas and Zalewski for the K* and ∆ decay.

CP and the three pion decay of the K°

The time distribution of the decays of an initially pure K° beam into π+π-π° has been analyzed to determine the complex parameter W (also known as Ƞ^+-° and (x + iy)). The K° beam was produced in a brass target by the interactions of a 2.85 GeV/c π- beam which was generated on an internal target in the Lawrence Radiation Laboratory (LRL) Bevatron. The counters and hodoscopes in the apparatus selected for events with a neutral (K°) produced in the brass target, two charged secondaries passing through a magnet spectrometer and a ɣ-ray shower in a shower hodoscope.

From the 275K apparatus triggers, 148 K → π+π-π° events were isolated. The presence of a ɣ-ray shower in the optical shower chambers and a two-prong vee in the optical spark chambers were devices used to isolate the events. The backgrounds were further reduced by reconstructing the momenta of the two charged secondaries and applying kinematic constraints.

The best fit to the final sample of 148 events distributed between .3 and 7.0 K_S lifetimes gives:

ReW = -.05 ±.17

ImW = +.39 +.35/-.37

This result is consistent with both CPT invariance (ReW = 0) and CP invariance (W = 0). Backgrounds are estimated to be less than 10% and systematic effects have also been estimated to be negligible.

An analysis of the present data on CP violation in this decay mode and other K° decay modes has estimated the phase of ɛ to be 45.3 ± 2.3 degrees. This result is consistent with the super weak theories of CP violation which predicts the phase of ɛ to be 43°. This estimate is in turn used to predict the phase of Ƞ°° to be 48.0 ± 7.9 degrees. This is a substantial improvement on presently available measurements. The largest error in this analysis comes from the present limits on W from the world average of recent experiments. The K → πuʋ mode produces the next largest error. Therefore further experimentation in these modes would be useful.