BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Logic of Hybrid Games - Andre Platzer\, CMU
DTSTART:20131011T133000Z
DTEND:20131011T143000Z
UID:TALK47559@talks.cam.ac.uk
CONTACT:Raphael Proust
DESCRIPTION:Hybrid systems model cyber-physical systems as dynamical syste
 ms with interacting discrete transitions and continuous evolutions along d
 ifferential equations.  They arise frequently in many application domains\
 , including aviation\, automotive\, railway\, and robotics.  This talk stu
 dies hybrid games\, i.e. games on hybrid systems combining discrete and co
 ntinuous dynamics. Unlike hybrid systems\, hybrid games allow choices in t
 he system dynamics to be resolved adversarially by different players with 
 different objectives.\n\nThis talk describes how logic and formal verifica
 tion can be lifted to hybrid games.  The talk describes a logic for hybrid
  systems called differential game logic dGL.  The logic dGL can be used to
  study the existence of winning strategies for hybrid games\, i.e. ways of
  resolving the player's choices in some way so that he wins by achieving h
 is objective for all choices of the opponent.  Hybrid games are determined
 \, i.e. one player has a winning strategy from each state\, yet their winn
 ing regions may require transfinite closure ordinals.  The logic dGL\, nev
 ertheless\, has a sound and complete axiomatization relative to any expres
 sive logic.  Separating axioms are identified that distinguish hybrid game
 s from hybrid systems.   Finally\, dGL is proved to be strictly more expre
 ssive than the corresponding logic of hybrid systems.
LOCATION:FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR