COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > How undecidable are HyperLTL and HyperCTL*?

## How undecidable are HyperLTL and HyperCTL*?Add to your list(s) Download to your calendar using vCal - Marie Fortin, University of Liverpool
- Friday 04 March 2022, 14:00-15:00
- FW26.
If you have a question about this talk, please contact Jamie Vicary.
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. Two of the most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL * by trace quantification. It is known that this expressiveness comes at a price, i.e., satisfiability is undecidable for both logics. We settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is \Sigma^1_1-complete and HyperCTL* satisfiability is \Sigma^2_1-complete. To prove \Sigma^2_1 membership for HyperCTL*, we prove that every satisfiable HyperCTL* formula has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. This is joint work with Louwe B. Kuijer, Patrick Totzke and Martin Zimmermann. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsPerspectives on Inclusive and Special Education Heritage Research Group Weekly Seminar Series cu palestine society## Other talksHead-on collision of vortex rings CERF Cavalcade 2022 Deep Learning for Inverse Problems in Medical Imaging Cold dark matter subhaloes at arbitrarily low masses Asymptotic results for families of power series distributions Strategic Default and Renegotiation: Evidence from Commercial Real Estate Loans |