A method for detecting relevant inputs while satisfying a reachability specification for piecewise affine systems

摘要

We address input design for piecewise affine systems so as to satisfy a reachability specification, and, simultaneously, detect the inputs that are actually relevant (influential inputs). This can be useful for system verification, when one has to check if some undesired/unsafe behavior coded via a reachability specification can actually occur and then possibly take appropriate corrective actions. The proposed method is based on a procedure to assess whether a set of inputs are non-influential for the given specification. This procedure rests on a geometrical set-containment test that involves a projection of the set of states that the system can reach and the set of states that represents the specification. The test can be formulated as a mixed integer feasibility problem and integrated in a depth-first exploration algorithm that returns the maximum number of non-influential inputs.