On the Expressive Power of Cost Logics over Infinite Words
On the Expressive Power of Cost Logics over Infinite Words
复制标题
论成本逻辑对无限词语的表达力
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
M. V. Boom
中科院分区：
文献类型：
--
作者：
Denis Kuperberg;M. V. Boom
代价函数被定义为从一个域（如单词或树）到$\mathbb{N} \cup \left\{{\infty}\right\}$的映射，模等价关系（忽略精确值但保留有界性）。成本逻辑，特别是成本一元二阶逻辑和成本自动机，是定义这些函数的不同方法。这些逻辑和自动机已经被Colcombet等人作为“正则代价函数理论”的一部分进行了研究，这是正则语言理论的扩展，保留了鲁棒等价性，闭包属性和可判定性。我们发展这个理论在无限的话，并表明，经典的结果FO = LTL和MSO = WMSO也保持在这个成本设置（其中的等价性是现在到100）。我们还描述了弱交替自动机与计数器的形式的连接。
Cost functions are defined as mappings from a domain like words or trees to $\mathbb{N} \cup \left\{{\infty}\right\}$, modulo an equivalence relation ≈ which ignores exact values but preserves boundedness properties. Cost logics, in particular cost monadic second-order logic, and cost automata, are different ways to define such functions. These logics and automata have been studied by Colcombet et al. as part of a "theory of regular cost functions", an extension of the theory of regular languages which retains robust equivalences, closure properties, and decidability. We develop this theory over infinite words, and show that the classical results FO = LTL and MSO = WMSO also hold in this cost setting (where the equivalence is now up to ≈). We also describe connections with forms of weak alternating automata with counters.