Temporal Team Semantics Revisited

Hyperproperties are an influential framework with the ability to describe important properties such as information flow policies, security requirements or relations between executions of threads in parallel systems. Recently, temporal logics have been studied as an approach to the specification of hyperproperties, resulting in the conception of "hyperlogics". With a few recent exceptions, the hyperlogics thus far developed can only relate different traces of a transition system in a synchronous manner, although important information is contained in the relation between different points in their asynchronous interaction. In order to specify such "asynchronous hyperproperties", new trace quantifier based hyperlogics have been developed. However, certain requirements describing relations between all executions of a system cannot be expressed in hyperlogics with trace quantification. Additionally, these logics induce model checking problems with prohibitively high model checking complexity costs in the number of quantifier alternations. In this paper, we study an alternative approach to asynchronous hyperproperties by introducing a novel foundation of temporal team semantics. Team semantics is a logical framework that specifies properties of sets of traces of unbounded size directly, and thus does not have the same limitation as the quantifier based logics mentioned above. We consider three logics: TeamLTL, TeamCTL and TeamCTL* which employ quantification over so-called "time evaluation functions" controlling the asynchronous progress of traces instead of quantification over traces. The use of time evaluation functions constitutes a novel approach to define expressive logics for hyperproperties where diverse asynchronous interactions between computations can be formalised and enforced. We relate synchronous TeamLTL to our new logics and show how it can be embedded into them. We show that the model checking problem for exists-TeamCTL with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. Finally, we present a translation from TeamCTL* to Alternating Asynchronous Büchi Automata (AABA), and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfiability problems. For the decidable fragments, the complexity is independent of the quantifier depth and indeed polynomial time in the size of the input system for fixed formulae. Our translation constitutes the first approach to team semantics based on automata-theoretic methods.