Gerardo Lafferriere

Graph Theoretic Methods in the Stability of Vehicle Formations \|/ PDF\|/
Authors:  Gerardo Lafferriere, John Caughman,  Anca Williams
Publication data:  Proc. ACC 2004, pages 3729--3724, July 2004
Abstract:
This paper investigates the stabilization of vehicle formations using techniques from algebraic graph theory. The vehicles exchange information according to a pre-specified (undirected) communication graph, G. The feedback control is based only on relative information about vehicle states shared via the communication links. We prove that a linear stabilizing feedback always exists provided that G is connected. Moreover, we show how the rate of convergence to formation is governed by the size of the smallest positive eigenvalue of the Laplacian of G. Several numerical simulations are used to illustrate the results.

Symbolic Reachability Computation for Families of Linear Vector Fields   \|/ PDF\|/
Authors: Gerardo Lafferriere, George J. Pappas, Sergio Yovine
Publication data: J. Symbolic Computation,  v32, pp 231-253, 2001.
Abstract:
The control paradigm of physical processes being supervised by digital programs has lead to the development of a theory of hybrid systems combining finite state automata with differential equations.  One of the most important problems in the verification of hybrid systems is the reachability problem.  Even though the computation of reachable spaces for finite state machines is well developed, computing the reachable space of a differential equation is difficult.  In this paper, we present the first known families of linear differential equations with a decidable reachability problem.  This is achieved by posing the reachability computation as a quantifier elimination problem in the decidable theory of the reals.  We illustrate the applicability of our approach by performing computations using the packages \textsc{Redlog} and \textsc{Qepcad}.  Such symbolic computations can be incorporated in computer-aided verification tools for purely discrete systems, resulting  in verification tools for hybrid systems with linear differential equations.

O-minimal Hybrid Systems   \|/ ZIP \|/ PDF\|/
Authors: Gerardo Lafferriere, George J. Pappas, Shankar Sastry
Publication data: Mathematics of Control, Signals, and Systems, v13, pp 1-21, 2000.
Abstract:
An important approach to decidability questions for verification algorithms of hybrid systems has been the construction of a bisimulation.  Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original infinite state hybrid system.  In this paper, we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and flows are definable in an o-minimal theory.  We prove that o-minimal hybrid systems always admit finite bisimulations.  We then present specific examples of hybrid systems with complex continuous dynamics for which finite bisimulations exist.

Hierarchically Consistent Control Systems    \|/ ZIP\|/ PDF\|/
Authors: George J. Pappas, Gerardo Lafferriere, Shankar Sastry
Publication data:  IEEE Transactions on Automatic Control, Vol 45, No 6, pp 1144-1160 June 2000.
Abstract:
Large scale control systems typically possess a hierarchical architecture in order to manage complexity.  Higher levels of the hierarchy utilize coarser models of the system resulting by aggregating the detailed lower level models. In this layered control paradigm, the notion of hierarchical consistency is important as it ensures the implementation of high level objectives  by the lower level system.  In this paper, we define a notion of modeling hierarchy for continuous control systems and obtain characterizations for hierarchically consistent linear systems with respect to controllability objectives.  As an interesting byproduct, we obtain a hierarchical controllability criterion for linear systems from which we recover the best of the known controllability algorithms from numerical linear algebra.

A New Class of Decidable Hybrid Systems    \|/ ZIP\|/ PDF\|/
Authors: Gerardo Lafferriere, George J. Pappas, Sergio Yovine
Publication data:  Lecture Notes in Computer Science vol. 1569,  pp 137-151, 1999.
Abstract:
One of the most important analysis problems of hybrid systems is the reachability problem.  State of the art computational tools perform reachability computation for timed automata, multirate automata, and rectangular automata. In this paper, we extend the decidability frontier for classes of  linear hybrid systems, which are introduced as hybrid systems with linear vector fields in each discrete location.    This result is achieved by showing that any such hybrid system admits a finite bisimulation, and by providing an algorithm that computes it using decision methods from mathematical logic.

Reachability Computation of Linear Hybrid Systems   \|/ ZIP\|/ PDF\|/
Coauthor(s): George J. Pappas, Sergio Yovine
Publication data: Proceedings of the 14th IFAC World Congress, Vol E, pp 7-12, Beijing, PRC, July 1999.
Abstract:
Linear hybrid systems are finite state machines with linear vector fields of the form $\dot{x}=Ax$ in each discrete location.  Very recently, the reachability problem for classes of linear hybrid systems was shown to be decidable. In this paper, the decidability result is extended to capture classes of linear hybrid systems where in each location the dynamics are of the form =Ax+Bu, for various types of inputs.

Hybrid Systems with Finite Bisimulations    \|/ ZIP\|/ PDF\|/
Coauthor(s): George J. Pappas, Shankar Sastry
Publication data:  Lecture Notes in Computer Science, vol. 1567, pp 186-203, 1999.
Abstract:
The theory of formal verification is one of the main approaches to hybrid system analysis. Decidability questions for verification algorithms are obtained by constructing finite, reachability preserving quotient systems called bisimulations. In this paper, we use recent results from stratification theory, subanalytic sets, and model theory in order to extend the state­of­the­art results on the existence of bisimulations for certain classes of planar hybrid systems.

