Complexity of LTL realizability of safety games with Next operator only

Question

It is known that the computational complexity of deciding whether an LTL specification is realizable in a safety game is 2EXP-complete (that is, you receive an LTL formula, where some variables belong to the environment and some to the system, and you ask if it's possible for the system to always satisfy the specification, at every point in time, no matter what the environment does).

I am interested in the particular case where the specification contains Next as the only temporal operator. Given such a restricted specification, where X is the only temporal operator, what is the complexity of deciding realizability? Is it known?

I am considering here a temporal formula $\psi$ containing X as the only temporal operator, and where we ask for $\psi$ to be satisfied at every point in time, i.e., $\text{G }\psi$.

My intuition is that this should be EXP-complete, but I do not have a proof.

EDIT: as mentioned in the answers below, I am interested in safety specifications of the form $\alpha \land \text{G } \psi$ where $\alpha$ is a Boolean formula over system variables specifying the initial conditions (no temporal operators here) and $\psi$ contains X as the only temporal operator, so that the only instance of G is the one at the front of $\psi$. The question is about the complexity of checking realizability of $\alpha \land \text{G } \psi$.

Answer 1

Indeed, the complexity of the reactive synthesis problem is lower if the only temporal operator allowed in the LTL specification is the Next-Time operation.

Let's consider the case that there is no occurrence of the "globally" operator first. Your complexity estimate can be refined to PSPACE-completeness then.

The canonical problem for PSPACE-completeness is the validity problem for quantified Boolean formulas (QBF). It is essentially equivalent to your problem, from which the claimed computational complexity follows.

In a QBF problem, you are given a Boolean formula $\psi$ over a set of variables $\{x^1_1, \ldots, x^1_{n_1}, y^2_1, \ldots, y^2_{n_2}, \ldots, x^m_{1}, \ldots, x^m_{n_m}\}$ and you ask the question if

$$\exists x^1_1, \ldots, x^1_{n_1} \forall y^2_1, \ldots, y^2_{n_2} \exists \ldots \exists x^m_{1}, \ldots, x^m_{n_m}. \psi$$

is $\mathbf{true}$ or $\mathbf{false}$. This is very similar to your LTL-with-only-next realizability problem. If you have such a specification, you can compute the number $k$ representing the deepest Next-nesting. After both environment and system decided their first $k$ input and output variable values, it is fixed whether the specification is satisfied on any (infinite) extension of their decisions. If you store the decisions of the environment and the system in the first $k$ steps into separate Boolean variables, then you can modify the LTL formula to replace all variable names by their respective new variable names in the step of the execution they refer to. The next-time operator occurrences can then be removed. Then you have a problem that looks exactly like the QBF problem above.

Note that you can also do this translation in the reverse direction. The only non-straight-forward aspect is that on every quantification level, the number of variables in constant in the reactive synthesis problem. But by using sufficiently many input/output variables in the synthesis problem and ignoring the unused variable values in the specification, this aspect can be addressed.

I am not aware of this complexity result being mentioned in any paper - it's certainly not a result that is sufficient for a paper on its own. The paper "Deterministic Generators and Games for LTL Fragments" by Alur and La Torre (2001) does not seem to discuss your particular case, and it probably the most well-known one discussing syntactic LTL restrictions in the scope of reactive synthesis. There may be some paper proving PSPACE-completeness of your result as a lemma, though.

Now let's consider the case that there is a globally operator spanning the most of the LTL formula. The problem becomes APSPACE=EXPTIME-complete in this case. You can encode the acceptance of a alternating polynomial-space Turing machine into the realizability problem restricted to this case and vice versa.

Let's consider containment in APSPACE first. For this, you reduce the non-realizability of an LTL specification of your particular shape to the acceptance by an alternating Turing machine with a polynomail space bound. Starting from your specification, you can compute the maximal number of nesting of the next-time operator. Let this number be $k$. You then encode a polynomially space-bounded Turing machine that always keeps track of the last $k$ values of the input and output variables. This allows you to check $\psi$ locally on these values. You assign the task to choose input proposition values to the existential non-determinism, and output proposition values to the universal non-determinism. You encode the Turing machine to accept if eventually the specification is violated, i.e., if the last $k$ variable valuations do not satisfy $\psi$. If the specification is realizable, the Turing machine does not accept. If it's realizable, it accepts.

Now let's consider APSPACE-hardness. For this, you encode the non-acceptance of the empty word of an alternating Turing machine to the realizability problem of your particular shape. Let's assume that the specification shape should be $\alpha \wedge \mathbf{G}(\psi)$. You allocate enough output propositions to output the complete tape content of the Turing machine (times two) along with the state of the Turing machine and the position on the tape. In $\alpha$, you encode that initially, the machine should be in the middle of the tape in the initial state. You use an input proposition to resolve universal non-determinism of the Turing machine. In $\psi$, you encode that the output proposition value changes encode the transition function/relation of the Turing machine, where the input propositions are used to choose successor state/value combinations for universal non-determinism. Finally, you add a conjunct in $\psi$ requiring that accepting states in the Turing machine are never visited.

If your specification is of the form $\mathbf{G}(\psi)$ and not $\alpha \wedge \mathbf{G}(\psi)$, you need to apply a little trick. You add an input proposition for resetting the execution. Whenever the reset proposition is 1, the Turing tape content and machine start is reset to the start. Otherwise, simulation of the Turing machine works as before. In this way, you don't need the $\alpha$ component for EXPTIME-hardness.

Doing the latter proof fully precise is tricky, as it requires you to also reason about executions of the Turing machine on which the tape boundaries are exceeded. There are some details that make a full formal proof rather lenghty.