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

A bootstrappable bio-plausible design for visual pose stabilization + (We consider the problem of purely visual p … We consider the problem of purely visual pose stabilization of a second-order rigid-body system: how to choose forces and torques, based on the visual input alone, such that the view converges to a memorized goal image. Emphasis has been given to the bio-plausibility of the computation, in the sense that the control laws could be in principle implemented on the neural substrate of simple insects. We show that stabilizing laws can be realized by bilinear/quadratic operations on the visual input. Moreover, the control laws can be ``bootstrapped'' (learned unsupervisedly) from experience, which further substantiate the bio-plausibility of such computation. the bio-plausibility of such computation.)
Specifying and Analyzing Networked and Layered Control Systems Operating on Multiple Clocks + (We consider the problem of reasoning about … We consider the problem of reasoning about networked and layered control systems using assume-guarantee specifications. As these systems are formed by the interconnection of components that operate under various clocks, we introduce a new logic, Multiclock Logic (MCL), to be able to express the requirements of components form the point of view of their local clocks. Specifying components locally promotes independent design and component reuse. We carry out a contract-based analysis of a control system implemented via two control algorithms (model predictive control and feedback linearization) running on their own processors and clocks. Then we implement each of the contracts to build a system. The system performs as desired when the requirements derived from our system-level analysis are respected. Violating the constraints required by the contract-based analysis of the system leads to error.sed analysis of the system leads to error.)
Temporal Logic Control of Switched Affine Systems with an Application in Fuel Balancing + (We consider the problem of synthesizing hi … We consider the problem of synthesizing hier- archical controllers for discrete-time switched affine systems subject to exogenous disturbances that guarantee that the trajectories of the system satisfy a high-level specification expressed as a linear temporal logic formula. Our method builds upon recent results on temporal logic planning and embedded controller synthesis. First, the control problem is lifted to a discrete level by constructing a finite transition system that abstracts the behavior of the underlying switched system. At the discrete level, we recast the problem as a two player temporal logic game by treating the environment driven switches as adversaries. The solution strategy for the game (i.e. the discrete plan) is then implemented at the continuous level by solving finite-horizon optimal control problems that establish reachability between discrete states and that compensate the effects of continuous disturbances. We also extend the earlier work by making efficient use of propositions in the temporal logic formula to drive the abstraction procedure and to facilitate the computation of continuous input at implementation time.An aircraft fuel system example is formulated; and solved using the proposed method. This sample problem demonstrates the applicability of the abstraction procedure and correct-by-construction controllers to regulate the fuel levels in multiple tanks during interesting operations like aerial refueling.eresting operations like aerial refueling.)
Distributed Synthesis of Control Protocols for Smart Camera Networks + (We consider the problem of synthesizing co … We consider the problem of synthesizing control protocols for smart camera networks where the goal is to guarantee that certain linear temporal logic (LTL) specifications related to a given surveillance task are met. We first present a centralized control architecture for assigning pan-tilt-zoom (PTZ) cameras to targets so that the specification is met for any admissible behavior of the targets. Then, in order to alleviate the computational complexity associated with LTL synthesis and to enable implementation of local control protocols on individual PTZ cameras, we propose a distributed synthe- sis methodology. The main idea is to decompose the global specification into local specifications for each PTZ camera. A thorough design example is presented to illustrate the steps of the proposed procedure.trate the steps of the proposed procedure.)
Hot-swapping robot task goals in reactive formal synthesis + (We consider the problem of synthesizing ro … We consider the problem of synthesizing robot controllers to realize a task that unpredictably changes with time. Tasks are formally expressed in the GR(1) fragment of temporal logic, in which some of the variables are set by an adversary. The task changes by the addition or removal of goals, which occurs online (i.e., at run-time). We present an algorithm for mending control strategies to realize tasks after the addition of goals, while avoiding global re-synthesis of the strategy. Experiments are presented for a planar surveillance task in which new regions of interest are incrementally added. Run-times are empirically shown to be extremely favorable compared to re-synthesizing from scratch. We also present an algorithm for mending control strategies for the removal of goals. While in this setting the original strategy is still feasible (as we prove), our algorithm provides a more satisfying solution by âtightening loose ends.â Both algorithms are shown to yield so-called reach annotations, and thus the control strategies are easily amenable to other algorithms concerning incremental synthesis, e.g., as in previous work by the authors for robot navigation in uncertain environments.obot navigation in uncertain environments.)
Equilibrium Controllability for a Class of Mechanical Systems + (We define a notion of controllability for … We define a notion of controllability for mechanical systems which determinesthe configurations which are accessible from a given configuration. Wederive sufficient conditions for this notion of controllability in terms ofthe given inputs, their Lie brackets, and their covariant derivatives.brackets, and their covariant derivatives.)
Real Time Trajectory Generation for Differentially Flat Systems with Unstable Zero Dynamics + (We define the real time trajectory generat … We define the real time trajectory generation problem to be how to generate,possibly with some delay, a full state space and input trajectory in realtime from an output trajectory that is given online, while allowing atradeoff between stability and performance. Wepropose two algorithms that solve the real time trajectory generationproblem for flat systems with zero dynamics, and discuss some interestingproperties. We explicitly address the tradeoff between stability andperformance. The algorithms are validated in simulations and experimentswith a thrust vectored ducted fan aircraft.ith a thrust vectored ducted fan aircraft.)
A two-state ribosome and protein model can robustly capture the chemical reaction dynamics of gene expression + (We derive phenomenological models of gene … We derive phenomenological models of gene expression from a mechanistic description of chemical reactions using an automated model reduction method. Using this method, we get analytical descriptions and computational performance guarantees to compare the reduced dynamics with the full models. We develop a new two-state model with the dynamics of the available free ribosomes in the system and the protein concentration. We show that this new two-state model captures the detailed mass-action kinetics of the chemical reaction network under various biologically plausible conditions on model parameters. On comparing the performance of this model with the commonly used mRNA transcript-protein dynamical model for gene expression, we analytically show that the free ribosome and protein model has superior error and robustness performance.superior error and robustness performance.)
Discrete Function Approximation: Numerical Tools for Nonlinear Control + (We describe a method for discrete represen … We describe a method for discrete representation of continuous functions and show howthis may be used for typical computations in nonlinear control desi gn. The methodinvolves representing functions by their values and finitely many derivatives at discreteset of points on the domain. We propose a grid structure based on a hierarchy ofrectangular boxes that provides flexibility in placing grid points densely in some regionsand sparsely in the other. The grids possess enough structure to facilitate easyinterpolation schemes based on piecewise polynomials. We illustrate the method using asimple example where we compute the feedback linearizing output of a system.e feedback linearizing output of a system.)
Coarse analysis of multiscale systems: diffuser flows, charged particle motion, and connections to averaging theory + (We describe a technique for the efficient … We describe a technique for the efficient computation of the dominant-scale dynamics of a fluid system when only a high-fidelity simulation is available. Such a technique is desirable when governing equations for the dominant scales are unavailable, when model reduction is impractical, or when the original high-fidelity computation is expensive. We adopt the coarse analysis framework proposed by I. G. Kevrekidis (Comm. Math. Sci. 2003), where a computational superstructure is designed to use short-time, high-fidelity simulations to extract the dominant features for a multi- scale system. We apply this technique to compute the dominant features of the compressible flow through a planar diffuser. We apply the proper orthogonal decomposition to classify the dominant and subdominant scales of diffuser flows. We derive a suitable coarse pro jective Adams-Bashforth time integration routine and apply it to compute averaged diffuser flows. The results include accu- rate tracking of the dominant-scale dynamics for a range of parameter values for the computational superstructure. These results demonstrate that coarse analysis methods are useful for solving fluid flow problems of a multiscale nature. In order to elucidate the behavior of coarse analysis techniques, we make comparisons to averaging theory. To this end, we derive governing equations for the average motion of charged particles in a magnetic field in a number of different settings. First, we apply a novel procedure, inspired by WKB theory and Whitham averaging, to average the variational principle. The resulting equations are equivalent to the guiding center equations for charged particle motion; this marks an instance where averaging and variational principles commute. Secondly, we apply Lagrangian averaging techniques, previously applied in fluid mechanics, to derive averaged equations. Making comparisons to the WKB/Whitham-style derivation allows for the necessary closure of the Lagrangian averaging formulation. We also discuss the Hamiltonian setting and show that averaged Hamiltonian systems may be derivable using concepts from coarse analysis. Finally, we apply a prototypical coarse analysis procedure to the system of charged particles and generate tra jectories that resemble guiding center tra jectories. We make connections to perturbation theory to derive guidelines for the design of coarse analysis techniques and comment on the prototypical coarse analysis application.on the prototypical coarse analysis application.)
Lagrangian Mechanics and Carangiform Locomotion + (We describe the interaction of a rigid bod … We describe the interaction of a rigid body and its incompressible fluid environmentwith reduced Euler-Lagrange equations on the appropriate Cartesian product manifold. Wepropose a modification to the planar form of these equations to accomodate control inputsconsistent with a model for carangiform swimming. Initial Lie algebraic analysis of theresulting control system suggests its usefulness in predicting efficacious gaits forpiscimimetic robots.efficacious gaits for piscimimetic robots.)
Extremal Properties of Complex Networks + (We describe the structure of connected gra … We describe the structure of connected graphs with the minimum and maximum average distance, radius, diameter, betweenness centrality, efficiency and resistance distance, given their order and size. We find tight bounds on these graph qualities for any arbitrary number of nodes and edges and analytically derive the form and properties of such networks. the form and properties of such networks.)
Networks with the Smallest Average Distance and the Largest Average Clustering + (We describe the structure of the graphs wi … We describe the structure of the graphs with the smallest average distance and the largest average clustering given their order and size. There is usually a unique graph with the largest average clustering, which at the same time has the smallest possible average distance. In contrast, there are many graphs with the same minimum average distance, ignoring their average clustering. The form of these graphs is shown with analytical arguments. Finally, we measure the sensitivity to rewiring of this architecture with respect to the clustering coefficient, and we devise a method to make these networks more robust with respect to vertex removal.ore robust with respect to vertex removal.)
Synthesis of Distributed Longitudinal Control 1 Protocols for a Platoon of Autonomous Vehicles + (We develop a framework for control protoco … We develop a framework for control protocol syn- thesis for a platoon of autonomous vehicles subject to temporal logic specifications. We describe the desired behavior of the platoon in a set of linear temporal logic formulas, such as collision avoidance, close spacing or comfortability. The problem of decomposing a global specification for the platoon into distributed specification for each pair of adjacent vehicles is hard to solve. We use the invariant specifications to tackle this problem and the decomposition is proved to be scalable.. Based on the specifications in Assumption/Guarantee form, we can construct a two-player game (between the vehicle and its closest leader) locally to automatically synthesize a controller protocol for each vehicle. Simulation example for a distributed vehicles control problem is also shown.ed vehicles control problem is also shown.)
Optimal Control of Non-deterministic Systems for a Computationally Efficient Fragment of Temporal Logic + (We develop a framework for optimal control … We develop a framework for optimal control policy synthesis for non-deterministic transition systems subject to temporal logic specifications. We use a fragment of temporal logic to specify tasks such as safe navigation, response to the environment, persistence, and surveillance. By restricting specifications to this fragment, we avoid a potentially doubly-exponential automaton construction. We compute feasible con- trol policies for non-deterministic transition systems in time polynomial in the size of the system and specification. We also compute optimal control policies for average, minimax (bottleneck), and average cost-per-task-cycle cost functions. We highlight several interesting cases when these can be computed in time polynomial in the size of the system and specification. Additionally, we make connections between computing optimal control policies for an average cost-per-task-cycle cost function and the generalized traveling salesman problem. We give simulation results for motion planning problems.tion results for motion planning problems.)
Automaton-Guided Controller Synthesis for Nonlinear Systems with Temporal Logic + (We develop a method for the control of dis … We develop a method for the control of discrete-time nonlinear systemssubject to temporal logic specifications. Our approach uses a coarseabstraction of the system and an automaton representing the temporal logicspecification to guide the search for a feasible trajectory. This decomposesthe search for a feasible trajectory into a series of constrainedreachability problems. Thus, one can create controllers for any system forwhich techniques exist to compute (approximate) solutions to constrainedreachability problems. Representative techniques include sampling-basedmethods for motion planning, reachable set computations for linear systems,and graph search for finite discrete systems. Our approach avoids theexpensive computation of a discrete abstraction, and its implementation isamenable to parallel computing. We demonstrate our approach with numericalexperiments on temporal logic motion planning problems with high-dimensional(10+ states) continuous systems.mensional (10+ states) continuous systems.)
Addressable, “Packet-Based” Intercellular Communication through Plasmid Conjugation + (We develop a system for implementing “pack … We develop a system for implementing “packet-based” intercellular communication in an engineered bacterial population via conjugation. Our system uses gRNA-based identification markers that allow messages to be addressed to specific strains via Cas9-mediated cleavage of messages sent to the wrong recipient, which we show reduces plasmid transfer by four orders of magnitude. Integrase-mediated editing of the address on the message plasmid allows cells to dynamically update the message’s recipients in vivo. As a proof-of-concept demonstration of our system, we propose a linear path scheme that would propagate a message sequentially through the strains of a population in a defined order.trains of a population in a defined order.)
Classification of Human Motion into Dynamics Based Primitives with Application to Drawing Tasks + (We develop the study of primitives of huma … We develop the study of primitives of human motion, which we refer to as movemes. The idea is to understand human motion by decomposing it into a sequence of elementary building blocks that belong to a known alphabet of dynamical systems. Where do these dynamic primitives come from in practice? How can we construct an alphabet of movemes from human data? In this paper we address these issues. We define conditions under which collections of signals are well-posed according to a dynamical model class M and thus can generate movemes. Using examples from human drawing data, we show that the definition of well-posedness can be applied in practice so to establish if sets of actions, reviewed as signals in time, can define movemes.d as signals in time, can define movemes.)
Reasoning over Test Specifications using Assume-Guarantee Contracts + (We establish a framework to reason about t … We establish a framework to reason about test campaigns described formally. First, we introduce the notion of a test structure — an object that carries i) the formal specifications of the system under test, and ii) the test objective, which is specified by a test engineer. We build on test structures to define test campaigns and specifications for the tester. Secondly, we use the algebra of assume-guarantee contracts to reason about constructing tester specifications, comparing test struc- tures and test campaigns, and combining and splitting test structures. Using the composition operator, we characterize the conditions on the constituent tester specifications and test objectives for feasibly combin- ing test structures. We illustrate the different applications of the quotient operator to split the test objective, the system into subsystems, or both. Finally, we illustrate test executions corresponding to the combined and split test structures in a discrete autonomous driving example and an aircraft formation-flying example. We anticipate that reasoning over test specifications would aid in generating optimal test campaigns. aid in generating optimal test campaigns.)
Optimal LQG Control Across a Packet-Dropping Link + (We examine optimal Linear Quadratic Gaussi … We examine optimal Linear Quadratic Gaussian control for a system in which communication betweenthe sensor (output of the plant) and the controller occurs across a packet-dropping link. We extend thefamiliar LQG separation principle to this problem that allows us to solve this problem using a standardLQR state-feedback design, along with an optimal algorithm for propagating and using the informationacross the unreliable link. We present one such optimal algorithm, which consists of a Kalman Filter atthe sensor side of the link, and a switched linear filter at the controller side. Our design does not assumeany statistical model of the packet drop events, and is thus optimal for an arbitrary packet drop pattern.Further, the solution is appealing from a practical point of view because it can be implemented as asmall modification of an existing LQG control design.ication of an existing LQG control design.)
Optimal LQG control across packet-dropping links + (We examine two special cases of the problem of optimal linear quadratic Gaussian control of a system whose state is being measured by sensors that communicate with the controller over packet-dropping links. We pose the problem as an)
Protein degradation in a TX-TL cell-free expression system using ClpXP protease + (We explored the possibility of supplementi … We explored the possibility of supplementing an in vitro S30-based Escherichia coli expression system (or âTX-TLâ) with ClpXP, an AAA+ protease pair that selectively degrades tagged proteins, to provide finely-tuned degradation. The mechanism of ClpXP degradation has been extensively studied both in vitro and in vivo. However, it has not been characterized for use in synthetic circuits -- metrics such as toxicity, ATP usage, degradation variation over time, and cellular loading need to be determined. In particular, TX-TL in batch mode is known to be resource limited, and ClpXP is known to require significant amounts of ATP to unfold different protein targets. We find that ClpXPâs protein degradation dynamics is dependent on protein identity, but can be determined experimentally. Degradation follows Michaels- Menten kinetics, and can be fine tuned by ClpX or ClpP concentration. Added purified ClpX is also not toxic to TX-TL reactions. Therefore, ClpXP provides a controllable way to introduce protein degradation and dynamics into synthetic circuits in TX-TL.NOTE: This is a technical report for future inclusion in work pending submission, review, and publication. Therefore, this work has not been peer-reviewed and is presented as-is.s not been peer-reviewed and is presented as-is.)
Flight dynamics and control of evasive maneuvers: the fruit fly's takeoff + (We have approached the problem of reverse … We have approached the problem of reverse engineering the flight control mechanism of the fruit fly by studying the dynamics of the responses to a visual stimulus during takeoff. Building upon a prior framework we seek to understand the strategies employed by the animal to stabilize attitude and orientation during these evasive, highly dynamical maneuvers. As a first step, we consider the dynamics from a gray-box perspective: examining lumped forces produced by the insect's legs and wings. The reconstruction of the flight initiation dynamics, based on the unconstrained motion formulation for a rigid body, allows us to assess the fly's responses to a variety of initial conditions induced by its jump. Such assessment permits refinement by using a visual tracking algorithm to extract the kinematic envelope of the wings in order to estimate lift and drag forces, and recording actual leg-joint kinematics and using them to estimate jump forces. In this paper we present the details of our approach in a comprehensive manner including the salient results.sive manner including the salient results.)
Theoretical Design of Paradoxical Signaling-Based Synthetic Population Control Circuit in E. coli + (We have developed a mathematical framework … We have developed a mathematical framework to analyze the cooperative control of cell population homeostasis via paradoxical signaling in synthetic contexts. Paradoxical signaling functions through quorum sensing (where cells produce and release a chemical signal as a function of cell density). Precisely, the same quorum sensing signal provides both positive (proliferation) and negative (death) feedback in different signal concentration regimes. As a consequence, the relationship between intercellular quorum sensing signal concentration and net growth rate (cell proliferation minus death rates) can be non-monotonic. This relationship is a condition for robustness to certain cell mutational overgrowths and allows for increased stability in the presence of environmental perturbations. Here, we explore stability and robustness of a conceptualized synthetic circuit. Furthermore, we asses possible design principles that could exist among a subset of paradoxical circuit implementations. This analysis sparks the development a bio-molecular control theory to identify ideal underlying characteristics for paradoxical signaling control systems.for paradoxical signaling control systems.)
Appealing to a Non-traditional Audience: A New Approach to Teaching Feedback + (We have developed a new course as well as … We have developed a new course as well as an undergraduate minor inControl and Dynamical Systems for teaching design and analysis offeedback systems to students from diverse fields such as biology,computer science, and economics as well as all traditional engineering%disciplines. all traditional engineering %disciplines.)

(We have developed a new course as well as an undergraduate minor in Cont)

A MATLAB toolbox for modeling genetic circuits in cell-free systems + (We introduce a MATLAB-based simulation too … We introduce a MATLAB-based simulation toolbox, called txtlsim, for an Escherichia coli-based Transcription–Translation (TX–TL) system. This toolbox accounts for several cell-free-related phenomena, such as resource loading, consumption and degradation, and in doing so, models the dynamics of TX–TL reactions for the entire duration of solution phase batch-mode experiments. We use a Bayesian parameter inference approach to characterize the reaction rate parameters associated with the core transcription, translation and mRNA degradation mechanics of the toolbox, allowing it to reproduce constitutive mRNA and protein-expression trajectories. We demonstrate the use of this characterized toolbox in a circuit behavior prediction case study for an incoherent feed-forward loop.study for an incoherent feed-forward loop.)
Cooperative Control of Multi-Vehicle Systems using Cost Graphs and Optimization + (We introduce a class of triangulated graph … We introduce a class of triangulated graphs for algebraic representation of formations that allows us to specify a mission cost for a group of vehicles. This representation plus the navigational information allows us to formally specify and solve tracking problems for groups of vehicles in formations using an optimization-based approach. The approach is illustrated using a collection of six underactuated vehicles that track a desired trajectory in formation. ack a desired trajectory in formation. )
The Dynamic Sensor Coverage Problem + (We introduce a theoretical framework for t … We introduce a theoretical framework for the dynamic sensor coverageproblem for a simple case with multiple discrete time linear dynamical systemslocated in different spacial locations. The objective is to keep an appreciableestimate of the states of the systems at all times by deploying a few mobile sensors.The sensors are assumed to have a limited range and they implement a Kalmanfilter to estimate the states of all the systems. The motion of the sensor is modeledas a discrete time discrete state Markov chain. Based on some recent results onthe Kalman filtering problem with intermittent observations by Sinopoli et. al., wederive conditions under which a single sensor fails to solve the coverage problem.We also give conditions under which we can guarantee that a single sensor isenough to solve the dynamic coverage problem.ugh to solve the dynamic coverage problem.)
A Compositional Approach to Stochastic Optimal Control with Temporal Logic Specifications + (We introduce an algorithm for the optimal … We introduce an algorithm for the optimal con- trol of stochastic nonlinear systems subject to temporal logic constraints on their behavior. We directly compute on the state space of the system, avoiding the expensive pre-computation of a discrete abstraction. An automaton that corresponds to the temporal logic specification guides the computation of a control policy that maximizes the probability that the system satisfies the specification. This reduces controller synthesis to solving a sequence of stochastic constrained reachability problems. The solution to each reachability problem corresponds to the solution to a corresponding Hamilton-Jacobi-Bellman (HJB) partial differential equation. To increase the efficiency of our approach, we exploit a class of systems where the HJB equation is linear due to structural assumptions on the noise. The linearity of the PDE allows us to pre-compute control policy primitives and then compose them, at essentially zero cost, to satisfy a complex temporal logic specification.fy a complex temporal logic specification.)
A Compositional Approach to Stochastic Optimal Control with Co-safe Temporal Logic Specifications + (We introduce an algorithm for the optimal … We introduce an algorithm for the optimal control of stochastic nonlinear systems subject to temporal logic constraints on their behavior. We compute directly on the state space of the system, avoiding the expensive pre-computation of a discrete abstraction. An automaton that corresponds to the temporal logic specification guides the computation of a control policy that maximizes the probability that the system satisfies the specification. This reduces controller synthesis to solving a sequence of stochastic constrained reachability problems. Each individual reachability problem is solved via the Hamilton-Jacobi-Bellman (HJB) partial differential equation of stochastic optimal control theory. To increase the efficiency of our approach, we exploit a class of systems where the HJB equation is linear due to structural assumptions on the noise. The linearity of the partial differential equation allows us to pre-compute control policy primitives and then compose them, at essentially zero cost, to conservatively satisfy a complex temporal logic specification.fy a complex temporal logic specification.)
Dynamical Models for Control of Cavity Oscillations + (We investigate nonlinear dynamical models … We investigate nonlinear dynamical models for self- sustainedoscillations in the flow past a rectangular cavity. The models arebased on the method of Proper Orthogonal Decomposition (POD) andGalerkin projection, and we introduce an inner product and formulationof the equations of motion which enables one to use vector-valued PODmodes for compressible flows. We obtain models between 3 and 20states, which accurately describe both the short-time and long-timedynamics. This is a substantial improvement over previous modelsbased on scalar-valued POD modes,which capture the dynamics for shorttime, but deviate for long time.for short time, but deviate for long time.)
Model Reduction Tools For Phenomenological Modeling of Input-Controlled Biological Circuits + (We present a Python-based software package … We present a Python-based software package to automatically obtain phenomenological models of input-controlled synthetic biological circuits that guide the design using chemical reaction-level descriptive models. From the parts and mechanism description of a synthetic biological circuit, it is easy to obtain a chemical reaction model of the circuit under the assumptions of mass-action kinetics using various existing tools. However, using these models to guide design decisions during an experiment is difficult due to a large number of reaction rate parameters and species in the model. Hence, phenomenological models are often developed that describe the effective relationships among the circuit inputs, outputs, and only the key states and parameters. In this paper, we present an algorithm to obtain these phenomenological models in an automated manner using a Python package for circuits with inputs that control the desired outputs. This model reduction approach combines the common assumptions of time-scale separation, conservation laws, and species’ abundance to obtain the reduced models that can be used for design of synthetic biological circuits. We consider an example of a simple gene expression circuit and another example of a layered genetic feedback control circuit to demonstrate the use of the model reduction procedure. the use of the model reduction procedure.)
Reactive Synthesis from Signal Temporal Logic Specifications + (We present a counterexample-guided inducti … We present a counterexample-guided inductive synthesis approach to controller synthesis for cyber-physical systems subject to signal temporal logic (STL) specifications, operating in potentially adversarial nondeterministic environments. We encode STL specifications as mixed integer-linear constraints on the variables of a discrete-time model of the system and environment dynamics, and solve a series of optimization problems to yield a satisfying control sequence. We demonstrate how the scheme can be used in a receding horizon fashion to fulfill properties over unbounded horizons, and present experimental results for reactive controller synthesis for case studies in building climate control and autonomous driving.ng climate control and autonomous driving.)
Biomolecular resource utilization in elementary cell-free gene circuits + (We present a detailed dynamical model of t … We present a detailed dynamical model of the behavior oftranscription-translation circuits in vitro that makes explicit the rolesplayed by essential molecular resources. A set of simple two-gene testcircuits operating in a cell-free biochemical âbreadboardâ validate thismodel and highlight the consequences of limited resource availability. Inparticular, we are able to confirm the existence of biomolecular âcrosstalkâand isolate its individual sources. The implications of crosstalk forbiomolecular circuit design and function are discussed.circuit design and function are discussed.)
Model Reduction for Compressible Flows using POD and Galerkin Projection + (We present a framework for applying the me … We present a framework for applying the method of Proper Orthogonal Decomposition(POD) and Galerkin projection to compressible fluids. For incompressible flows,only the kinematic variables are important, and the techniques are well known. Ina compressible flow, both the kinematic and thermodynamic variables are dynamicallyimportant, and must be included in the configuration space. We introducean energy-based inner product which may be used to obtain POD modes for thisconfiguration space. We then obtain an approximate version of the Navier-Stokesequations, valid for cold flows at moderate Mach number, and project these equationsonto a POD basis. The resulting equations of motion are quadratic, and aremuch simpler than projections of the full compressible Navier-Stokes equations.full compressible Navier-Stokes equations.)
Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems + (We present a framework for merging unit te … We present a framework for merging unit tests for autonomous systems. Typically, it is intractable to test an autonomous system for every scenario in its operating environment. The question of whether it is possible to design a single test for multiple requirements of the system motivates this work. First, we formally define three attributes of a test: a test specification that characterizes behaviors observed in a test execution, a test environment, and a test policy. Using the merge operator from contract-based design theory, we provide a formalism to construct a merged test specification from two unit test specifications. Temporal constraints on the merged test specification guarantee that non-trivial satisfaction of both unit test specifications is necessary for a successful merged test execution. We assume that the test environment remains the same across the unit tests and the merged test. Given a test specification and a test environment, we synthesize a test policy filter using a receding horizon approach, and use the test policy filter to guide a search procedure (e.g. Monte-Carlo Tree Search) to find a test policy that is guaranteed to satisfy the test specification. This search procedure finds a test policy that maximizes a pre-defined robustness metric for the test while the filter guarantees a test policy for satisfying the test specification. We prove that our algorithm is sound. Furthermore, the receding horizon approach to synthesizing the filter ensures that our algorithm is scalable. Finally, we show that merging unit tests is impactful for designing efficient test campaigns to achieve similar levels of coverage in fewer test executions. We illustrate our framework on two self-driving examples in a discrete-state setting.ving examples in a discrete-state setting.)
Characterization of Integrase and Excisionase Activity in Cell-free Protein Expression System Using a Modeling and Analysis Pipeline + (We present a full-stack modeling, analysis … We present a full-stack modeling, analysis, and parameter identification pipeline to guide the modeling and design of biological systems starting from specifications to circuit implementations and parameterizations. We demonstrate this pipeline by characterizing the integrase and excisionase activity in cell-free protein expression system. We build on existing Python tools — BioCRNpyler, AutoReduce, and Bioscrape — to create this pipeline. For enzyme-mediated DNA recombination in cell-free system, we create detailed chemical reaction network models from simple high-level descriptions of the biological circuits and their context using BioCRNpyler. We use Bioscrape to show that the output of the detailed model is sensitive to many parameters. However, parameter identification is infeasible for this high-dimensional model, hence, we use AutoReduce to automatically obtain reduced models that have fewer parameters. This results in a hierarchy of reduced models under different assumptions to finally arrive at a minimal ODE model for each circuit. Then, we run sensitivity analysis-guided Bayesian inference using Bioscrape for each circuit to identify the model parameters. This process allows us to quantify integrase and excisionase activity in cell extracts enabling complex-circuit designs that depend on accurate control over protein expression levels through DNA recombination. The automated pipeline presented in this paper opens up a new approach to complex circuit design, modeling, reduction, and parameterization.modeling, reduction, and parameterization.)
Tracking for Fully Actuated Mechanical Systems: A Geometric Framework + (We present a general framework for the con … We present a general framework for the control of Lagrangian systems with as manyinputs as degrees of freedom. Relying on the geometry of mechanical systems on manifolds,we propose a design algorithm for the tracking problem. The notion of error function andtransport map lead to a proper definition of configuration and velocity error. These arethe crucial ingredients in designing a proportional derivative feedback and feedforwardcontroller. The proposed approach includes as special cases a variety of results oncontrol of manipulators, pointing devices and autonomous vehicles. Our design providesparticular insight into both aerospace and underwater applications where the configurationmanifold is a Lie group.the configuration manifold is a Lie group.)
Optimal Control of Nonlinear Systems with Temporal Logic Specifications + (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.)
Model Predictive Control for Signal Temporal Logic Specifications + (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.)
Model Predictive Control with Signal Temporal Logic Specifications + (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.)
Optimization-based Control of Nonlinear Systems with Linear Temporal Logic Specifications + (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.)
Analysis of Dynamics in Escaping Flight Initiation in Drosophila + (We present a mathematical reconstruction … We present a mathematical reconstruction 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.,)
Robust Control of Uncertain Markov Decision Processes with Temporal Logic Specifications + (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.)
Patching task-level robot controllers based on a local Î¼-calculus formula + (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.)
Receding Horizon Temporal Logic Planning + (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 .)
Control Primitives for Robot Systems + (We present a set of primitive operations w … We present a set of primitive operations which forms the core of a robot systemdescription and control language. The actions of the individual primitives are derivedfrom the mathematical structure of the equations of motion for constrained mechanicalsystems. The recursive nature of the primitives allows composite robots to be constructedfrom more elementary daughter robots. We review a few pertinent results of classicalmechanics, describe the functionality of our primitive operations, and present severaldifferent hierarchical strategies for the description and control of a two-fingered handholding a box.trol of a two-fingered hand holding a box.)
Robust Connectivity of Networked Vehicles + (We present a simple geometric analysis of … We present a simple geometric analysis of wirelessconnectivity in vehicle networks. We introduce a localizednotion of connectedness, and construct a function that measuresthe robustness of this local connectedness to variationsin position. Under a mild feasibility hypothesis, this functionprovides a sufficient condition for global connectedness ofthe network. Further, it is distributed, in the sense thatboth the function and its gradients can be calculated usingonly neighbor-to-neighbor communications. It can thus formthe basis for distributed motion-control algorithms whichrespect connectivity constraints. We conclude with two simpleexamples of target applications.wo simple examples of target applications.)
Synthesis of Reactive Protocols for Vehicle-to-Vehicle Communication + (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.)
Contracts of Reactivity + (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.)

Search by property

List of results

Navigation menu

Page actions

Page actions

Personal tools

Navigation

Search

Tools