Reachability of Uncertain Nonlinear Systems Using a Nonlinear Hybridization

Abstract. In this paper, we investigate nonlinear reachability compu-tation in presence of model uncertainty, via guaranteed set integration. We show how this can be done by using the classical Müller’s existence theorem. The core idea developed is to no longer deal with whole sets but to derive instead two nonlinear dynamical systems which involve no model uncertainty and which bracket in a guaranteed way the space reachable by the original uncertain system. We give a rule for building the bracketing systems. In the general case, the bracketing systems ob-tained are only piecewise Ck-continuously differential nonlinear systems and hence can naturally be modeled with hybrid automata. We show how to derive the hybrid model and how to address mode switching. An example is given with a biological process. 1 Introducion Computing reachable sets for hybrid systems is an important step when one addresses verification or synthesis taks. A key issue then lays in the calcula-tion of the reachable space for continuous dynamics with nonlinear models. In this paper, we will also emphasize the presence of parameter uncertainty in the nonlinear dynamical models used for characterizing the continuous dynamics. Consider an uncertain dynamical system described by non-autonomous dif-ferential equations with the following form:{ ẋ(t) = f(x,p, t), x(t0) ∈ X0 ⊆ D, p ∈ P (1) where function f: D ×P × IR+ 7 → IRn is possibly nonlinear, D ⊆ IRn, X0 is the initial domain for state vector x at time t0 ≥ 0 and P is an uncertainty domain for parameter vector p. The reachable space of system (1) is then defined as follows R([t0, t];X0) = x(τ), t0 ≤ τ ≤ t | (ẋ(τ) = f(x,p, τ)) ∧ (x(t0) ∈ X0) ∧ (p ∈ P