论文标题
关于自动机向线性时间逻辑的翻译
On the Translation of Automata to Linear Temporal Logic
论文作者
论文摘要
虽然将未来的线性时间逻辑（LTL）转换为无限单词的自动机的复杂性是充分理解的，但将自动机回到LTL的大小增加并非如此。特别是，在将确定性的$ω$ -GROMAMALA自动机转换为LTL的复杂性上没有已知的基本结合。我们的第一个贡献包括LTL的紧密界限：交替，非确定性和确定性自动机的交替，分别与任何等效的LTL公式相比，分别是指数性，四边形和线性更为简洁的。我们的主要贡献包括使用中级krohn-rhodes cascade cascade cascade Demottions的翻译，将一般无反对确定性的$ω$定型自动机转换为双指数的时间嵌入式深度和三重指数长度的LTL公式。据我们所知，这是该翻译的第一个基本界限。此外，我们的翻译将自动机的接受条件保留在循环，弱，büchi，cobüchi或muller automaton的意义上，成为属于属性未来层次结构的匹配类别的公式。特别是，它可用于将识别安全性语言的LTL公式转换为属于LTL安全片段的公式（有限和无限单词）。
While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the complexity of translating deterministic $ω$-regular automata to LTL. Our first contribution consists of tight bounds for LTL over a unary alphabet: alternating, nondeterministic and deterministic automata can be exactly exponentially, quadratically and linearly more succinct, respectively, than any equivalent LTL formula. Our main contribution consists of a translation of general counter-free deterministic $ω$-regular automata into LTL formulas of double exponential temporal-nesting depth and triple exponential length, using an intermediate Krohn-Rhodes cascade decomposition of the automaton. To our knowledge, this is the first elementary bound on this translation. Furthermore, our translation preserves the acceptance condition of the automaton in the sense that it turns a looping, weak, Büchi, coBüchi or Muller automaton into a formula that belongs to the matching class of the syntactic future hierarchy. In particular, it can be used to translate an LTL formula recognising a safety language to a formula belonging to the safety fragment of LTL (over both finite and infinite words).
