Forbidden Patterns for FO2 Alternation Over Finite and Infinite Words

DOI10.1142/S0129054123440021MaRDI QIDQ6169964zbMATH OpenOpenAlexFDO

Authors Viktor Henriksson, Manfred Kufleitner

Publication date 15 August 2023

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2105.09291

zbMATH Keywords

finite model theoryregular languageautomataforbidden patterninfinite words

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Model theory of finite structures (03C13) Descriptive complexity and finite models (68Q19)

Abstract: We consider two-variable first-order logic $ext{FO}^2$ and its quantifier alternation hierarchies over both finite and infinite words. Our main results are forbidden patterns for deterministic automata (finite words) and for Carton-Michel automata (infinite words). In order to give concise patterns, we allow the use of subwords on paths in finite graphs. This concept is formalized as subword-patterns. For certain types of subword-patterns there exists a non-deterministic logspace algorithm to decide their presence or absence in a given automaton. In particular, this leads to $mathbfNL$ algorithms for deciding the levels of the $ext{FO}^2$ quantifier alternation hierarchies. This applies to both full and half levels, each over finite and infinite words. Moreover, we show that these problems are $mathbfNL$-hard and, hence, $mathbfNL$-complete.

Cites work

• scientific article; zbMATH DE number 4028925 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3561239 (Why is no real title available?)
• scientific article; zbMATH DE number 1775408 (Why is no real title available?)
• scientific article; zbMATH DE number 2206109 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• A SURVEY ON SMALL FRAGMENTS OF FIRST-ORDER LOGIC OVER FINITE WORDS
• An Effective Characterization of the Alternation Hierarchy in Two-Variable Logic
• Characterizations of some classes of regular events
• Complexity of some problems from the theory of automata
• Deciding \(\mathrm{FO}^2\) alternation for automata over finite and infinite words
• Effective characterizations of simple fragments of temporal logic using Carton-Michel automata
• Finite-automaton aperiodicity is PSPACE-complete
• First-order fragments with successor over infinite words
• Forbidden patterns for ordered automata
• Fragments of first-order logic over infinite words
• Languages of dot-depth 3/2
• Level two of the quantifier alternation hierarchy over infinite words
• On finite monoids having only trivial subgroups
• On the expressive power of temporal logic
• Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words
• The \(\mathrm{FO}^2\) alternation hierarchy is decidable
• The half-levels of the \(\mathrm {FO}_2\) alternation hierarchy
• Unambiguous Büchi automata.
• Varieties

This page was built for publication: Forbidden Patterns for FO² Alternation Over Finite and Infinite Words

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6169964)