On the Complexity of Realizability for Safety LTL and Related Subfragments
share
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 αψ, where α is a present formula over system variables and ψ contains Next as the only temporal operator. The realizability problem for this new fragment, which we call 𝖦𝖷_0, is also EXP-complete.
READ FULL TEXT