ABSTRACT
In this paper, the stability of discrete-time piecewise linear hybrid systems is in-vestigated using piecewise linear Lyapunov functions. In particular, we consider switched discrete-time linear systems and we identify classes of switching sequences that result in stable trajectories. Given a switched linear system, we present a systematic methodology for computing switching laws that guarantee stability based on the matrices of the system. In the proposed approach, we assume that each individual subsystem is stable and admits a piece-wise linear Lyapunov function. Based on these Lyapunov functions, we compose “global” Lyapunov functions that guarantee stability of the switched linear system. A large class of stabilizing switching sequences for switched linear systems is characterized by computing conic partitions of the state space.
ABSTRACT
The problem of minimum-time reachability for timed automata is: given an automaton, and initial state q0 and a target state qf , find whether a run from q0 to qf exists, and if yes, a minimum time run. We show that this problem can be solved by examining acyclic paths in a forward reachability graph generated on-the- y from the timed automaton. Based on this result, we then propose three algorithms with different complex- ities.
ABSTRACT
This contribution describes an approach to investigate reachability properties for a class of controlled hybrid systems. The continuous dynamics of these so-called Switched Continuous Systems (SCS) is selected by the discrete output of a logic controller. While reachability analysis is in general undecidable for this class of systems, the analysis is known to terminate for the class of Timed Automata (TA). In order to make reachability analysis amenable to the control structure, we propose an approximating algorithm to convert a SCS into a TA. Different modifications and extensions of the procedure are given and the approach is illustrated by the application to a chemical reaction system.
ABSTRACT
A well known problem in robotics is the motion planning problem in the presence of static obstacles. The trajectory of the robot must satisfy a linear differential equation as well as possible input and state constraints. In this paper, we explore the use of symbolic reachability algorithms to decide whether the motion planning problem is feasible or not. In the case where it is feasible, it computes a feasible nominal input prole satisfying all system constraints. Our algorithm is based on quantifier elimination techniques in the ordered field of the reals, which have been recently applied to compute the reachable space for classes of linear hybrid systems.