Recursos de colección

Caltech Authors (147.820 recursos)

Repository of works by Caltech published authors.

Group = Control and Dynamical Systems Technical Reports

Mostrando recursos 1 - 20 de 169

  1. Formalizing synthesis in TLA+

    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...

  2. Symbolic construction of GR(1) contracts for systems with full information

    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...

  3. Simultaneous Model Identification and Task Satisfaction in the Presence of Temporal Logic Constraints

    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...

  4. Interfacing TuLiP with the JPL Statechart Autocoder: Initial progress toward synthesis of flight software from formal specifications

    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...

  5. Time-annotated game graphs for synthesis from abstracted systems

    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...

  6. Revisiting the AMBA AHB bus case study

    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...

  7. Cross-entropy Temporal Logic Motion Planning

    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...

  8. Online Horizon Selection in Receding Horizon Temporal Logic Planning

    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...

  9. Synthesis from multi-paradigm specifications

    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,...

  10. Hot-swapping robot task goals in reactive formal synthesis

    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...

  11. Evaluation and Benchmarking for Robot Motion Planning Problems Using TuLiP

    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...

  12. Optimal Control of Mixed Logical Dynamical Systems with Long-Term Temporal Logic Specifications

    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...

  13. Discriminating external and internal causes for heading changes in freely flying Drosophila

    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...

  14. Motion planning in observations space with learned diffeomorphism models

    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...

  15. Convex optimal uncertainty quantification: Algorithms and a case study in energy storage placement for power grids

    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...

  16. Patching task-level robot controllers based on a local µ-calculus formula

    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.

  17. Swing Dynamics as Primal-Dual Algorithm for Optimal Load Control

    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...

  18. Stochastic Distributed Protocol for Electric Vehicle Charging with Discrete Charging Rate

    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...

  19. Fast Load Control with Stochastic Frequency Measurement

    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...

  20. Optimal Decentralized Protocols for Electric Vehicle Charging

    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...

Aviso de cookies: Usamos cookies propias y de terceros para mejorar nuestros servicios, para análisis estadístico y para mostrarle publicidad. Si continua navegando consideramos que acepta su uso en los términos establecidos en la Política de cookies.