无限词语言的有界性
Boundedness in languages of infinite words
AI总结：
本文定义了严格扩展ω-正则语言的新语言类，通过引入两种新的Kleene星号变体（有界和无界）及对应的自动机模型，并证明了补集引理，从而为相关逻辑MSOLB获得部分可判定性结果。
摘要：
我们定义了一个新的ω-词语言类，严格扩展了ω-正则语言。呈现这个新类的一种方式是通过一种正则表达式类型。新表达式是ω-正则表达式的扩展，其中添加了Kleene星号$L^*$的两种新变体：$L^B$和$L^S$。这些新指数分别用于表示输入词的部分具有有界大小，以及输入的部分可以具有任意大的大小。例如，表达式$(a^Bb)^ω$表示字母$a,b$上的无限词语言，其中连续字母$a$的数量存在一个公共界限。表达式$(a^Sb)^ω$表示类似的语言，但这次要求连续$b$之间的距离趋向于无穷。我们为这些语言发展了一套理论，重点关注可判定性和封闭性。我们定义了一个等价的自动机模型，扩展了Büchi自动机。主要的技术结果是一个补集引理，适用于只使用一种指数类型——要么是$L^B$要么是$L^S$——的语言。我们利用封闭性和可判定性结果来获得逻辑MSOLB的部分可判定性结果，该逻辑是通过扩展一元二阶逻辑并添加关于集合大小的新量词而得到的。
英文摘要：
We define a new class of languages of $ω$-words, strictly extending $ω$-regular languages. One way to present this new class is by a type of regular expressions. The new expressions are an extension of $ω$-regular expressions where two new variants of the Kleene star $L^*$ are added: $L^B$ and $L^S$. These new exponents are used to say that parts of the input word have bounded size, and that parts of the input can have arbitrarily large sizes, respectively. For instance, the expression $(a^Bb)^ω$ represents the language of infinite words over the letters $a,b$ where there is a common bound on the number of consecutive letters $a$. The expression $(a^Sb)^ω$ represents a similar language, but this time the distance between consecutive $b$'s is required to tend toward the infinite. We develop a theory for these languages, with a focus on decidability and closure. We define an equivalent automaton model, extending Büchi automata. The main technical result is a complementation lemma that works for languages where only one type of exponent---either $L^B$ or $L^S$---is used. We use the closure and decidability results to obtain partial decidability results for the logic MSOLB, a logic obtained by extending monadic second-order logic with new quantifiers that speak about the size of sets.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
