ALGORITHMIC ANALYSIS OF NONLINEAR HYBRID SYSTEMS

Hybrid systems are digital real-time systems that are embedded in anal og environments. Model-checking tools are available for the automatic analysis of linear hybrid automata, whose environment variables are su bject to piecewise-constant polyhedral differential inclusions, In mos t embedded systems, however, the environment variables have differenti al inclusions that vary with the values of the variables, e.g,, (x) ov er dot = x, Such inclusions are prohibited in the linear hybrid automa ton model, We present two methods for translating nonlinear hybrid sys tems into linear hybrid automata, Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated lin ear hybrid automata. The first method, called clock translation, repla ces constraints on nonlinear variables by constraints on clock variabl es. The clock translation is efficient but has limited applicability, The second method, called linear phase-portrait approximation, conserv atively overapproximates the phase portrait of a hybrid automaton usin g piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties; that is; if we establish a safety pro perty of the translated linear system, we may conclude that the origin al nonlinear system satisfies the property, When applicable, the clock translation is also complete for safety properties; that is, the orig inal system and the translated system satisfy the same safety properti es. The phase-portrait approximation method is not complete for safety properties, but it is asymptotically complete; intuitively, for every safety property, and for every relaxed nonlinear system arbitrarily c lose to the original, if the relaxed system satisfies the safety prope rty, then there is a linear phase-portrait approximation that also sat isfies the property. We illustrate both methods by using HYTECH-a symb olic model checker for linear hybrid automata-to automatically check p roperties of a nonlinear temperature controller and of a predator-prey ecology.