Search by property

This page provides a simple browsing interface for finding entities described by a property and a named value. Other available search interfaces include the page property search, and the ask query builder.

List of results

• We present a mathematical programming-base … We present a mathematical programming-based method for model predictive control of cyber-physical systems subject to signal temporal logic (STL) specifications. We describe the use of STL to specify a wide range of properties of these systems, including safety, response and bounded liveness. For synthesis, we encode STL specifications as mixed integer-linear constraints on the system variables in the optimization problem at each step of a receding horizon control framework. We prove correctness of our algorithms, and present experimental results for controller synthesis for building energy and climate control.s for building energy and climate control.  +
• We present a mathematical programming-base … We present a mathematical programming-based method for model predictive control of discrete-time cyber- physical systems subject to signal temporal logic (STL) speci- fications. We describe the use of STL to specify a wide range of properties of these systems, including safety, response and bounded liveness. For synthesis, we encode STL specifications as mixed integer-linear constraints on the system variables in the optimization problem at each step of model predictive control. We present experimental results for controller synthesis on simplified models of a smart micro-grid and HVAC system.els of a smart micro-grid and HVAC system.  +
• We present a mathematical programming-base … We present a mathematical programming-based method for optimal con- trol of nonlinear systems subject to temporal logic task specifications. We specify tasks using a fragment of linear temporal logic (LTL) that allows both finite- and infinite-horizon properties to be specified, including tasks such as surveillance, periodic motion, repeated assembly, and environmental monitoring. Our method di- rectly encodes an LTL formula as mixed-integer linear constraints on the system variables, avoiding the computationally expensive process of creating a finite ab- straction. Our approach is efficient; for common tasks our formulation uses significantly fewer binary variables than related approaches and gives the tightest possible convex relaxation. We apply our method on piecewise affine systems and certain classes of differentially flat systems. In numerical experiments, we solve temporal logic motion planning tasks for high-dimensional (10+) continuous systems.high-dimensional (10+) continuous systems.  +
• We present a mathematical programming-base … We present a mathematical programming-based method for optimal control of discrete-time nonlinear systems subject to temporal logic task specifications. We use linear temporal logic (LTL) to specify a wide range of properties and tasks, such as safety, progress, response, surveillance, repeated assembly, and environmental monitoring. Our method directly encodes an LTL formula as mixed-integer linear constraints on the continuous system variables, avoiding the computationally expensive processes of creating a finite abstraction of the system and a Bu Ìchi automaton for the specification. In numerical experiments, we solve temporal logic motion planning tasks for high-dimensional (more than 10 continuous states) dynamical systems.n 10 continuous states) dynamical systems.  +
• We present a mathematical reconstruction … We present a mathematical reconstruction </br>of the kinematics and dynamics of flight initiation as observed in high-speed video recordings of the insect Drosophila melanogaster. The behavioral dichotomy observed in the fruit flies' flight initiation sequences, as a response to different stimuli, was reflected in two contrasting sets of dynamics once the flies had become airborne. By reconstructing the dynamics of unconstrained motion during flight initiations, we assess the fly's responses (generation of forces and moments) amidst these two dynamic patterns. Moreover, we introduce a 3D visual tracking algorithm as a tool to analyze the wing kinematics applied by the insect, and investigate their relation(s) to the production of these aerodynamic forces. Using this framework we formulate different hypotheses about the modulation of flight forces and moments during flight initiation as a way torefining our understanding of insect flight control.,r understanding of insect flight control.,  +
• We present a method for designing robust c … We present a method for designing robust con- trollers for dynamical systems with linear temporal logic specifications. We abstract the original system by a finite Markov Decision Process (MDP) that has transition probabilities in a specified uncertainty set. A robust control policy for the MDP is generated that maximizes the worst-case probability of satisfying the specification over all transition probabilities in the uncertainty set. To do this, we use a procedure from probabilistic model checking to combine the system model with an automaton representing the specification. This new MDP is then transformed into an equivalent form that satisfies assumptions for stochastic shortest path dynamic programming. A robust version of dynamic programming allows us to solve for a eps-suboptimal robust control policy with time complexity O(log1/eps) times that for the non-robust case. We then implement this control policy on the original dynamical system.l policy on the original dynamical system.  +
• We present a method for mending strategies … We present a method for mending strategies for GR(1) specifications. Given the addition or removal of edges from the game graph describing a problem (essentially transition rules in a GR(1) specification), we apply a μ-calculus formula to a neighborhood of states to obtain a âlocal strategyâ that navigates around the invalidated parts of an original synthesized strategy. Our method may thus avoid global resynthesis while recovering correctness with respect to the new specification. We illustrate the results both in simulation and on physical hardware for a planar robot surveillance task.ware for a planar robot surveillance task.  +
• We present a methodology for automatic syn … We present a methodology for automatic synthesis of embedded control software that incorporates a class of linear temporal logic (LTL) specifications sufficient to describe a wide range of properties including safety, stability, progress, obligation, response and guarantee. To alleviate the associated computational complexity of LTL synthesis, we propose a receding horizon framework that effectively reduces the synthesis problem into a set of smaller problems. The proposed control architecture consists of a goal generator, a trajectory planner, and a continuous controller. The goal generator reduces the trajectory generation problem into a sequence of smaller problems of short horizon while preserving the desired system-level temporal properties. Subsequently, in each iteration, the trajectory planner solves the corresponding short-horizon problem with the currently observed state as the initial state and generates a feasible trajectory to be implemented by the continuous controller. Based on the simulation property, we show that the composition of the goal generator, trajectory planner and continuous controller and the corresponding receding horizon framework guarantee the correctness of the system with respect to its specification regardless of the environment in which the system operates. In addition, we present a response mechanism to handle failures that may occur due to a mismatch between the actual system and its model. The effectiveness of the proposed technique is demonstrated through an example of an autonomous vehicle navigating an urban environment. This example also illustrates that the system is not only robust with respect to exogenous disturbances but is also capable of properly handling violation of the environment assumption that is explicitly stated as part of the system specification .ated as part of the system specification .  +
• We present a set of primitive operations w … We present a set of primitive operations which forms the core of a robot system</br>description and control language. The actions of the individual primitives are derived</br>from the mathematical structure of the equations of motion for constrained mechanical</br>systems. The recursive nature of the primitives allows composite robots to be constructed</br>from more elementary daughter robots. We review a few pertinent results of classical</br>mechanics, describe the functionality of our primitive operations, and present several</br>different hierarchical strategies for the description and control of a two-fingered hand</br>holding a box.trol of a two-fingered hand holding a box.  +
• We present a simple geometric analysis of … We present a simple geometric analysis of wireless</br>connectivity in vehicle networks. We introduce a localized</br>notion of connectedness, and construct a function that measures</br>the robustness of this local connectedness to variations</br>in position. Under a mild feasibility hypothesis, this function</br>provides a sufficient condition for global connectedness of</br>the network. Further, it is distributed, in the sense that</br>both the function and its gradients can be calculated using</br>only neighbor-to-neighbor communications. It can thus form</br>the basis for distributed motion-control algorithms which</br>respect connectivity constraints. We conclude with two simple</br>examples of target applications.wo simple examples of target applications.  +
• We present a synthesis method for communic … We present a synthesis method for communication protocols for active safety applications that satisfy certain formal specifications on quality of service requirements. The protocols are developed to provide reliable communication services for automobile active safety applications. The synthesis method transforms a specification into a distributed implementation of senders and receivers that together satisfy the quality of service requirements by transmitting messages over an unreliable medium. We develop a specification language and an execution model for the implementations, and demonstrate the viability of our method by developing a protocol for a traffic scenario in which a car runs a red light at a busy intersection.r runs a red light at a busy intersection.  +
• We present a theory of contracts that is c … We present a theory of contracts that is centered around reacting to failures and explore it from a general assume-guarantee perspective as well as from a concrete context of automated synthesis from linear temporal logic (LTL) specifications, all of which are compliant with a contract metatheory introduced by Benveniste et al. We also show how to obtain an automated procedure for synthesizing reactive assume-guarantee contracts and implementations that capture ideas like optimality and robustness based on assume-guarantee lattices computed from antitone Galois connection fixpoints. Lastly, we provide an example of a “reactive GR(1)” contract and a simulation of its implementation.ct and a simulation of its implementation.  +
• We present an approach that allows mission … We present an approach that allows mission and contingency management to be achieved in a distributed and dynamic manner without any central control over multiple software modules. This approach comprises two key elements---a mission management subsystem and a Canonical Software Architecture (CSA) for a planning subsystem. The mission management subsystem works in conjunction with the planning subsystem to dynamically replan in reaction to contingencies. The CSA ensures the consistency of the states of all the software modules in the planning subsystem. System faults are identified and replanning strategies are performed distributedly in the planning and the mission management subsystems through the CSA. The approach has been implemented and tested on Alice, an autonomous vehicle developed by the California Institute of Technology for the 2007 DARPA Urban Challenge.nology for the 2007 DARPA Urban Challenge.  +
• We present an automated model reduction al … We present an automated model reduction algorithm that uses quasi-steady state approximation based reduction to minimize the error between the desired outputs. Additionally, the algorithm minimizes the sensitivity of the error with respect to parameters to ensure robust performance of the reduced model in the presence of parametric uncertainties. We develop the theory for this model reduction algorithm and present the implementation of the algorithm that can be used to perform model reduction of given SBML models. To demonstrate the utility of this algorithm, we consider the design of a synthetic biological circuit to control the population density and composition of a consortium consisting of two different cell strains. We show how the model reduction algorithm can be used to guide the design and analysis of this circuit.e the design and analysis of this circuit.  +
• We present an identification framework for … We present an identification framework for biochemical systems that allows multiple candidate models to be compared. This framework is designed to select a model that fits the data while maintaining model simplicity. The model identification task is divided into a parameter estimation stage and a model comparison stage. Model selection is based on calculating Akaike's Information Criterion, which is a systematic method for determining the model that best represents a set of experimental data. Two case studies are presented: a simulated transcriptional control circuit and a system of oscillators that has been built and characterized in vitro. In both examples the multi-model framework is able to discriminate between model candidates to select the one that best describes the data.lect the one that best describes the data.  +
• We present the results from a flight exper … We present the results from a flight experiment demonstrating two significant advances in software enabled</br>control: optimization-based control using real-time trajectory generation and logical programming environments for</br>formal analysis of control software. Our demonstration platform consisted of a human-piloted F-15 jet flying together</br>with an autonomous T-33 jet. We describe the behavior of the system in two scenarios. In the first, nominal state</br>communications were present and the autonomous aircraft maintained formation as the human pilot flew maneuvers. In</br>the second, we imposed the loss of high-rate communications and demonstrated an autonomous safe âlost wingmanâ</br>procedure to increase separation and re-acquire contact. The flight demonstration included both a nominal formation</br>flight component and an execution of the lost wingman scenario.an execution of the lost wingman scenario.  +
• We propose a compositional stability analy … We propose a compositional stability analysis methodology for verifying properties of systems that are interconnections of multiple subsystems. The proposed method assembles stability certificates for the interconnected system based on the certificates for the input-output properties of the subsystems. The hierarchy in the analysis is achieved by utilizing dual decomposition ideas in optimization. Decoupled subproblems establish subsystem level input-output properties whereas the ``master'' problem imposes and updates the conditions on the subproblems toward ensuring interconnected system level stability properties. Both global stabilityanalysis and region-of-attraction analysis are discussed.gion-of-attraction analysis are discussed.  +
• We propose a general algorithm for the sys … We propose a general algorithm for the systematic design of feedback strategies to stabilize the evolutionary dynamics of a generic disease model using an H1 approach. We show that designing antibody concentrations can be cast as an H1 state feedback synthesis problem, where the feedback gain is constrained to not only be strictly diagonal, but also that its diagonal elements satisfy an overdetermined set of linear equations. Leveraging recent results in positive systems, we additionally show that our algorithm always converges to a stabilizing controller.ays converges to a stabilizing controller.  +
• We propose a method for eliminating variab … We propose a method for eliminating variables from component specifications during the decomposition of GR(1) properties into contracts. The variables that can be eliminated are identified by parameterizing the communication architecture to investigate the dependence of realizability on the availability of information. We prove that the selected variables can be hidden from other components, while still expressing the resulting specification as a game with full information with respect to the remaining variables. The values of other variables need not be known all the time, so we hide them for part of the time, thus reducing the amount of information that needs to be communicated between components. We improve on our previous results on algorithmic decomposition of GR(1) properties, and prove existence of decompositions in the full information case. We use semantic methods of computation based on binary decision diagrams. To recover the constructed specifications so that humans can read them, we implement exact symbolic minimal covering over the lattice of integer orthotopes, thus deriving minimal formulae in disjunctive normal form over integer variable intervals.rmal form over integer variable intervals.  +
• We propose a methodology for abstracting d … We propose a methodology for abstracting discrete-time piecewise-affine systems influenced by additive continuous environment variables, to synthesize correct-by-construction controllers from linear temporal logic specifications. The proposed algorithm partitions the environment domain into polytopes, considered as modes controlled by the environment. In each mode the environment variable is treated as a bounded disturbance for the system. Mode polytopes are iteratively enlarged while a strategy isomorphism between successive system partitions can be constructed. Isomorphisms are obtained by solving the stable marriage problem after proving that our case admits a unique solution. This leads to mapping high-level symbolic variables to equivalence classes of polytopes, instead of single polytopes as in other works. We thus avoid the need to merge partitions, which can create sliver polytopes, causing numerical problems during reachability computations. The approach enables using the same strategy over partitions that have an isomorphic subgraph relevant to the strategy. Reachability checks between neighboring partitions are used to reduce non-determinism introduced by switching and allow continuous restoration of discrete state. If bifurca- tions occur that prevent strategy reuse, then switched system game synthesis is performed, and a logic modeling formalism proposed that avoids trivial cyclic counterexamples.hat avoids trivial cyclic counterexamples.  +
• We propose a methodology for automatic syn … We propose a methodology for automatic synthesis of embedded control software that accounts for exogenous disturbances. The resulting system is guaranteed, by construction, to satisfy a given specification expressed in linear temporal logic. The embedded control software consists of three components: a goal generator, a trajectory planner, and a continuous controller. We demonstrate the effectiveness of the proposed technique through an example of an autonomous vehicle navigating an urban environment. This example also illustrates that the system is not only robust with respect to exogenous disturbances but also capable of handling violation of the environment assumptions. violation of the environment assumptions.  +
• We propose a model for planar carangiform … We propose a model for planar carangiform swimming based on conservative equations for</br>the interaction of a rigid body and an incompressible fluid. We account for the generation</br>of thrust due to vortex shedding through controlled coupling terms. We investigate the</br>correct form of this coupling experimentally with a robotic propulsor, comparing its</br>observed behavior with that predicted by unsteady hydrodynamics. Our analysis of thrust</br>generation by an oscillating hydrofoil allows us to characterize and evaluate certain</br>families of gaits. Our final swimming model takes the form of a control-affine nonlinear</br>system.form of a control-affine nonlinear system.  +
• We propose a negative feedback architectur … We propose a negative feedback architecture that regulates activity of artificial genes, or "genelets", to meet their output downstream demand, achieving robustness with respect to uncertain open-loop output production rates. In particular, we consider the case where the outputs of two genelets interact to form a single assembled product. We show with analysis and experiments that negative autoregulation matches the production and demand of the outputs: the magnitude of the regulatory signal is proportional to the error between the circuit output concentration and its actual demand. This two-device system is experimentally implemented using in vitro transcriptional networks, where reactions are systematically designed by optimizing nucleic acid sequences with publicly available software packages. We build a predictive ordinary differential equation (ODE) model that captures the dynamics of the system, and can be used to numerically assess the scalability of this architecture to larger sets of interconnected genes. Finally, with numerical simulations we contrast our negative autoregulation scheme with a cross-activation architecture, which is less scalable and results in slower response times.able and results in slower response times.  +
• We propose a new abstraction refinement pr … We propose a new abstraction refinement procedure based on machine learning to improve the performance of nonlinear constraint solving algorithms on large-scale problems. The proposed approach decomposes the original set of constraints into smaller subsets, and uses learning algorithms to propose sequences of abstractions that take the form of conjunctions of classifiers. The core procedure is a refinement loop that keeps improving the learned results based on counterexamples that are obtained from partial constraints that are easy to solve. Experiments show that the proposed techniques significantly improve the performance of state-of-the-art constraint solvers on many challenging benchmarks. The mechanism is capable of producing intermediate symbolic abstractions that are also important for many applications and for understanding the internal structures of hard constraint solving problems.tures of hard constraint solving problems.  +
• We propose a planar model for the swimming … We propose a planar model for the swimming </br>of certain marine animals based on </br>reduced Euler-Lagrange equations for the interaction of a rigid body and </br>an incompressible fluid. </br>This model assumes the form of a control-affine nonlinear system with drift;</br>preliminary accessibility analysis suggests its utility in predicting</br>efficacious gaits for piscimimetic robots. </br>We account for the generation of thrust due to </br>vortex shedding through controlled coupling terms. At the</br>heart of this coupling is an abstraction from hydrofoil theory; </br>we investigate its applicability to real</br>swimming using an articulated robotic caudal fin. We compare the </br>observed behavior of our experimental apparatus to that predicted </br>numerically by steady hydrodynamic theory.numerically by steady hydrodynamic theory.  +
• We propose a procedure for the synthesis o … We propose a procedure for the synthesis of con- trol protocols for systems governed by nonlinear differential equations and constrained by temporal logic specifications. This procedure relies on a particular finite-state abstraction of the un- derlying continuous dynamics and a discrete representation of the external environmental signals. A two-player game formulation provides computationally efficient means to construct a discrete strategy based on the finite-state model. We focus on systems with differentially flat outputs, which, in a straightforward manner, allows the construction of continuous control signals from the discrete transitions dictated by the discrete strategy. The resulting continuous-time output trajectories are provably guaranteed to robustly satisfy the original specifications.ustly satisfy the original specifications.  +
• We propose an adversarial, time-varying te … We propose an adversarial, time-varying test-synthesis procedure for safety-critical systems without requiring specific knowledge of the underlying controller steering the system. From a broader test and evaluation context, determination of difficult tests of system behavior is important as these tests would elucidate problematic system phenomena before these mistakes can engender problematic outcomes, e.g. loss of human life in autonomous cars, costly failures for airplane systems, etc. Our approach builds on existing, simulation-based work in the test and evaluation literature by offering a controller-agnostic test-synthesis procedure that provides a series of benchmark tests with which to determine controller reliability. To achieve this, our approach codifies the system objective as a timed reach-avoid specification. Then, by coupling control barrier functions with this class of specifications, we construct an instantaneous difficulty metric whose minimizer corresponds to the most difficult test at that system state. We use this instantaneous difficulty metric in a game-theoretic fashion, to produce an adversarial, time-varying test-synthesis procedure that does not require specific knowledge of the system's controller, but can still provably identify realizable and maximally difficult tests of system behavior. Finally, we develop this test-synthesis procedure for both continuous and discrete-time systems and showcase our test-synthesis procedure on simulated and hardware examples.cedure on simulated and hardware examples.  +
• We propose formal means for synthesizing s … We propose formal means for synthesizing switching protocols that determine the sequence in which the modes of a switched system are activated to satisfy certain high-level specifications in linear temporal logic (LTL). The synthesized protocols are robust against exogenous disturbances on the continuous dynamics and can react to possibly adversarial events (both external and internal). Finite-state approximations that abstract the behavior of the underlying continuous dynamics are defined using finite transition systems. Such approximations allow us to transform the continuous switching synthesis problem into a discrete synthesis problem in the form of a two-player game between the system and the environment, where the winning conditions represent the high-level temporal logic specifications. Restricting to an expressive subclass of LTL formulas, these temporal logic games are amenable to solutions with polynomial-time complexity. By construction, existence of a discrete switching strategy for the discrete synthesis problem guarantees the existence of a switching protocol that can be implemented at the continuous level to ensure the correctness of the nonlinear switched system and to react to the environment at run time.d to react to the environment at run time.  +
• We propose formal means for synthesizing s … We propose formal means for synthesizing switching protocols that determine the sequence in which the modes of a switched system are activated to satisfy certain high-level specifications in linear temporal logic. The synthesized protocols are robust against exogenous disturbances on the continuous dynamics. Two types of finite tran- sition systems, namely (deterministic) under-approximations and over-approximations (potentially with nondeterministic transitions), that abstract the behavior of the underlying continuous dynamics are defined. In particular, we show that the discrete synthesis problem for an under-approximation can be formulated as a model checking problem, whereas that for an over-approximation can be transformed into a two-player game. Both of these formulations are amenable to efficient, off-the-shelf software tools. By construction, existence of a discrete switching strategy for the discrete synthesis problem guarantees the existence of a continuous switching protocol for the continuous synthesis problem, which can be implemented at the continuous level to ensure the correctness of the nonlinear switched system. Moreover, the proposed framework can be straightforwardly extended to accommodate specifications that require reacting to possibly adversarial external events.g to possibly adversarial external events.  +
• We provide a new perspective on using form … We provide a new perspective on using formal methods to model specifications and synthesize implementations for the design of biological circuits. In synthetic biology, design objectives are rarely described formally. We present an assume-guarantee contract framework to describe biological circuit design objectives as formal specifications. In our approach, these formal specifications are implemented by circuits modeled by ordinary differential equations, yielding a design framework that can be used to design complex synthetic biological circuits at scale. We describe our approach using the design of a biological AND gate as a motivating, running example.AND gate as a motivating, running example.  +
• We regard the internal configuration of a … We regard the internal configuration of a deformable body, together with</br>its position and orientation in ambient space, as a point in a trivial</br>principal fiber bundle over the manifold of body deformations.</br>In the presence of a symmetry which leads to a conservation law, the </br>self-propulsion of such a body due to cyclic changes in shape is </br>described by the corresponding mechanical connection on the configuration </br>bundle. In the presence of viscous drag sufficient to negate inertial</br>effects, the viscous connection takes the place of the mechanical connection. </br>Both connections may be represented locally in terms of the variables</br>describing the body's shape. In the presence of both inertial and</br>viscous effects, the equations of motion may be written in terms of the</br>two local connection forms as an affine control system with drift on</br>the manifold of configurations and body momenta. We apply techniques</br>from nonlinear control theory to the equations in this form to obtain</br>criteria for a particular form of accessibility.ia for a particular form of accessibility.  +
• We study a distributed multi-agent optimiz … We study a distributed multi-agent optimization problem of minimizing the sum of convex objective functions. A new decentralized optimization algorithm is introduced, based on dual decomposition, together with the subgradient method for finding the optimal solution. The iterative algorithm is implemented on a multi-hop network and is designed to handle communication delays. The convergence of the algorithm is proved for communication networks with bounded delays. An explicit bound, which depends on the communication delays, on the convergence rate is given. A numerical comparison with a decentralized primal algorithm shows that the dual algorithm converges faster, with less communication.converges faster, with less communication.  +
• We study a simple pursuit scenario in whic … We study a simple pursuit scenario in which the</br>pursuer has potential access to an additional off-board global</br>sensor. However, the global sensor can be used for either of</br>two purposes: to improve the state estimate of the pursuer, or</br>to obtain more data about the trajectory being tracked. The</br>problem is to determine the variation in the performance of</br>the system as the global sensor changes its behavior. We use a</br>stochastic strategy to optimize over the transmission pattern</br>of the global sensor.transmission pattern of the global sensor.  +
• We study automated test generation for ver … We study automated test generation for verifying discrete decision-making modules in autonomous systems. We utilize linear temporal logic to encode the requirements on the system under test in the system specification and the behavior that we want to observe during the test is given as the test specification which is unknown to the system. First, we use the specifications and their corresponding non-deterministic Bu ̈chi automata to generate the specification product automaton. Second, a virtual product graph representing the high-level interaction between the system and the test environment is constructed modeling the product automaton encoding the system, the test environment, and specifications. The main result of this paper is an optimization problem, framed as a multi-commodity network flow problem, that solves for constraints on the virtual product graph which can then be projected to the test environment. Therefore, the result of the optimization problem is reactive test synthesis that ensures that the system meets the test specifications along with satisfying the system specifications. This framework is illustrated in simulation on grid world examples, and demonstrated on hardware with the Unitree A1 quadruped, wherein dynamic locomotion behaviors are verified in the context of reactive test environments.the context of reactive test environments.  +
• We study the continuous-time consensus pro … We study the continuous-time consensus problem where nodes on a graph attempt to reach average consensus. We consider communication graphs that can be decomposed into a hierarchical structure and present a consensus scheme that exploits this hierarchical topology. The scheme consists of splitting the overall graph into layers of smaller connected subgraphs. </br>Consensus is performed within the individual subgraphs starting with those of the lowest layer of the hierarchy and moving upwards. Certain ``leader'' nodes bridge the layers of the hierarchy. By exploiting the increased convergence speed of the smaller subgraphs, we show </br>how this scheme can achieve faster overall convergence than the standard single-stage consensus algorithm running on the full graph topology. The result presents some fundamentals on how the communication architecture influences the global performance of a networked system. Analytical </br>performance bounds are derived and simulations provided to illustrate the effectiveness of the scheme.llustrate the effectiveness of the scheme.  +
• We study the dynamic and static input outp … We study the dynamic and static input output behavior of several primitive genetic interactions and their e↵ect on the performance of a genetic signal di↵erentiator. In a simplified design, several requirements for the linearity and time-scales of processes like transcription, translation and competitive promoter binding were introduced. By ex- perimentally probing simple genetic constructs in a cell-free experimental environment and fitting semi-mechanistic models to these data, we show that some of these require- ments can be verified, while others are only met with reservations in certain operational regimes. Analyzing the linearized model of the resulting genetic network we conclude that it approximates a di↵erentiator with relative degree one. Taking also the discovered non-linearities into account and using a describing function approach, we further deter- mine the particular frequency and amplitude ranges where the genetic di↵erentiator can be expected to behave as such.ntiator can be expected to behave as such.  +
• We study the dynamic stability of low Reyn … We study the dynamic stability of low Reynolds number swimming near a plane wall from a control-theoretic viewpoint. We consider a special class of swimmers having a constant shape, focus on steady motion parallel to the wall, and derive conditions under which it is passively stable without sensing or feedback. We study the geometric structure of the swimming equation and highlight the relation between stability and reversing symmetry of the dynamical system. Finally, our numerical simulations reveal the existence of stable periodic motion. The results have implications for design of miniature robotic swimmers, as well as for explaining the attraction of micro-organisms to surfaces.attraction of micro-organisms to surfaces.  +
• We study the dynamics of the relative moti … We study the dynamics of the relative motion of</br>satellites in the gravitational field of the Earth, including</br>the effects of the bulge of the Earth (the $J_2$ effect). Using</br>Routh reduction and dynamical systems ideas, a method is found</br>that locates orbits such that the cluster of satellites remains</br>close with very little dispersing, even with no controls. The use of</br>controls in the context of this natural dynamics is studied to maintain and</br>achieve precision formations.maintain and achieve precision formations.  +
• We study the effect of quantization on the … We study the effect of quantization on the performance</br>of a scalar dynamical system. We provide an expression</br>for calculation of the LQR cost of a dynamical system for</br>a general quantizer. Using the high-rate approximation, we</br>evaluate it for two commonly used quantizers: uniform and</br>logarithmic. We also provide a lower bound on performance</br>of the optimal quantizer based on entropy arguments and</br>consider the case when the channel drops data packets</br>stochastically.channel drops data packets stochastically.  +
• We study the problem of using a small numb … We study the problem of using a small number </br>of mobile sensors to monitor various threats in a geographical </br>area. Using some recent results on stochastic sensor scheduling, </br>we propose a stochastic sensor movement strategy. We present </br>simple conditions under which it is not possible to maintain a </br>bounded estimate error covariance for all the threats. We also </br>study a simple sub-optimal algorithm to generate stochastic </br>trajectories. Simulations are presented to illustrate the results.s are presented to illustrate the results.  +
• We study the synthesis problem of a LQR co … We study the synthesis problem of a LQR controller when the matrix describing the control</br>law is additionally constrained to lie in a particular vector space. Our motivation is the use of</br>such control laws to stabilize networks of autonomous agents in a decentralized fashion; with</br>the information </br>ow being dictated by the constraints of a pre-specified topology. We formulate</br>the problem as an optimization problem and provide numerical procedures to solve it. Then we</br>apply the technique to the decentralized vehicle formation control problem and show that the</br>topology can have a significant effect on the optimal cost. We also discuss the issue of optimal</br>topology.lso discuss the issue of optimal topology.  +
• We study the synthesis problem of an LQR c … We study the synthesis problem of an LQR controller when the matrix describing the control law is</br>constrained to lie in a particular vector space. Our motivation is the use of such control laws to stabilize</br>networks of autonomous agents in a decentralized fashion; with the information flow being dictated by</br>the constraints of a pre-specified topology. In this paper, we consider the finite-horizon version of the</br>problem and provide both a computationally intensive optimal solution and a sub-optimal solution that</br>is computationally more tractable. Then we apply the technique to the decentralized vehicle formation</br>control problem and show that the loss in performance due to the use of the sub-optimal solution is not</br>huge; however the topology can have a large effect on performance.gy can have a large effect on performance.  +
• When autonomous robots interact with human … When autonomous robots interact with humans, such as during autonomous driving, explicit safety guarantees are crucial in order to avoid potentially life-threatening accidents. Many data-driven methods have explored learning probabilistic bounds over human agents' trajectories (i.e. confidence tubes that contain trajectories with probability ), which can then be used to guarantee safety with probability . However, almost all existing works consider . The purpose of this paper is to argue that (1) in safety-critical applications, it is necessary to provide safety guarantees with , and (2) current learning-based methods are ill-equipped to compute accurate confidence bounds at such low . Using human driving data (from the highD dataset), as well as synthetically generated data, we show that current uncertainty models use inaccurate distributional assumptions to describe human behavior and/or require infeasible amounts of data to accurately learn confidence bounds for . These two issues result in unreliable confidence bounds, which can have dangerous implications if deployed on safety-critical systems.ns if deployed on safety-critical systems.  +
• When used as part of a hybrid controller, … When used as part of a hybrid controller, finite- memory strategies synthesized from LTL specifications rely on an accurate dynamics model in order to ensure correctness of trajectories. In the presence of uncertainty about this underlying model, there may exist unexpected trajectories that manifest as unexpected transitions under control of the strategy. While some disturbances can be captured by augmenting the dynamics model, such approaches may be conservative in that bisimulations may fail to exist for which strategies can be synthesized. In this paper, we characterize the tolerance of such hybrid controllers - synthesized for generalized reactivity(1) specifications- to disturbances that appear as unexpected jumps (transitions) to states in the discrete strategy part of the con- troller. As a first step, we show robustness to certain unexpected transitions that occur in a finite-manner, i.e., despite a certain number of unexpected jumps, the sequence of states obtained will still meet a stricter specification and hence the original specification. Additionally, we propose algorithms to improve robustness by increasing tolerance to additional disturbances. A robot gridworld example is presented to demonstrate the application of the developed ideas and also to obtain empirical computational and memory cost estimates.l computational and memory cost estimates.  +
• When used as part of a hybrid controller, … When used as part of a hybrid controller, finite-memory strategies synthesized from linear-time temporal logic (LTL) specifications rely on an accurate dynamics model in order to ensure correctness of trajectories. In the presence of uncertainty about the underlying model, there may exist unexpected trajectories that manifest as unexpected transitions under control of the strategy. While some disturbances can be captured by augment- ing the dynamics model, such approaches may be con- servative in that bisimulations may fail to exist for which strategies can be synthesized. In this paper, we consider games of the GR(1) fragment of LTL, and we character- ize the tolerance of hybrid controllers to perturbations that appear as unexpected jumps (transitions) to states in the discrete strategy part of the controller. As a first step, we show robustness to certain unexpected transi- tions that occur in a finite manner, i.e., despite a certain number of unexpected jumps, the sequence of states ob- tained will still meet a stricter specification and hence the original specification. Additionally, we propose al- gorithms to improve robustness by increasing tolerance to additional disturbances. A robot gridworld example is presented to demonstrate the application of the de- veloped ideas and also to perform empirical analysis.as and also to perform empirical analysis.  +
• While complex dynamic biological networks … While complex dynamic biological networks control gene expression in all living organisms, the forward engineering of comparable synthetic networks remains challenging. The current paradigm of characterizing synthetic networks in cells results in lengthy design-build-test cycles, minimal data collection, and poor quantitative characterization. Cell-free systems are appealing alternative environments, but it remains questionable whether biological networks behave similarly in cell-free systems and in cells. We characterized in a cell-free system the 'repressilator,' a three-node synthetic oscillator. We then engineered novel three, four, and five-gene ring architectures, from characterization of circuit components to rapid analysis of complete networks. When implemented in cells, our novel 3-node networks produced population-wide synchronized oscillations and 95% of 5-node oscillator cells oscillated for up to 72 hours. Oscillation periods in cells matched the cell-free system results for all networks tested. An alternate forward engineering paradigm using cell-free systems can thus accurately capture cellular behavior.thus accurately capture cellular behavior.  +
• While the use of formal synthesis for robo … While the use of formal synthesis for robotics problems in which the environment may act adversarially provides for exactârather than probabilisticâcorrectness of controllers, such methods are impractical when the adversary can move freely in a large portion of the workspace. As is well-known, this is due to exponential growth in the state space with the addition of each new problem variable. Furthermore, such an approach is overly conservative because most configurations will not be reached in typical runs. Rather than entirely abandon the discrete game view, we propose a combined method that ensures exact satisfaction of a given specification, expressed in linear temporal logic, while providing a lower bound on robot-obstacle distance throughout execution. Our method avoids explicit encoding of the moving obstacle and thus substantially reduces the reactive synthesis problem size, while allowing other nondeterministic variables to still be included in the specification. Our approaches centers on modeling obstacle motion as changes in the presence of a virtual static obstacle, and performing incremental synthesis in response. The algorithm is tested in application to a planar surveillance task.application to a planar surveillance task.  +
• Whole-cell bioconversion of technical lign … Whole-cell bioconversion of technical lignins using Pseudomonas putida strains overexpressing amine transaminases (ATAs) has the potential to become an eco-efficient route to produce phenolic amines. Here, a novel cell growth-based screening method to evaluate the in vivo activity of recombinant ATAs towards vanillylamine in P. putida KT2440 was developed. It allowed the identification of the native enzyme Pp-SpuC-II and ATA from Chromobacterium violaceum (Cv-ATA) as highly active towards vanillylamine in vivo. Overexpression of Pp-SpuC-II and Cv-ATA in the strain GN442ΔPP_2426, previously engineered for reduced vanillin assimilation, resulted in 94- and 92-fold increased specific transaminase activity, respectively. Whole-cell bioconversion of vanillin yielded 0.70 ± 0.20 mM and 0.92 ± 0.30 mM vanillylamine, for Pp-SpuC-II and Cv-ATA, respectively. Still, amine production was limited by a substantial re-assimilation of the product and formation of the by-products vanillic acid and vanillyl alcohol. Concomitant overexpression of Cv-ATA and alanine dehydrogenase from Bacillus subtilis increased the production of vanillylamine with ammonium as the only nitrogen source and a reduction in the amount of amine product re-assimilation. Identification and deletion of additional native genes encoding oxidoreductases acting on vanillin are crucial engineering targets for further improvement.gineering targets for further improvement.  +
• With the advent of powerful computing and … With the advent of powerful computing and efficient computational algorithms,</br>real-time solutions to constrained optimal control problems are nearing a reality. In</br>this thesis, we develop a computationally efficient Nonlinear Trajectory Generation</br>(NTG) algorithm and describe its software implementation to solve, in real-time,</br>nonlinear optimal trajectory generation problems for constrained systems. NTG is</br>a nonlinear trajectory generation software package that combines nonlinear control</br>theory, B-spline basis functions, and nonlinear programming. We compare NTG</br>with other numerical optimal control problem solution techniques, such as direct</br>collocation, shooting, adjoints, and differential inclusions.</br>We demonstrate the performance of NTG on the Caltech Ducted Fan testbed.</br>Aggressive, constrained optimal control problems are solved in real-time for hover-</br>to-hover, forward flight, and terrain avoidance test cases. Real-time trajectory</br>generation results are shown for both the two-degree of freedom and receding</br>horizon control designs. Further experimental demonstration is provided with the</br>station-keeping, reconfiguration, and deconfiguration of micro-satellite formation</br>with complex nonlinear constraints. Successful application of NTG in these cases</br>demonstrates reliable real-time trajectory generation, even for highly nonlinear</br>and non-convex systems. The results are among the first to apply receding horizon</br>control techniques for agile flight in an experimental setting, using representative dynamics and computation.g representative dynamics and computation.  +
• Without accounting for the limited availab … Without accounting for the limited availability of shared cellular resources, the standard model of gene expression fails to reliably predict experimental data obtained in vitro. To overcome this limitation, we develop a dynamical model of gene expression explicitly modeling competition for scarce resources. In addition to accurately describing the experimental data, this model only depends on a handful of easily identifiable parame- ters with clear physical interpretation. Based on this model, we then characterize the combinations of protein concentrations that are simultaneously realizable with shared resources. As application examples, we demonstrate how the results can be used to explain similarities/differences among different in vitro extracts, furthermore, we illustrate that accounting for resource usage is essential in circuit design considering the toggle switch.cuit design considering the toggle switch.  +