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.

Formal methods for control synthesis in partially observed environments : application to autonomous robotic manipulation

Modern robots are increasingly expected to function in uncertain and dynamically challenging environments, often in proximity with humans. In addition, wide scale adoption of robots requires on-the-fly adaptability of software for diverse application. These requirements strongly suggest the need to adopt formal representations of high level goals and safety specifications, especially as temporal logic formulas. This approach allows for the use of formal verification techniques for controller synthesis that can give guarantees for safety and performance. Robots operating in unstructured environments also face limited sensing capability. Correctly inferring a robot's progress toward high level goal can be challenging.

This thesis develops new algorithms for synthesizing discrete controllers in partially known environments under specifications represented as linear temporal logic (LTL) formulas. It is inspired by recent developments in finite abstraction techniques for hybrid systems and motion planning problems. The robot and its environment is assumed to have a finite abstraction as a Partially Observable Markov Decision Process (POMDP), which is a powerful model class capable of representing a wide variety of problems. However, synthesizing controllers that satisfy LTL goals over POMDPs is a challenging problem which has received only limited attention.

This thesis proposes tractable, approximate algorithms for the control synthesis problem using Finite State Controllers (FSCs). The use of FSCs to control finite POMDPs allows for the closed system to be analyzed as finite global Markov chain. The thesis explicitly shows how transient and steady state behavior of the global Markov chains can be related to two different criteria with respect to satisfaction of LTL formulas. First, the maximization of the probability of LTL satisfaction is related to an optimization problem over a parametrization of the FSC. Analytic computation of gradients are derived which allows the use of first order optimization techniques.

The second criterion encourages rapid and frequent visits to a restricted set of states over infinite executions. It is formulated as a constrained optimization problem with a discounted long term reward objective by the novel utilization of a fundamental equation for Markov chains - the Poisson equation. A new constrained policy iteration technique is proposed to solve the resulting dynamic program, which also provides a way to escape local maxima.

The algorithms proposed in the thesis are applied to the task planning and execution challenges faced during the DARPA Autonomous Robotic Manipulation - Software challenge.

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.

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.

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.

Formal methods in the foundations of science

The intent of this study is to provide formal apparatus which facilitates the investigation of problems in the methodology of science. The introduction contains several examples of such problems and motivates the subsequent formalism.

A general definition of a formal language is presented, and this definition is used to characterize an individual’s view of the world around him. A notion of empirical observation is developed which is independent of language. The interplay of formal language and observation is taken as the central theme. The process of science is conceived as the finding of that formal language that best expresses the available experimental evidence.

To characterize the manner in which a formal language imposes structure on its universe of discourse, the fundamental concepts of elements and states of a formal language are introduced. Using these, the notion of a basis for a formal language is developed as a collection of minimal states distinguishable within the language. The relation of these concepts to those of model theory is discussed.

An a priori probability defined on sets of observations is postulated as a reflection of an individual’s ontology. This probability, in conjunction with a formal language and a basis for that language, induces a subjective probability describing an individual’s conceptual view of admissible configurations of the universe. As a function of this subjective probability, and consequently of language, a measure of the informativeness of empirical observations is introduced and is shown to be intuitively plausible – particularly in the case of scientific experimentation.

The developed formalism is then systematically applied to the general problems presented in the introduction. The relationship of scientific theories to empirical observations is discussed and the need for certain tacit, unstatable knowledge is shown to be necessary to fully comprehend the meaning of realistic theories. The idea that many common concepts can be specified only by drawing on knowledge obtained from an infinite number of observations is presented, and the problems of reductionism are examined in this context.

A definition of when one formal language can be considered to be more expressive than another is presented, and the change in the informativeness of an observation as language changes is investigated. In this regard it is shown that the information inherent in an observation may decrease for a more expressive language.

The general problem of induction and its relation to the scientific method are discussed. Two hypotheses concerning an individual’s selection of an optimal language for a particular domain of discourse are presented and specific examples from the introduction are examined.

Formal languages, part theory, and change

A general definition of interpreted formal language is presented. The notion “is a part of" is formally developed and models of the resulting part theory are used as universes of discourse of the formal languages. It is shown that certain Boolean algebras are models of part theory.

With this development, the structure imposed upon the universe of discourse by a formal language is characterized by a group of automorphisms of the model of part theory. If the model of part theory is thought of as a static world, the automorphisms become the changes which take place in the world. Using this formalism, we discuss a notion of abstraction and the concept of definability. A Galois connection between the groups characterizing formal languages and a language-like closure over the groups is determined.

It is shown that a set theory can be developed within models of part theory such that certain strong formal languages can be said to determine their own set theory. This development is such that for a given formal language whose universe of discourse is a model of part theory, a set theory can be imbedded as a submodel of part theory so that the formal language has parts which are sets as its discursive entities.