Recursos de colección
Caltech Authors (147.820 recursos)
Repository of works by Caltech published authors.
Group = Control and Dynamical Systems Technical Reports
Repository of works by Caltech published authors.
Group = Control and Dynamical Systems Technical Reports
Filippidis, Ioannis; Murray, Richard M.
This report proposes a TLA+ definition for the problem of constructing a strategy that implements a temporal property. It is based on a note by Lamport [1] that outlines a formalization of realizability in TLA. The modified definition proposed here is expressed axiomatically in TLA+. Specifying what function is acceptable as a strategy requires care, so that a function with empty domain be avoided, while ensuring that the strategy will not need to have a domain too large to be a set.
We prove that initial conditions should appear in assumptions only, unless an initial predicate is added to the...
Filippidis, Ioannis; Murray, Richard M.
This work proposes a symbolic algorithm for the construction of assume-guarantee specifications that allow multiple agents to cooperate. Each agent is assigned goals expressed in a fragment of linear temporal logic known as generalized Streett with one pair, GR(1). These goals may be unrealizable, unless each agent makes additional assumptions, about the behavior of other agents. The algorithm constructs a contract among the agents, in that only the infinite behavior of the given goals is constrained, known as liveness, not the finite one, known as safety. This defers synthesis to a later stage of refinement, modularizing the design process. We...
Chinchali, Sandeep; Livingston, Scott C.; Pavone, Marco; Burdick, Joel W.
Recent proliferation of cyber-physical systems, ranging from autonomous cars to nuclear hazard inspection robots, has exposed several challenging research problems on automated fault detection and recovery. This paper considers how recently developed formal synthesis and model verification techniques may be used to automatically generate information-seeking trajectories for anomaly detection. In particular, we consider the problem of how a robot could select its actions so as to maximally disambiguate between different model hypotheses that govern the environment it operates in or its interaction with other agents whose prime motivation is a priori unknown. The identification problem is posed as selection of...
Dathathri, Sumanth; Livingston, Scott C.; Reder, Leonard J.; Murray, Richard M.
This paper describes the implementation of an interface connecting the two tools : the JPL SCA (Statechart Autocoder) and TuLiP (Temporal Logic Planning Toolbox) to enable the automatic synthesis of low level implementation code directly from formal specifications. With system dynamics, bounds on uncertainty and formal specifications as inputs, TuLiP synthesizes Mealy machines that are correct-by-construction. An interface is built that automatically translates these Mealy machines into UML statecharts. The SCA accepts the UML statecharts (as XML files) to synthesize flight-certified implementation code. The functionality of the interface is demonstrated through three example systems of varying complexity a) a simple...
Livingston, Scott C.
The construction of discrete abstractions is a crucial part of many methods for control synthesis of hybrid systems subject to formal specifications. In general, the product of discrete abstractions may not be a discrete abstraction for the product of the underlying continuously-valued systems. Addressing this, we present a control synthesis method for transition systems that are built from components with uncertain timing characteristics. The new device, called here time-annotated game graphs, is demonstrated in a variety of examples. While it is applicable generally to parity games, we consider it in the context of control subject to GR(1) specifications. We show...
Filippidis, Ioannis; Murray, Richard M.
This report describes a number of changes to the ARM AMBA bus case study from Bloem et al. that lead to significant reduction in synthesis time. In addition, it identifies the reason of blowup for the synthesized strategies in earlier studies as lack of binary decision diagram (BDD) reordering during strategy construction. Enabling dynamic BDD reordering with the group sifting algorithm, we synthesized strategies for as many as 18 masters, with both the original and revised specifications. This conclusion is based on detailed experimental measurements that show the changes of BDD sizes over time for the fixpoint and other variables...
Livingston, Scott C.; Wolff, Eric M.; Murray, Richard M.
This paper presents a method for optimal trajectory generation for discrete-time nonlinear systems with linear temporal logic (LTL) task specifications. Our approach is based on recent advances in stochastic optimization algorithms for optimal trajectory generation. These methods rely on estimation of the rare event of sampling optimal trajectories, which is achieved by incrementally improving a sampling distribution so as to minimize the cross-entropy. A key component of these stochastic optimization algorithms is determining whether or not a trajectory is collision-free. We generalize this collision checking to efficiently verify whether or not a trajectory satisfies a LTL formula. Interestingly, this verification...
Raman, Vasumathi; Fält, Mattias; Wongpiromsarn, Tichakorn; Murray, Richard M.
Temporal logics have proven effective for correct-by-construction synthesis of controllers for a wide range of applications. Receding horizon frameworks mitigate the computational intractability of reactive synthesis for temporal logic, but have thus far been limited by pursuing a single sequence of short horizon problems to the current goal. We propose a receding horizon algorithm for reactive synthesis that automatically determines a path to the currently pursued goal at runtime, in response to a nondeterministic environment. This is achieved by allowing each short horizon to have multiple local goals, and determining which local goal to pursue based on the current global...
Filippidis, Ioannis; Murray, Richard M.; Holzmann, Gerard J.
This work proposes a language for describing reactive synthesis problems that integrates imperative and declarative elements. The semantics is defined in terms of two-player turn-based infinite games with full information. Currently, synthesis tools accept linear temporal logic (LTL) as input, but this description is less structured and does not facilitate the expression of sequential constraints. This motivates the use of a structured programming language to specify synthesis problems. Transition systems and guarded commands serve as imperative constructs, expressed in a syntax based on that of the modeling language Promela. The syntax allows defining which player controls data and control flow,...
Livingston, Scott C.; Murray, Richard M.
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 favorable compared to re-synthesizing...
Spooner, Nicholas
Model checking is a technique commonly used in the verification of software and hardware. More recently, similar techniques have been employed to synthesize software that is correct by construction. TuLiP is a toolkit which interfaces with game solvers and model checkers to achieve this, producing a finite-state automaton representing a controller that satisfies the supplied specification. For motion planning in particular, a model checker may be employed in a deterministic scenario to produce a path satisfying a specification φ by checking against its negation ¬φ. If a counterexample is found, it will be a trace which satisfies φ. This was...
Wolff, Eric M.; Murray, Richard M.
We present a mathematical programming-based method for control of large a class of nonlinear systems subject to temporal logic task specifications. We consider Mixed Logical Dynamical (MLD) systems, which include linear hybrid automata, constrained linear systems, and piecewise affine systems. 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 walking, repeated assembly, and environmental monitoring. Our method directly encodes an LTL formula as mixed-integer linear constraints on the MLD system, instead of computing a finite abstraction. This approach is efficient; for common...
Censi, Andrea; Straw, Andrew D.; Sayaman, Rosalyn; Murray, Richard M.; Dickinson, Michael H.
As animals move through the world in search of resources, they change course in reaction to both external sensory cues and internally-generated programs. Elucidating the functional logic of complex search algorithms is challenging because the observable actions of the animal cannot be unambiguously assigned to externally- or internally-triggered events. We present a technique that addresses this challenge by assessing quantitatively the contribution of external stimuli and internal processes. We apply this technique to the analysis of rapid turns (“saccades”) of freely flying Drosophila melanogaster. We show that a single scalar feature computed from the visual stimulus experienced by the animal...
Censi, Andrea; Nilsson, Adam; Murray, Richard M.
We consider the problem of planning motions in observations
space, based on learned models of the dynamics that
associate to each action a diffeomorphism of the
observations domain. For an arbitrary set of
diffeomorphisms, this problem must be formulated as a
generic search problem. We adapt established algorithms of
the graph search family. In this scenario, node expansion
is very costly, as each node in the graph is associated to
an uncertain diffeomorphism and corresponding predicted
observations. We describe several improvements that
ameliorate performance: the introduction of better image
similarities to use as heuristics; a method to reduce the
number...
Han, Shuo; Topcu, Ufuk; Tao, Molei; Owhadi, Houman; Murray, Richard M.
How does one evaluate the performance of a stochastic system in the absence of a perfect model (i.e. probability distribution)? We address this question under the framework of optimal uncertainty quantification (OUQ), which is an information-based approach for worst-case analysis of stochastic systems. We are able to generalize previous results and show that the OUQ problem can be solved using convex optimization when the function under evaluation can be expressed in a polytopic canonical form (PCF). We also propose iterative methods for scaling the convex formulation to larger systems. As an application, we study the problem of storage placement in...
Livingston, Scott C.; Prabhakar, Pavithra; Jose, Alex B.; Murray, Richard M.
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.
Zhao, Changhong; Topcu, Ufuk; Low, Steven H.
Frequency regulation and generation-load balancing are key issues in power transmission networks. Complementary to generation control, loads provide flexible and fast responsive sources for frequency regulation, and local frequency measurement capability of loads offers the opportunity of decentralized control. In this paper, we propose an optimal load control problem, which balances the load reduction (or increase) with the generation shortfall (or surplus), resynchronizes the bus frequencies, and minimizes a measure of aggregate disutility of participation in such a load control. We find that, a frequency-based load control coupled with the dynamics of swing equations and branch power flows serve as...
Gan, Lingwen; Topcu, Ufuk; Low, Steven H.
To address the grid-side challenges associated with the anticipated high electric vehicle (EV) penetration level, various charging protocols have been proposed in the literature. Most if not all of these protocols assume continuous charging rates and allow intermittent charging. However, due to charging technology limitations, EVs can only be charged at a fixed rate, and the intermittency in charging shortens the battery lifespan. We consider these charging requirements, and formulate EV charging scheduling as a discrete optimization problem.
We propose a stochastic distributed algorithm to approximately
solve the optimal EV charging scheduling problem in an
iterative procedure. In each iteration, the transformer receives
charging...
Zhao, Changhong; Topcu, Ufuk; Low, Steven H.
Matching demand with supply and regulating frequency
are key issues in power system operations. Flexibility
and local frequency measurement capability of loads offer new regulation mechanisms through load control. We present a
frequency-based fast load control scheme which aims to match
total demand with supply while minimizing the global end-use
disutility. Local frequency measurement enables loads to make decentralized decisions on their power from the estimates of total demand-supply mismatch. To resolve the errors in such estimates caused by stochastic frequency measurement errors, loads communicate via a neighborhood area network. Case studies show that the proposed load control can balance demand with supply and restore...
Gan, Lingwen; Topcu, Ufuk; Low, Steven
We propose decentralized algorithms for optimally scheduling electric vehicle charging. The algorithms exploit the elasticity and controllability of electric vehicle related loads in order to fill the valleys in electric demand profile. We formulate a global optimization problem whose objective is to impose a generalized notion of valley-filling, study properties of the optimal charging profiles, and give decentralized offline and online algorithms to solve the problem. In each iteration of the proposed algorithms, electric vehicles choose their own charging profiles for the rest horizon according to the price profile broadcast by the utility, and the utility updates the price profile...