Abstract

MetiTarski is an automatic proof procedure for inequalities on elementary functions. In this talk, we describe applications of MetiTarski in the verification of control and hybrid systems.

For control systems, we will concentrate on stability analysis based on Nichols plots. Nichols plot plots the gain (in decibels) against the phase-shift of the output sinusoid of the system as the frequency varies. Nichols plots have some exclusion regions to be avoided for stability and performance. The exclusion region is formulated using inequalities involving arctan, ln, and sqrt. MetiTarski is then used to solve these inequalities. Two moderately sized case studies are presented, namely an inverted pendulum and a magnetic disk drive reader system.

On the other hand, a hybrid system is a dynamical system that involves both continuous and discrete states. An important task is to verify that a given hybrid system is safe. Many hybrid systems can be specified by systems of differential equations. We can solve these using Maple, typically yielding a problem involving the exponential and trigonometric functions. Examples include Collision Avoidance, Room Heating, and Navigation systems.