摘要：We address robust bounded feasibility verification for a discrete-time PieceWise Affine (PWA) system whose evolution can be influenced by some input. The aim is to determine an input sequence that makes the system satisfy a certain property within a finite time horizon, while maximizing the amount of perturbation that can be applied to the input without violating the given property. This is important to assess the robustness of the solution to numerical errors. We focus on the case of a property expressed in terms of the output of the system taking values in a certain spec set, and propose a verification method resting on reachability computations. The idea is to determine the set of states that the system can reach through all its possible evolutions, with the input taking values in its whole range, and check if the computed reach sets intersect with the one corresponding to the output spec set. If this is the case, then, an input sequence driving the output to the spec set exists and can be determined together with its robustness level by solving a linear optimization program.
