文章基本信息

标题：Boundedness in languages of infinite words
本地全文：下载
作者：Colcombet, Thomas ; Bojańczyk, Mikołaj
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2017
卷号：13
期号：4
语种：English
出版社：Technical University of Braunschweig
摘要：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. Thenew expressions are an extension of $\omega$-regular expressions where two newvariants of the Kleene star $L^*$ are added: $L^B$ and $L^S$. These newexponents are used to say that parts of the input word have bounded size, andthat parts of the input can have arbitrarily large sizes, respectively. Forinstance, the expression $(a^Bb)^\omega$ represents the language of infinitewords over the letters $a,b$ where there is a common bound on the number ofconsecutive letters $a$. The expression $(a^Sb)^\omega$ represents a similarlanguage, but this time the distance between consecutive $b$'s is required totend toward the infinite. We develop a theory for these languages, with a focus on decidability andclosure. We define an equivalent automaton model, extending B\"uchi automata.The main technical result is a complementation lemma that works for languageswhere only one type of exponent---either $L^B$ or $L^S$---is used. We use the closure and decidability results to obtain partial decidabilityresults for the logic MSOLB, a logic obtained by extending monadic second-orderlogic with new quantifiers that speak about the size of sets.
关键词：Computer Science - Formal Languages and Automata Theory;Computer Science - Logic in Computer Science