BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification of Control Laws Using Formal Methods - Kestutis Siaul
 ys\, University of Cambridge
DTSTART:20170511T130000Z
DTEND:20170511T140000Z
UID:TALK72525@talks.cam.ac.uk
CONTACT:Tim Hughes
DESCRIPTION:In this talk\, we show how general analysis/synthesis problems
  in control theory can be expressed as quantified first order formulas and
  introduce a verification approach based on formal methods (in particular\
 , quantifier elimination (QE) algorithms). This verification approach work
 s by expressing a verification criterion of choice in a mathematical form 
 that one of the QE algorithms (such as cylindrical algebraic decomposition
  (CAD) or Weispfenning's virtual substitution algorithm) are capable of ch
 ecking.\n\nConsequently\, this allows us to analyse problems from a differ
 ent angle. One of the main benefits of the proposed approach based on QE a
 lgorithms is that these procedures work by algebraically manipulating the 
 mathematical expression representing the verification criterion to arrive 
 at the conclusion and do not involve numerical techniques such as simulati
 on or gridding. This guarantees that verification by QE algorithms does no
 t miss a critical frequency or parameter combination at which the desired 
 property is violated. Additionally\, the generality of these methods allow
 s us to relax some standard conditions like convexity of the cost function
  in the optimisation problem.\n\nThe downside to this approach is the comp
 utational penalty that has to be paid when compared to numerical methods\,
  especially when a general QE algorithm (like CAD) is used. Hence\, we foc
 us our attention to control problems that can be converted to quantifier e
 limination ones with a particular quantification structure.\n\nAs an examp
 le\, we propose a method based on Weispfenning's `quantifier elimination b
 y virtual substitution' algorithm for obtaining explicit model predictive 
 control (MPC) laws for linear time invariant systems with quadratic object
 ive and polytopic constraints. Weispfenning's algorithm is applicable to f
 irst order formulas in which quantified variables appear at most quadratic
 ally. It has much better practical computational complexity than general q
 uantifier elimination algorithms\, such as cylindrical algebraic decomposi
 tion. Additionally\, we show how this explicit MPC solution\, together wit
 h Weispfenning's algorithm\, can be used to check recursive feasibility of
  the system\, for both nominal and disturbed systems. Finally\, we show ho
 w the structured singular value calculation problem can be tackled with We
 ispfenning's algorithm as well.
LOCATION: Cambridge University Engineering Department\, LR6
END:VEVENT
END:VCALENDAR