Temporal Team Semantics Revisited

We introduce a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We define three new logics: TeamLTL, TeamCTL and TeamCTL∗, which are obtained by adding quantification over so-called time evaluation functions controlling the asynchronous progress of traces. We study the complexity of model checking of different fragments of the new logics, and map their undecidability boundier. We show that the model checking problem for already the existential fragment of TeamCTL with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. On the positive side, we present a translation from TeamCTL∗ to Alternating Asynchronous Büchi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfiability problems. Finally, we identify a restrictive setting in which model checking can be done in polynomial time. This is joint work with Jens Oliver Gutsfeld, Arne Meier, and Christoph Ohrem.

Authors

• Jonni Virtema

Keywords

No keywords are indexed for this paper.