 Linear Temporal Logic may also be given a “Team Semantics” of sorts, in which formulas are evaluated with respect to sets of traces (that is to say, sets of sequences of states), representing possible computations of a system. Such a logical framework can be used for the specification and verification of hyperproperties (Krebs et al. 2017, Other Internet Resources; Lück 2020), that is to say, properties like “The system terminates within a bounded amount of time” whose truth cannot be ascertained by checking every possible trace of the system on its own but only by looking at the set of all possible traces as a whole.