关于自动机到线性时序逻辑的翻译

尽管将未来线性时序逻辑（LTL）翻译为无穷字上的自动机的复杂性已被充分理解，但将自动机转回 LTL 所涉及的大小增长却并非如此。特别地，对于将确定性 $\omega$-正则自动机翻译为 LTL 的复杂性，尚无已知初等界。我们的第一个贡献给出了 unary 字母表上 LTL 的紧界：交替、非确定性和确定性自动机分别可以比任何等价的 LTL 公式精确指数级、二次方级和线性级更简洁。我们的主要贡献在于，利用自动机的中间 Krohn-Rhodes 级联分解，将一般的无计数器确定性 $\omega$-正则自动机翻译为具有双重指数时间嵌套深度和 triple 指数长度的 LTL 公式。据我们所知，这是该翻译的首个初等界。此外，我们的翻译在保持自动机接受条件的意义下，将 looping、weak、Büchi、coBüchi 或 Muller 自动机转换为属于语法未来层次结构相应类的公式。特别地，它可用于将识别安全语言的 LTL 公式翻译为属于 LTL 安全片段（在有限和无穷字上）的公式。