Synchronous Team Semantics for Temporal Logics

TL;DR

The paper develops synchronous team semantics for LTL and CTL, introducing TeamLTL and TeamCTL to capture hyperproperties beyond standard trace properties. It provides a thorough complexity landscape: TeamLTL satisfiability and path checking are $PSPACE$-complete, with model checking tractable for splitjunction-free fragments and open for the general case; TeamCTL model checking is $PSPACE$-complete and satisfiability is $EXPTIME$-complete. It also analyzes extensions (dependence/inclusion atoms, generalized FO-atoms, and contradictory negation) and compares TeamLTL to HyperLTL, showing incomparability in expressivity. The work highlights that temporal team semantics offer a viable, sometimes simpler alternative for specifying and verifying hyperproperties, while uncovering rich avenues for future research in expressivity, fragments, and validity questions.

Abstract

We present team semantics for two of the most important linear and branching time specification languages, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). With team semantics, LTL is able to express hyperproperties, which have in the last decade been identified as a key concept in the verification of information flow properties. We study basic properties of the logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of the basic logic react to adding additional atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL with team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties. For CTL with team semantics, we investigate the computational complexity of the satisfiability and model checking problem. The satisfiability problem is shown to be EXPTIME-complete while we show that model checking is PSPACE-complete.

Figures (4)

• Figure 1: Overview of complexity results for $\mathrm{TeamLTL}$ and $\mathrm{TeamCTL}$. '$\mathop{\mathrm{\mathrm{dep}}}\nolimits$' refers to dependence atoms, '$\sim$' refers to the contradictory negation, $\varovee$ refers to the Boolean disjunction, $\mathcal{D}$ refers to any finite set of first-order definable generalised atoms, and '$\mathrm{TeamLTL}\xspace-\lor$' refers to disjunction free $\mathrm{TeamLTL}$. All results are completeness results unless otherwise stated. We write '?' for open cases and '--' if the problem is not meaningful for the logic.
• Figure 2: Structural properties overview for $\mathrm{TeamLTL}$.
• Figure 5: (left) A team $T$ does not satisfy the $\mathrm{TeamCTL}$ formula $\mathsf{E}\mathsf{F} p$ while all singleton teams $\{ \{ v\} \} \subseteq T$ individually do satisfy the formula. (right) The multiplicity of elements in a team matters: If the multiplicity of the world w in $S$ is $1$ then $S$ satisfies $\mathsf{A}\mathsf{F} p$, while for larger multiplicities $S$ falsifies $\mathsf{A}\mathsf{F} p$.
• Figure 7: Example structure built in proof of Lemma \ref{['lem:mcs-pspacehard']} for the qBf $\exists x_1\forall x_2\exists x_3(x_1\lor\lnot x_2\lor \lnot x_3)\land(\lnot x_1\lor x_2\lor x_3)\land(\lnot x_1\lor \lnot x_2\lor \lnot x_3)$.

Theorems & Definitions (38)

• proposition 1
• lemma 1
• Remark 1
• lemma 2
• theorem 1
• theorem 2
• definition 1
• theorem 3
• proposition 2: Hannula:2018:CPL:3176362.3157054
• theorem 4