Safety Analysis of Hybrid Systems with SpaceEx

– number type is templated (substitute your own) … – interfaces to linear programming solvers (GLPK,PPL), Parma … – additive “inputs” u,w model continuous disturbances (noise etc.) … – plus event detection over a dense domain … – Transition Successors Mixing Support Functions and Polyhedra … – explicit solution at discrete points in time … – Compute reachable states over finite time: Reach … – x(t) is in ǫ(δ)-neighborhood of some X … – discrete transitions might “fire” between sampling times … – if transitions are “missed,” x(t) not in ǫ(δ)-neighborhood … – In other examples this error might not be as obvious … – variables x  ,…,x n , inputs u  ,…,u p … – can be used for overapproximating nonlinear dynamics … – How far can the input “push” the system in δ time … X 0 X δ X 0 X δ … 0 and X δ = eAδ X 0 … Taylor approximation of inputs with error bound … – bound remainder with absolute value sum instead of …