几乎线性Büchi自动机
Almost Linear Büchi Automata
摘要：
本文介绍了线性时序逻辑的一个新的片段LIO和一类新的Buechi自动机ALBA。我们提供了有效的翻译LIO和ALBA表明，这两种形式主义是表达等价的。虽然LTL到BA的标准翻译使用一些中间形式，但LIO到ALBA的翻译是直接的。正如我们所期望的ALBA在模型检验中的应用，我们比较了ALBA与其他类的Buechi自动机研究在这方面的表现力，我们指出可能的应用。
英文摘要：
We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Buechi automata (BA) called Almost linear Buechi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Buechi automata studied in this context and we indicate possible applications.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
