Applications of MetiTarski in the Verification of Control and Hybrid Systems

MetiTarski, an automatic proof procedure for inequalities on elementary functions, can be used to verify control and hybrid systems. We perform a stability analysis of control systems using Nichols plots, presenting an inverted pendulum and a magnetic disk drive reader system. Given a hybrid systems specified by a system of differential equations, we use Maple to obtain a problem involving the exponential and trigonometric functions, which MetiTarski can prove automatically.

• Type: Conference
• Year: 2009
• Where: HYBRID
• Authors: Behzad Akbarpour, Lawrence C. Paulson
• Keywords: Automatic Proof Procedure, Control Systems, HYBRID 2009, Hybrid Systems, Magnetic Disk Drive