BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Applications of MetiTarski in the Verification of Control and Hybr
 id Systems - Behzad Akbarpour (University of Cambridge)
DTSTART:20081014T120000Z
DTEND:20081014T130000Z
UID:TALK13420@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:MetiTarski is an automatic proof procedure for inequalities on
  elementary functions. In this talk\, we describe applications of MetiTars
 ki in the verification of control and hybrid systems.\n\nFor control syste
 ms\, we will concentrate on stability analysis based on Nichols plots. Nic
 hols plot plots the gain (in decibels) against the phase-shift of the outp
 ut sinusoid of the system as the frequency varies. Nichols plots have some
  exclusion regions to be avoided for stability and performance. The exclus
 ion region is formulated using inequalities involving arctan\, ln\, and sq
 rt. MetiTarski is then used to solve these inequalities. Two moderately si
 zed case studies are presented\, namely an inverted pendulum and a magneti
 c disk drive reader system. \n\nOn the other hand\, a hybrid system is a d
 ynamical system that involves both continuous and discrete states. An impo
 rtant task is to verify that a given hybrid system is safe. Many hybrid sy
 stems 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.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR