BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:CUED Control Group Seminars
SUMMARY:Verification of Control Laws Using Formal Methods
- Kestutis Siaulys\, University of Cambridge
DTSTART;TZID=Europe/London:20170511T140000
DTEND;TZID=Europe/London:20170511T150000
UID:TALK72525AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/72525
DESCRIPTION:In this talk\, we show how general analysis/synthe
sis problems in control theory can be expressed as
quantified first order formulas and introduce a v
erification approach based on formal methods (in p
articular\, quantifier elimination (QE) algorithms
). This verification approach works by expressing
a verification criterion of choice in a mathematic
al form that one of the QE algorithms (such as cyl
indrical algebraic decomposition (CAD) or Weispfen
ning's virtual substitution algorithm) are capable
of checking.\n\nConsequently\, this allows us to
analyse problems from a different angle. One of th
e main benefits of the proposed approach based on
QE algorithms is that these procedures work by alg
ebraically manipulating the mathematical expressio
n representing the verification criterion to arriv
e at the conclusion and do not involve numerical t
echniques such as simulation or gridding. This gua
rantees that verification by QE algorithms does no
t miss a critical frequency or parameter combinati
on at which the desired property is violated. Addi
tionally\, the generality of these methods allows
us to relax some standard conditions like convexit
y of the cost function in the optimisation problem
.\n\nThe downside to this approach is the computat
ional penalty that has to be paid when compared to
numerical methods\, especially when a general QE
algorithm (like CAD) is used. Hence\, we focus our
attention to control problems that can be convert
ed to quantifier elimination ones with a particula
r quantification structure.\n\nAs an example\, we
propose a method based on Weispfenning's `quantifi
er elimination by virtual substitution' algorithm
for obtaining explicit model predictive control (M
PC) laws for linear time invariant systems with qu
adratic objective and polytopic constraints. Weisp
fenning's algorithm is applicable to first order f
ormulas in which quantified variables appear at mo
st quadratically. It has much better practical com
putational complexity than general quantifier elim
ination algorithms\, such as cylindrical algebraic
decomposition. Additionally\, we show how this ex
plicit MPC solution\, together with Weispfenning's
algorithm\, can be used to check recursive feasib
ility of the system\, for both nominal and disturb
ed systems. Finally\, we show how the structured s
ingular value calculation problem can be tackled w
ith Weispfenning's algorithm as well.
LOCATION: Cambridge University Engineering Department\, LR6
CONTACT:Tim Hughes
END:VEVENT
END:VCALENDAR