Deterministic Automata for the (F,G)-fragment of LTL
Deterministic Automata for the (F,G)-fragment of LTL
复制标题
LTL (F,G) 片段的确定性自动机
DOI：
10.1007/978-3-642-31424-7_7
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
J. Esparza
中科院分区：
文献类型：
--
作者：
Jan Křetínský;J. Esparza
当在游戏或概率系统的设置中处理线性时序逻辑属性时，人们通常需要将它们表示为确定性欧米茄自动机。为了将LTL转化为确定性的omega-自动机，传统的方法首先将公式转化为非确定性的Buchi自动机。然后执行确定性过程，例如Safra，产生确定性ω-自动机。我们提出了一个直接的翻译的（F，G）-片段的LTL到确定性ω-自动机，没有涉及确定性的过程。由于我们的方法是针对LTL的，我们经常避免通常不必要的大爆破所造成的一般确定性算法。我们调查这种翻译的复杂性，并提供实验结果，并将其与传统方法进行比较。
When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Buchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic ω-automaton. We present a direct translation of the ( F , G )-fragment of LTL into deterministic ω-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation and provide experimental results and compare them to the traditional method.