On the Complexity of Realizability for Safety LTL and Related Subfragments

TL;DR

This paper proves that the realizability problem for Safety LTL, a fragment of Linear Temporal Logic, is EXP-complete, correcting previous conjectures and analyzing related subfragments.

Contribution

It establishes the exact complexity of Safety LTL realizability as EXP-complete and introduces a new fragment, GX0, with the same complexity.

Findings

Safety LTL realizability is EXP-complete.

Every Safety LTL formula reduces to a formula of the form α ∧ ◻ψ.

Realizability for the GX0 fragment is also EXP-complete.

Abstract

We study the realizability problem for Safety LTL, the syntactic fragment of Linear Temporal Logic capturing safe formulas. We show that the problem is EXP-complete, disproving the existing conjecture of 2EXP-completeness. We achieve this by comparing the complexity of Safety LTL with seemingly weaker subfragments. In particular, we show that every formula of Safety LTL can be reduced to an equirealizable formula of the form $\alpha \land \Box \psi$, where $\alpha$ is a present formula over system variables and $\psi$ contains Next as the only temporal operator. The realizability problem for this new fragment, which we call $\mathsf{GX}_{\mathsf{0}}$, is also EXP-complete.