Convex programs for temporal verification of nonlinear dynamical systems
A methodology for safety verification of continuous and hybrid systems using barrier certi.ficates has been proposed recently. Conditions that must be satisfi.ed by a barrier certi. cate can be formulated as a convex program, and the feasibility of the program implies system safety in the sense that there is no trajectory starting from a given set of initial states that reaches a given unsafe regi
