COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Applications of MetiTarski in the Verification of Control and Hybrid Systems

## Applications of MetiTarski in the Verification of Control and Hybrid SystemsAdd to your list(s) Download to your calendar using vCal - Behzad Akbarpour (University of Cambridge)
- Tuesday 14 October 2008, 13:00-14:00
- Computer Laboratory, William Gates Building, Room SS03.
If you have a question about this talk, please contact Thomas Tuerk. 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. This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Laboratory Automated Reasoning Group Lunches
- Computer Laboratory, William Gates Building, Room SS03
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsCorrelated quantum systems discussion group Required lists for MLG IOP East Anglia Branch Applied Physics Seminars## Other talksThe Digital Doctor: Hope, Hype, and Harm at the Dawn of Medicine’s Computer Age Connecting behavioural and neural levels of analysis Statistical Methods in Pre- and Clinical Drug Development: Tumour Growth-Inhibition Model Example The world is not flat: towards 3D cell biology and 3D devices Cycloadditions via TMM-Pd Intermediates: New Strategies for Asymmetric Induction and Total Synthesis Simulating Electricity Prices: negative prices and auto-correlation 'Cambridge University, Past and Present' Cambridge - Corporate Finance Theory Symposium September 2017 - Day 2 The role of the oculomotor system in visual attention and visual short-term memory The evolution of photosynthetic efficiency How could education systems research prompt a change to how DFIS works on education |