LTL到确定性Emerson-Lei自动机
LTL to Deterministic Emerson-Lei Automata
摘要：
我们介绍了一个新的翻译从线性时序逻辑（LTL）确定性Emerson-Lei自动机，这是欧米茄自动机与Muller验收条件象征性地表示为一个布尔公式。更丰富的接受条件结构允许复杂性从状态空间转移到接受条件。从概念上讲，构造是一种增强的产品构造，它利用其组件的知识来减少状态的数量。我们确定了两个片段的LTL，其中一个可以很容易地构建确定性自动机，并显示这些组件的知识可以减少国家的数量。我们将这个想法扩展到一个一般的LTL框架，在那里我们可以使用任意的LTL确定性自动机翻译器的部分公式以外的提到的片段。此外，我们显示简洁的翻译相比，现有的建设。该结构是在工具Delag中实现的，我们对LTL公式和概率模型检验案例研究的几个基准进行了评估。
英文摘要：
We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata, which are omega-automata with a Muller acceptance condition symbolically expressed as a Boolean formula. The richer acceptance condition structure allows the shift of complexity from the state space to the acceptance condition. Conceptually the construction is an enhanced product construction that exploits knowledge of its components to reduce the number of states. We identify two fragments of LTL, for which one can easily construct deterministic automata and show how knowledge of these components can reduce the number of states. We extend this idea to a general LTL framework, where we can use arbitrary LTL to deterministic automata translators for parts of formulas outside the mentioned fragments. Further, we show succinctness of the translation compared to existing construction. The construction is implemented in the tool Delag, which we evaluate on several benchmarks of LTL formulas and probabilistic model checking case studies.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
