Being hyper: the complexity of temporal hyper-logics

24^th May 2021, 16:00
Louwe Kuijer

Abstract

Temporal logics, such as Linear Temporal Logic (LTL) and the more complex Computation Tree Logic (CTL/CTL*), can be used to reason about the behaviour of (computer) systems. Any possible execution of such a system can be represented by a trace, i.e., a sequence s(0), s(1) , ... such that the system is in state s(i) at time i. A single system typically has multiple possible executions, either due to nondeterminism or simply because the system can be initiated with different inputs.



LTL is designed to reason about individual traces of the system, and allows the user to verify various standard properties, such as liveness or safety ("in every possible execution, a certain event occurs infinitely often/never"). CTL* additionally allows reasoning about the branching nature of the system and can express properties such as "it is always possible to reach a certain state s from the current one".



However, both logics are only able to refer to one trace at a time. What they cannot do is compare different traces to each other. HyperLTL and HyperCTL* extend LTL and CTL* with path quantifiers that do allow such a comparison. For example, in a situation where both input and output to the system are divided into public and private parts, one may want to formalize that no information leaks, in the sense that any two traces with the same public input should have the same public output.



Unfortunately, the extra expressive power that these path quantifiers provide comes at a price. In this talk we discuss one aspect of this price, namely the computational complexity of the satisfiability problem for these logics (both of which are undecidable). We show that HyperLTL satisfiability is ?^1_1 complete (which is very high) and HyperCTL* satisfiability is ?^2_1 complete (which is infinitely higher).