Fragments of first-order logic over infinite words

Adding modular predicates to first-order fragments

We investigate the decidability of the definability problem for fragments of first order logic over finite words enriched with modular predicates. Our approach aims toward the most generic statements that we could achieve, which successfully covers the quantifier alternation hierarchy of first order logic and some of its fragments. We obtain that deciding this problem for each level of the alternation hierarchy of both first order logic and its two-variable fragment when equipped with all regular numerical predicates is not harder than deciding it for the corresponding level equipped with only…

Level Two of the Quantifier Alternation Hierarchy over Infinite Words

The study of various decision problems for logic fragments has a long history in computer science. This paper is on the membership problem for a fragment of first-order logic over infinite words; the membership problem asks for a given language whether it is definable in some fixed fragment. The alphabetic topology was introduced as part of an effective characterization of the fragment $Σ_2$ over infinite words. Here, $Σ_2$ consists of the first-order formulas with two blocks of quantifiers, starting with an existential quantifier. Its Boolean closure is $\mathbb{B}Σ_2$. Our first main result …

Rankers over Infinite Words

We consider the four fragments FO2, the intersection of Sigma2 and FO2, the intersection of Pi2 and FO2, and Delta2 of first-order logic FO[<] over finite and infinite words. For all four fragments, we give characterizations in terms of rankers. In particular, we generalize the notion of a ranker to infinite words in two possible ways. Both extensions are natural in the sense that over finite words, they coincide with classical rankers and over infinite words, they both have the full expressive power of FO2. Moreover, the first extension of rankers admits a characterization of the intersection…

First-Order logic and its Infinitary Quantifier Extensions over Countable Words

We contribute to the refined understanding of the language-logic-algebra interplay in the context of first-order properties of countable words. We establish decidable algebraic characterizations of one variable fragment of FO as well as boolean closure of existential fragment of FO via a strengthening of Simon's theorem about piecewise testable languages. We propose a new extension of FO which admits infinitary quantifiers to reason about the inherent infinitary properties of countable words. We provide a very natural and hierarchical block-product based characterization of the new extension. …

Positive first-order logic on words

We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is a FO-definable language that is monotone in monadic predicates but not definable in FO+. This provides a simple proof that Lyndon's preservation theorem fails on finite structures. We additionally show that given a regular language, it is undecidable whether it is definable in FO+.

Asynchronous Distributed Automata: A Characterization of the Modal Mu-Fragment

We establish the equivalence between a class of asynchronous distributed automata and a small fragment of least fixpoint logic, when restricted to finite directed graphs. More specifically, the logic we consider is (a variant of) the fragment of the modal $μ$-calculus that allows least fixpoints but forbids greatest fixpoints. The corresponding automaton model uses a network of identical finite-state machines that communicate in an asynchronous manner and whose state diagram must be acyclic except for self-loops. Exploiting the connection with logic, we also prove that the expressive power of …

A model-theoretic characterization of monadic second order logic on infinite words

Monadic second order logic and linear temporal logic are two logical formalisms that can be used to describe classes of infinite words, i.e., first-order models based on the natural numbers with order, successor, and finitely many unary predicate symbols. Monadic second order logic over infinite words (S1S) can alternatively be described as a first-order logic interpreted in $\mathcal{P}(ω)$, the power set Boolean algebra of the natural numbers, equipped with modal operators for 'initial', 'next' and 'future' states. We prove that the first-order theory of this structure is the model companion…

具有上下文无关以下复杂度的非交换线性逻辑片段

Non-commutative linear logic fragments with sub-context-free complexity

本文提出了Lambek演算片段对REG、LCFL和CFL类的新的描述复杂性刻画，首次将Lambek演算片段与证明复杂性REG和LCFL等同，并基于直接转换与结构归纳展示了最弱变体的CFL复杂性，确立了Cut消解定理在比较形式文法与矢列演算中的效用。

First-Order Quantifiers and the Syntactic Monoid of Height Fragments of Picture Languages

We investigate the expressive power of first-order quantifications in the context of monadic second-order logic over pictures. We show that k+1 set quantifier alternations allow to define a picture language that cannot be defined using k set quantifier alternations preceded by arbitrarily many first-order quantifier alternations. The approach uses, for a given picture language L and an integer m > 0 the height-m fragment of L, which is defined as the word language obtained by considering each picture p of height m in L as a word, where the letters of that word are the columns of p. A key idea …

An automaton over data words that captures EMSO logic

We develop a general framework for the specification and implementation of systems whose executions are words, or partial orders, over an infinite alphabet. As a model of an implementation, we introduce class register automata, a one-way automata model over words with multiple data values. Our model combines register automata and class memory automata. It has natural interpretations. In particular, it captures communicating automata with an unbounded number of processes, whose semantics can be described as a set of (dynamic) message sequence charts. On the specification side, we provide a loca…