一句话：定义扩展 ω-正则语言的无限字语言类，用有界/无界 Kleene 指数与自动机刻画，并给出可判定与封闭性结果。
论文在 ω-正则表达式上新增两类 Kleene 指数 L^B 与 L^S，用于表达输入片段的长度有界或无界：L^B 要求某类片段存在公共上界，L^S 允许片段长度任意大但趋于无穷。由此定义一个严格包含 ω-正则语言的无限字语言类，并给出等价的自动机模型，扩展 Büchi 自动机。作者发展该语言类的封闭性与可判定性理论；主要技术结果是当表达式只使用一种指数（L^B 或 L^S）时成立的补语言引理。基于这些结果，论文进一步得到 MSOLB——在单子二阶逻辑上加入谈论集合大小的新量词——的部分可判定性结果。
We define a new class of languages of $\omega$-words, strictly extending $\omega$-regular languages. One way to present this new class is by a type of regular expressions. The new expressions are an extension of $\omega$-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)^\omega$ 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)^\omega$ 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\"uchi 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1708-09765,
title = {Boundedness in languages of infinite words},
author = {Mikołaj Bojańczyk and Thomas Colcombet},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:3)2017}
}