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:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:**Cancelled** Logic of Hybrid Games - Andre Platze
r\, CMU
DTSTART;TZID=Europe/London:20130628T160000
DTEND;TZID=Europe/London:20130628T170000
UID:TALK45526AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/45526
DESCRIPTION:Hybrid systems model cyber-physical systems as dyn
amical systems with interacting discrete transitio
ns and continuous evolutions along differential eq
uations. They arise frequently in many applicatio
n domains\, including aviation\, automotive\, rail
way\, and robotics. We study hybrid games\, i.e.
games on hybrid systems combining discrete and con
tinuous dynamics. Unlike hybrid systems\, hybrid g
ames allow choices in the system dynamics to be re
solved adversarially by different players with dif
ferent objectives.\n\nThis talk describes how logi
c and formal verification can be lifted to hybrid
games. The talk describes a logic for hybrid syst
ems called differential game logic dGL. The logic
dGL can be used to study the existence of winning
strategies for hybrid games. We present a simple
sound and complete axiomatization of dGL relative
to the fixpoint logic of differential equations.
We prove hybrid games to be determined and their
winning regions to require higher closure ordinals
and we identify separating axioms\, i.e. axioms t
hat distinguish hybrid games from hybrid systems.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Jonathan Hayman
END:VEVENT
END:VCALENDAR