Property:Abstract
From Murray Wiki
Jump to navigationJump to search
This is a property of type Text.
A
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. +
M
We propose a model for planar carangiform swimming based on conservative equations for
the interaction of a rigid body and an incompressible fluid. We account for the generation
of thrust due to vortex shedding through controlled coupling terms. We investigate the
correct form of this coupling experimentally with a robotic propulsor, comparing its
observed behavior with that predicted by unsteady hydrodynamics. Our analysis of thrust
generation by an oscillating hydrofoil allows us to characterize and evaluate certain
families of gaits. Our final swimming model takes the form of a control-affine nonlinear
system. +
N
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. +
L
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. +
M
We propose a planar model for the swimming
of certain marine animals based on
reduced Euler-Lagrange equations for the interaction of a rigid body and
an incompressible fluid.
This model assumes the form of a control-affine nonlinear system with drift;
preliminary accessibility analysis suggests its utility in predicting
efficacious gaits for piscimimetic robots.
We account for the generation of thrust due to
vortex shedding through controlled coupling terms. At the
heart of this coupling is an abstraction from hydrofoil theory;
we investigate its applicability to real
swimming using an articulated robotic caudal fin. We compare the
observed behavior of our experimental apparatus to that predicted
numerically by steady hydrodynamic theory. +
S
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. +
B
Barrier-Based Test Synthesis for Safety-Critical Systems Subject to Timed Reach-Avoid Specifications +
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. +
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. +
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. +
F
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. +
T
We regard the internal configuration of a deformable body, together with
its position and orientation in ambient space, as a point in a trivial
principal fiber bundle over the manifold of body deformations.
In the presence of a symmetry which leads to a conservation law, the
self-propulsion of such a body due to cyclic changes in shape is
described by the corresponding mechanical connection on the configuration
bundle. In the presence of viscous drag sufficient to negate inertial
effects, the viscous connection takes the place of the mechanical connection.
Both connections may be represented locally in terms of the variables
describing the body's shape. In the presence of both inertial and
viscous effects, the equations of motion may be written in terms of the
two local connection forms as an affine control system with drift on
the manifold of configurations and body momenta. We apply techniques
from nonlinear control theory to the equations in this form to obtain
criteria for a particular form of accessibility. +
D
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. +
O
We study a simple pursuit scenario in which the
pursuer has potential access to an additional off-board global
sensor. However, the global sensor can be used for either of
two purposes: to improve the state estimate of the pursuer, or
to obtain more data about the trajectory being tracked. The
problem is to determine the variation in the performance of
the system as the global sensor changes its behavior. We use a
stochastic strategy to optimize over the transmission pattern
of the global sensor. +
S
Synthesizing Reactive Test Environments for Autonomous Systems: Testing Reach-Avoid Specifications with Multi-Commodity Flows +
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. +
U
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.
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
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
performance bounds are derived and simulations provided to illustrate the effectiveness of the scheme. +
A
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. +
D
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. +
J
We study the dynamics of the relative motion of
satellites in the gravitational field of the Earth, including
the effects of the bulge of the Earth (the $J_2$ effect). Using
Routh reduction and dynamical systems ideas, a method is found
that locates orbits such that the cluster of satellites remains
close with very little dispersing, even with no controls. The use of
controls in the context of this natural dynamics is studied to maintain and
achieve precision formations. +
O
We study the effect of quantization on the performance
of a scalar dynamical system. We provide an expression
for calculation of the LQR cost of a dynamical system for
a general quantizer. Using the high-rate approximation, we
evaluate it for two commonly used quantizers: uniform and
logarithmic. We also provide a lower bound on performance
of the optimal quantizer based on entropy arguments and
consider the case when the channel drops data packets
stochastically. +
We study the problem of using a small number
of mobile sensors to monitor various threats in a geographical
area. Using some recent results on stochastic sensor scheduling,
we propose a stochastic sensor movement strategy. We present
simple conditions under which it is not possible to maintain a
bounded estimate error covariance for all the threats. We also
study a simple sub-optimal algorithm to generate stochastic
trajectories. Simulations are presented to illustrate the results. +
