Temporal Team Semantics Revisited
Jens Oliver Gutsfeld, Arne Meier, Christoph Ohrem, Jonni Virtema
TL;DR
This work reframes asynchronous hyperproperties by introducing temporal team semantics based on time evaluation functions ($TEFs$), enabling direct quantification over asynchronous progress of multiple traces rather than over traces themselves. It builds a unifying framework for TeamLTL, TeamCTL, and TeamCTL* with extensions such as dependence and inclusion atoms, and shows how synchronous TeamLTL embeds into this setting. The authors demonstrate that some fragments (e.g., exists TeamCTL with disjunction) are highly undecidable, while also providing a novel automata-theoretic route by translating TeamCTL* into Alternating Asynchronous Büchi Automata (AABA) and GAABA, yielding decidability results for path checking and certain finite variants under restricted TEFs. This automata-based viewpoint offers a foundational approach to solving decision problems in temporal team semantics and lays groundwork for future restricted/semi-decidable fragments and broader applicability to asynchronous hyperproperties.
Abstract
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 synchronously. However, important information is contained in the relation between different points in their asynchronous interaction. To specify such "asynchronous hyperproperties", new trace quantifier based hyperlogics have been developed. Yet, hyperlogics with trace quantification cannot express certain requirements that describe the relationships between all executions of a system. Also, these logics induce model checking problems (MC) with prohibitively high complexity costs in the number of quantifier alternations. 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 temporal team logics which employ quantification over so-called "time evaluation functions" (TEFs) controlling the asynchronous progress of traces instead of quantification over traces. TEFs constitute a novel approach to defining expressive logics for hyperproperties where diverse asynchronous interactions between computations can be formalised and enforced. We show embeddings of synchronous TeamLTL into our new logics. We show that MC for some TeamCTL fragment is highly undecidable. We present a translation from TeamCTL* to Alternating Asynchronous Büchi Automata, and obtain decidability results for the path checking problem and restrictions of MC and SAT. Our translation constitutes the first approach to team semantics based on automata-theoretic methods.