REACHABILITY COMPUTATION FOR UNCERTAIN PLANAR AFFINE SYSTEMS USING LINEAR ABSTRACTIONS

Reachability computation is the central problem arising in the verification of hybrid or continuous systems. One approach, among others, to compute an over approximation of the reachable space is to split the continuous state space and to abstract the continuous dynamics in each resulting cell by a linear differential inclusion for which the reachable space may be computed with polyhedra. A previous work proposed to use characteristics of the affine continuous dynamics to guide the polyhedral partition. This paper presents an extension of this approach to uncertain planar systems where one parameter of the model may take its value in a polytope. t is shown that the result for all values of the parameter may be deduced from the computation for a finite number of values. An algorithm that performs the reachability computation and determines the minimum number of values of the parameter required at each step is proposed and exemplified.