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.

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.

适合于小飞机防撞系统的机载小型激光测距仪

报道了一种重量轻、功耗低、适合于小飞机防撞系统应用的小型激光测距仪。系统基于脉冲激光测距原理，采用905nm半导体脉冲激光器、电感升压式偏置高压电源和可编程逻辑器件（PLD），研制出重量不大于100g，功耗不大于625mW，测量范围100m，盲区3．0m，分辨率±1m的机载小型激光测距仪。实验测试结果表明，其各项技术性能指标符合无人驾驶小飞机防撞系统的应用要求。

Parallel optical negabinary arithmetic based on logic operations

On the basis of signed-digit negabinary representation, parallel two-step addition and one-step subtraction can be performed for arbitrary-length negabinary operands.; The arithmetic is realized by signed logic operations and optically implemented by spatial encoding and decoding techniques. The proposed algorithm and optical system are simple, reliable, and practicable, and they have the property of parallel processing of two-dimensional data. This leads to an efficient design for the optical arithmetic and logic unit. (C) 1997 Optical Society of America.

Compact parallel optical modified-signed-digit arithmetic-logic array processor with electron-trapping device

A compact two-step modified-signed-digit arithmetic-logic array processor is proposed. When the reference digits are programmed, both addition and subtraction can be performed by the same binary logic operations regardless of the sign of the input digits. The optical implementation and experimental demonstration with an electron-trapping device are shown. Each digit is encoded by a single pixel, and no polarization is included. Any combinational logic can be easily performed without optoelectronic and electro-optic conversions of the intermediate results. The system is compact, general purpose, simple to align, and has a high signal-to-noise ratio. (C) 1999 Optical Society of America.

Logic-operated mathematical morphology and its optical implementation

A more powerful tool for binary image processing, i.e., logic-operated mathematical morphology (LOMM), is proposed. With LOMM the image and the structuring element (SE) are treated as binary logical variables, and the MULTIPLY between the image and the SE in correlation is replaced with 16 logical operations. A total of 12 LOMM operations are obtained. The optical implementation of LOMM is described. The application of LOMM and its experimental results are also presented. (C) 1999 Optical Society of America.

Code conversion from signed-digit to complement representation based on look-ahead optical logic operations

We present, for the first time to our knowledge, a generalized lookahead logic algorithm for number conversion from signed-digit to complement representation. By properly encoding the signed-digits, all the operations are performed by binary logic, and unified logical expressions can be obtained for conversion from modified-signed-digit (MSD) to 2's complement, trinary signed-digit (TSD) to 3's complement, and quarternary signed-digit (QSD) to 4's complement. For optical implementation, a parallel logical array module using an electron-trapping device is employed and experimental results are shown. This optical module is suitable for implementing complex logic functions in the form of the sum of the product. The algorithm and architecture are compatible with a general-purpose optoelectronic computing system. (C) 2001 Society of Photo-Optical Instrumentation Engineers.

Enzyme induction in Neurospora crassa

I. Studies on Nicotinamide Adenine Dinucleotide Glycohydrase (NADase)

NADase, like tyrosinase and L-amino acid oxidase, is not present in two day old cultures of wild type Neurospora, but it is coinduced with those two enzymes during starvation in phosphate buffer. The induction of NADase, like tyrosinase, is inhibited by puromycin. The induction of all three enzymes is inhibited by actinomycin D. These results suggest that NADase is synthesized de novo during induction as has been shown directly for tyrosinase. NADase induction differs in being inhibited by certain amino acids.

The tyrosinaseless mutant ty-1 contains a non-dialyzable, heat labile inhibitor of NADase. A new mutant, P110A, synthesizes NADase and L-amino acid oxidase while growing. A second strain, pe, fl;cot, makes NADase while growing. Both strains can be induced to make the other enzymes. These two strains prove that the control of these three enzymes is divisible. The strain P110A makes NADase even when grown in the presence of Tween 80. The synthesis of both NADase and L-amino acid oxidase by P110A is suppressed by complete medium. The theory of control of the synthesis of the enzymes is discussed.

II. Studies with EDTA

Neurospora tyrosinase contains copper but, unlike other phenol oxidases, this copper has never been removed reversibly. It was thought that the apo-enzyme might be made in vivo in the absence of copper. Therefore cultures were treated with EDTA to remove copper before the enzyme was induced. Although no apo-tyrosinase was detected, new information on the induction process was obtained.

A treatment of Neurospora with 0.5% EDTA pH 7, inhibits the subsequent induction during starvation in phosphate buffer of tyrosinase, L-amino acid oxidase and NADase. The inhibition of tyrosinase and L-amino acid oxidase induction is completely reversed by adding 5 x 10^-5M CaCl₂, 5 x 10^-4M CuSO₄, and a mixture of L-amino acids (2 x 10^-3M each) to the buffer. Tyrosinase induction is also fully restored by 5 x 10^-4M CaCl₂ and amino acids. As yet NADase has been only partially restored.

The copper probably acts by sequestering EDTA left in the mycelium and may be replaced by nickel. The EDTA apparently removes some calcium from the mycelium, which the added calcium replaces. Magnesium cannot replace calcium. The amino acids probably replace endogenous amino acids lost to the buffer after the EDTA treatment.

The EDTA treatment also increases permeability, thereby increasing the sensitivity of induction to inhibition by actinomycin D and allowing cell contents to be lost to the induction buffer. EDTA treatment also inhibits the uptake of exogenous amino acids and their incorporation into proteins.

The lag period that precedes the first appearance of tyrosinase is demonstrated to be a separate dynamic phase of induction. It requires oxygen. It is inhibited by EDTA, but can be completed after EDTA treatment in the presence of 5 x 10^-5M CaCl₂ alone, although no tyrosinase is synthesized under these conditions.

The time course of induction has an early exponential phase suggesting an autocatalytic mechanism of induction.

The mode of action of EDTA, the process of induction and the kinetics of induction are discussed.