Subanalytic Stratifications and Bisimulations    \|/ ZIP\|/ PDF\|/
Coauthor(s): George J. Pappas, Shankar Sastry
Publication data:  Lecture Notes in Computer Science, vol. 1386, pp 205-220, 1998.
Abstract:
Decidability results for the verification of hybrid systems consist of constructing special finite state quotients called bisimulations whose properties are equivalent to those of the original infinite state system. This approach has had success in the case of timed automata and linear hybrid automata. In this paper, the powerful frameworks of stratification theory and subanalytic sets are presented and used in order to obtain bisimulations of certain analytic vector fields on analytic manifolds.

A Computational Method for Simulation of Trunk Motion: Towards a Theoretical based Quantitative Assessment of Trunk Performance     \|/ ZIP\|/ PDF\|/
Coauthor(s): M. Parnianpour, J. L. Wang, A. Shirazi-Adl, B. Khayatian,
Publication data:   Biomedical Engineering, Application, Basis, and Communication, 1999, to appear.  (A shorter version appeared in PD. vol 77, Engineering Systems Design and Analysis, vol 5, ASME,  pp 69-76, 1996.)
Abstract:
Quantitative assessment of trunk muscle performance is important in documenting the extent of impairment and disability due to low back disorders (LBD). The statistical pattern recognition problem of classifying LBD patients and normal subjects based on dynamic trunk performance has been data driven. To provide clinical insight for interpretation of the distinctive features in the movement profiles, we have suggested an optimization-based approach for simulation of dynamic point-to-point sagittal trunk movement. The effect of strength impairment on movement patterns was simulated based on minimizing different physical cost functions: Energy, Jerk, Peak Torque, Impulse, and Work. During unconstrained simulations, uni-modal velocity patterns are predicted, while time to peak velocity is distinct for each cost function. The significant differences between unimpaired optimal movement profiles were diminished by imposing an 80% reduction in extensor muscle strength. The results indicate that the search for finding the objective function being used by central nervous system is an ill-posed problem since we are never sure if we have included all the active constraints in the simulation. The four application areas of this study are: 1) providing optimized trajectories for bio-feedback to patients during the rehabilitation process; 2) training workers to lift safely; 3) estimating the task demand based on the global description of the job; and 4) aiding the engineering evaluation to develop ergonomic and workplace interventions which needed to accommodate individuals with prior disability.

Discontinuous Stabilizing Feedback Using Partially Defined Lyapunov Functions       \|/ ZIP\|/ PDF\|/
Publication data:  Proceedings of the 33rd CDC, pp 3487-3491, Orlando, Florida, 1994.
Abstract:
We generalize earlier results on the construction of discontinuous feedback laws from smooth but partially defined control Lyapunov functions.  The resulting feedback law is continuous at the origin and smooth except on a hypersurface of codimension 1. We provide a formula for the feedback law which is in a sense ``universal.''  The new results presented cover situations where trajectories of the closed loop system switch an infinite number of times between regions where smooth control Lyapunov functions exist. The conditions on the system vector fields can be verified without solving the differential equations and are therefore in the spirit of the ``direct'' methods of Lyapunov. Using a recently developed formula we are also able to guarantee certain bounds on the feedback controls provided that the Lyapunov property can be satisfied using controls values in the unit ball.

Remarks on Control Lyapunov Functions for Discontinuous Stabilizing Feedback       \|/ ZIP\|/ PDF\|/
Coauthor(s): Eduardo Sontag
Publication data:  Proceedings of the 32rd CDC, pp 306-308, San Antonio, Texas, 1993.
Abstract:
We present a formula for a stabilizing feedback law under the assumption that a piecewise smooth control­Lyapunov function exists. The resulting feedback is continuous at the origin and smooth everywhere except on a hypersurface of codimension 1. We provide an explicit and ``universal'' formula. Finally, we mention a general result connecting asymptotic controllability and the existence of control­Lyapunov functions in the sense of nonsmooth optimization.

A Differential Geometric Approach to motion Planning       \|/ ZIP\|/ PDF\|/
Publication data:  In Nonholonomic Motion Planning, Z. Li and J.F. Canny, Eds, Kluwer Academic Publishers, pp 235-270, 1993.
Coauthor(s): Héctor Sussmann
Abstract:
We propose a general strategy for solving the motion planning problem for real analytic, controllable systems without drift. The procedure starts by computing a control that steers the given initial point to the desired target point for an extended system, in which a number of Lie brackets of the system vector fields are added to the right­hand side. The main point then is to use formal calculations based on the product expansion relative to a P. Hall basis, to produce another control that achieves the desired result on the formal level. It then turns out that this control provides an exact solution of the original problem if the given system is nilpotent. When the system is not nilpotent, one can still produce an iterative algorithm that converges very fast to a solution. Using the theory of feedback nilpotentization, one can find classes of non­nilpotent systems for which the algorithm, in cascade with a precompensator, produces an exact solution in a finite number of steps. We also include results of simulations which illustrate the effectiveness of the procedure.