Verification of nonlinear systems through hybridization and invariant set computation

This work addresses the design of an automated tool for nonlinear systems control and verification, and represents a first step to achieve this ambitious and challenging goal. The main focus of our approach is to provide safety guarantees with respect to predefined operation specifications by the design of a safety controller. Safety control design is particularly essential in the face of the on-going industrial revolution that tends to automate and unify high level planning tasks with control of complex dynamics, e.g., in autonomous vehicle fleet management, production lines, and petrochemical plants. The planning task for a system consisting of various subsystems relies on guarantees regarding the operation of underlying systems that are subject to various uncertainties; therefore, control design is needed not only to ensure the task fulfillment at a given level, but also at higher levels to provide safety guarantees while accounting for the uncertain operating environment. Uncertainties can arise due to several sources of error such as linearization, time discretization, and exogenous disturbances to name a few. In our approach, we adopt a hybridization procedure so as to reduce the nonlinear system description to a PieceWise Affine (PWA) model subject to an additive disturbance that allows to account for the introduced approximation error. Safety control design is then performed on the PWA model focusing on safety specifications that require the state of the system to keep evolving within a given compact set. Precisely, our initial step is to divide the state-input space into a hyper-rectangular grid and approximate by linearization the nonlinear system in each grid cell referred to as a mode. In the linearization process we compute on each mode a conservative bound for the error between the PWA model and the original nonlinear system. The conservative error bounds ensure that if safety holds robustly for the PWA model approximation, then, it holds for the nonlinear system as well. Subsequently, safety control design for the PWA system is reformulated as a Mixed Integer Linear Program (MILP). The goal is to determine a PWA control law so as to maximize the volume of a box in the safe set such that the controlled dynamics makes the state remains indefinitely inside that box, which is called maximal controlled invariant box. A main positive feature of the proposed method is that it applies to a general class of nonlinear systems, all those that can be reduce to PWA models through the hybridization procedure. The strength of the approach is its significantly lower computational cost as compared to state of the art Multi-Parametric MILPs (MP-MILP) methods both in offline computation of the control law and in online execution. This allows the algorithm to be applicable to problems of larger sizes. This computational benefit however comes at the price of more restricted and in cases degenerate solutions due mainly to the box-shaping of modes and invariant set. We discuss the limitations of the proposed algorithm and propose methods to alleviate them. In particular, we propose strategies to linearly transform the state space in order to better match the algorithm with the system dynamics or the specification requirements. If the algorithm fails to verify the safety property, we iterate through the hybridiziation and invariant set computation steps and refine the grid at each iteration. We actually use the invariant set computation result to decide the modes in which refinement would be beneficial so as to avoid redundant refinements that increase the computation time. To obtain a sound iterative process, our hybridization procedure guarantees that the refinement inclusion property holds, that is if we refine the grid, then, the possible state evolutions of the obtained PWA model are a subset of those of the previous PWA model built on a rougher grid.

NA