On the complexity of linear temporal logic with team semantics (Q2193280)

The paper considers the well-known temporal logic LTL, but with a novel semantics, based on teams, that is, sets of traces rather than single traces. Boolean negation is also added, since it is not available in the logic, where Boolean connectives behave in a nonstandard way. The problem of characterizing stuttering-invariant formulas is partially solved. Satisfiability and model checking of LTL with negation are shown to be logspace equivalent to third-order arithmetic.