BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:How undecidable are HyperLTL and HyperCTL*? - Marie Fortin\, Unive
 rsity of Liverpool
DTSTART:20220304T140000Z
DTEND:20220304T150000Z
UID:TALK169205@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:*THIS TALK WILL BE IN SS03\, NOT FW26*\n\nTemporal logics for 
 the specification of information-flow properties are able to express relat
 ions between multiple executions of a system. Two of the most important su
 ch logics are HyperLTL and HyperCTL&#42\;\, which generalise LTL and CTL&#
 42\; by trace quantification. It is known that this expressiveness comes a
 t a price\, i.e.\, satisfiability is undecidable for both logics. We settl
 e the exact complexity of these problems\, showing that both are in fact h
 ighly undecidable: we prove that HyperLTL satisfiability is \\Sigma&#94\;1
 _1-complete and HyperCTL&#42\; satisfiability is \\Sigma&#94\;2_1-complete
 . To prove \\Sigma&#94\;2_1 membership for HyperCTL&#42\;\, we prove that 
 every satisfiable HyperCTL&#42\; formula has a model that is equinumerous 
 to the continuum\, the first upper bound of this kind. We prove this bound
  to be tight.\n\nThis is joint work with Louwe B. Kuijer\, Patrick Totzke 
 and Martin Zimmermann.
LOCATION:FW26
END:VEVENT
END:VCALENDAR