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.
翻译：我们研究了安全LTL的可变性问题,这是线性时空逻辑捕捉安全公式的合成碎片。 我们显示问题已经完成, 无法证明现有的2EXP完整性的假设。 我们通过将安全LTL的复杂性与看起来较弱的亚裂块进行比较来实现这一目标。 特别是, 我们显示, 安全LTL的每种公式都可以降低到一个可等化的公式, 即 $\alpha\ land\Box\psi$, 其中, $\alpha$是当前系统变量的公式, $\psi$包含下一个唯一的时间操作器。 这个新碎片的可变性问题, 我们称之为$mathsf{G{Xathsf{0$, 也是 EXP的完成 。
相关内容
微信扫码咨询专知VIP会员